形式化验证入门：用 Lean 定理证明器保证代码正确性

形式化验证用数学证明而非测试来保证代码正确性。Lean 定理证明器兼具函数式编程语言和定理证明器双重身份，能在区块链、密码学、操作系统等关键领域消除人为证明错误。本文从依赖类型、策略系统到 Shannon 密码抽象，带你入门可验证软件的世界。

本节你将能

理解形式化验证的核心思想和 Lean 定理证明器的基本架构
掌握依赖类型、策略系统等关键概念
编写第一个 Lean 证明：从定义到验证的完整流程

直觉模型

传统软件测试就像用探照灯检查一座大楼——你能照亮每个角落，但永远无法保证暗处没有裂缝。形式化验证则是对建筑结构进行数学建模，用严密的逻辑证明整栋楼在所有可能的外力下都不会倒塌。

Lean 由 Leonardo de Moura 于 2013 年在微软研究院创建，它具有双重身份：既是纯函数式编程语言，又是定理证明器。你可以用它写程序，也可以用它证明数学定理——而如果证明能通过 Lean 编译器检查，就意味着证明是正确的。

图1：传统测试与形式化验证的对比

核心概念

1. 依赖类型（Dependent Type）

Lean 的类型系统比主流语言更强大——类型可以依赖于值。例如 BitString (L : Nat) 可以根据不同长度 L 生成不同类型实例，让编译器在类型层面区分 8 位和 16 位比特串，杜绝长度不匹配的错误。

structure BitString (L : Nat) where
  data : Vector Bool L

-- 8 位和 16 位是不同类型，不可混淆
variable (a : BitString 8)
variable (b : BitString 16)
-- a + b 会在编译期报错

2. 策略系统（Tactics）

Lean 不要求你手写完整证明，而是通过策略一步步化简证明目标：

intro — 将假设引入上下文
simp — 自动化简等价表达式
apply — 应用已知定理
rfl — 通过计算相等性证明
exact? — 让 Lean 自动搜索可用证明

theorem xor_comm (a b : Bool) : xor a b = xor b a := by
  simp [xor, Bool.xor]

3. Shannon 密码抽象

Lean 能将密码学理论精确形式化。以下定义了 Shannon 密码的抽象结构，并证明一次性密码本（OTP）是它的实例：

structure ShannonCipher (K M C : Type) where
  enc : K -> M -> C
  dec : K -> C -> M
  correctness : forall k m, dec k (enc k m) = m

instance OTP_is_Shannon : ShannonCipher (BitString n) (BitString n) (BitString n) :=
  { enc := fun k m => xor k m
    dec := fun k c => xor k c
    correctness := fun k m => by simp [xor, Bool.xor] }

图2：Lean 形式化验证的标准工作流

实际应用场景

区块链与密码学：Shielded Labs 用 Lean 验证 Zcash 的 Orchard 电路；Nethermind 验证了 SP1 中的芯片
操作系统内核：seL4 微内核用形式化方法证明了内核实现的正确性
编译器验证：CompCert（C 编译器）的编译过程经过形式化验证
数学研究：Lean 的 mathlib 库已形式化了现代数学的大量定理

核心要点

Lean 既是编程语言也是定理证明器，核心优势是机器可检查的证明
依赖类型让编译器在类型层面捕获更多错误
策略系统提供自动化辅助，不必手写每一步证明
形式化验证适用于安全关键系统，成本高但提供数学确定性
局限性：实际代码与形式化模型之间始终存在抽象差距