Dafny/Lean：程序验证语言

可视化演示

展示形式化验证三大核心：霍尔三元组{P}S{Q}验证流程、Dafny自动证明管线（Code→Spec→VCG→Z3）、Dafny/Lean多维度对比。切换步骤查看不同验证机制。

验证语言概述

假设你一觉醒来，AI 施工队已经用铲车般的速度盖好了一座二十层楼。你很高兴，但心里打鼓：承重墙真的安全吗？传统做法是请验收员拿锤子敲几面墙——这就像单元测试，只能抽查。可楼有二十层，万一没敲到的那层恰好有裂缝呢？你需要一种“不用逐块敲，却能保证每块砖都合格”的验收方法。

程序验证语言给出的答案，是把“施工合同”和“建筑图纸”同时交给验证器，让它在数学上证明：只要按合同施工，整栋楼的每一层都满足要求。程序验证（formal verification）就是这样的数学验收：它不依赖“多试几个输入”的运气，而是用演绎推理穷尽所有可能的输入路径，把“程序正确”变成一条可证明的定理。

程序正确性通常拆成两层：功能正确性，指输出符合预期；安全性，指不崩溃、不越界、不发生产生死锁。传统软件工程靠测试、代码评审、静态分析不断逼近正确性，但测试永远覆盖不了无穷的输入域。形式化验证则把检查对象从“有限算例”提升为“全体输入”，这就是它和测试最本质的分野。

$$\displaystyle \text{Correct}(f) \equiv \forall x \in \text{Input}:\; P_{\text{pre}}(x) \rightarrow Q_{\text{post}}(x, f(x))$$

1. 全称量词 ∀：表示“对每一个输入都要考核”，而不是测试式的抽样抽查——这是验证与测试最本质的分野。

$$\forall x$$

2. 输入域 Input：程序允许接受的所有合法输入的集合，规模可能无穷大，这也决定了测试永远无法覆盖完全。

$$\text{Input}$$

3. 前置条件 P_pre(x)：输入 x 进入函数之前必须具备的资格，相当于施工前对地基的要求——不满足就不允许开工。

$$P_{\text{pre}}(x)$$

4. 蕴含箭头 →：逻辑上表示“前提成立，结论就必须成立”，它把前置条件和后置条件串成一条硬性承诺。

$$\rightarrow$$

5. 后置条件 Q_post(x, f(x))：函数在输入 x 上运行后，输出 f(x) 必须兑现的验收承诺，如“返回值不小于每个元素”。

$$Q_{\text{post}}(x, f(x))$$

回到施工队的比喻：Dafny 和 Lean 就是两位风格迥异的数学检察官。Dafny 像举着扫描仪的自动巡检员，Lean 像亲手拼榫卯的匠人。它们不敲墙，而是用数学证明整栋楼每一面墙都安全——这就是验证语言存在的全部意义。

Dafny 规范验证

现在认识第一位检察官：Dafny。它的工作方式像签合同：代码还没跑，先把“开工前必须满足什么”和“完工后必须保证什么”白纸黑字写进代码。这两样东西，在 Dafny 里分别叫 requires（前置条件）和 ensures（后置条件）。就像装修合同里写“动工前，墙必须是空的；完工后，垃圾必须清走”，Dafny 要求程序员在函数头上写明这份合同。

这段“合同”不是给人看的摆设。Dafny 的验证器会拿它当法律条文，逐条核对函数体是否兑现承诺。如果函数实现里有一条路径违反了合同，验证直接失败。比如下面这个“找数组最大值”的函数，合同规定：数组不能为空（前置），返回的 max 不小于每个元素且必须是某个元素（后置）。

除了前后置条件，Dafny 还有第三个关键工具：循环不变量（invariant）。盖楼时每一层都要遵守“承重墙不得移位”这个规则，每层都保持不变的性质就是循环不变量。验证循环时，Dafny 需要程序员提供它，然后检查三件事：进入循环前是否成立、每轮迭代后是否仍成立、退出循环后能否推出目标结论。这个检查过程在逻辑学里有经典的三元组记号。

$$\displaystyle \{P\}\; S\; \{Q\}$$

1. 花括号里的 P：前置条件，描述程序片段 S 执行前的世界状态，好比开工前“地基必须平整”。

$$P$$

2. 程序片段 S：待验证的那段代码，比如 FindMax 的整个循环体，像一整个施工工序。

$$S$$

3. 花括号里的 Q：后置条件，描述 S 执行后的世界状态，好比完工后“墙体必须垂直”。

$$Q$$

4. 三元组整体：读作“只要 P 成立，并且 S 正常结束，Q 就必然成立”——这是对“这面墙安全”的数学定义。

$$\{P\}\;S\;\{Q\}$$

回头看那段 Dafny 代码：“数组非空”是入场券，“max 是最大元素”是验收标准，“已扫描区间的最大值”是每层楼的结构规则。前置条件、后置条件、循环不变量三位一体，Dafny 才会在验证报告上盖章放行。

method FindMax(a: array<int>) returns (max: int)  requires a.Length > 0  ensures forall i :: 0 <= i < a.Length ==> a[i] <= max  ensures exists i :: 0 <= i < a.Length && a[i] == max{  var i := 1;  max := a[0];  while i < a.Length    invariant 1 <= i <= a.Length  {    if a[i] > max { max := a[i]; }    i := i + 1;  }}

Dafny 自动证明

Dafny 最让程序员省心的是“自动”二字。巡检员不是拿锤子逐面墙敲，而是举着一台扫描仪扫遍整栋楼的所有可能裂缝。这台扫描仪，就是 SMT 求解器（Satisfiability Modulo Theories，可满足性模理论求解器），最著名的实现是微软的 Z3。

Dafny 的自动证明分三步走。第一步，把程序翻译成一组“验证条件”（verification condition，VC）——这是一串数学命题，意思大致是“前置条件满足、代码走到某一步、后置条件被违反，这三件事不可能同时发生”。第二步，把验证条件交给 SMT 求解器，让它判断是否存在一个输入让这三件事同时成立。第三步，看结果：找不到这样的输入，验证通过；找到了，恭喜你，那是一个活生生的反例（counterexample）。

这里的关键是“符号执行”思想：扫描仪不需要枚举具体数值，而是把输入当成未知数 x，把所有代码路径翻译成约束方程，一次性判定“是否存在某个 x 撕毁合同”。这比跑一百万条测试更彻底，因为方程覆盖的是无限个可能性。下面的公式就是 SMT 求解器要回答的问题。

$$\displaystyle \forall x:\; \big(P(x) \land \neg Q(x, f(x))\big) \rightarrow \bot$$

1. 前置条件 P(x)：输入 x 的入场资格，例如“取款金额必须大于零”。

$$P(x)$$

2. 后置条件的否定 ¬Q(x, f(x))：表示“承诺被违背”，例如“取款后余额没有减少那么多”——这正是验收员最想抓的裂缝。

$$\neg Q(x, f(x))$$

3. 合取 ∧：把“资格达标”和“承诺被违背”拼在一起，组成一个“坏输入”的条件。

$$\land$$

4. 蕴含矛盾 → ⊥：坏输入会导致逻辑上的矛盾（⊥ 读作“底”，表示假），所以坏输入不可能存在。

$$\rightarrow \bot$$

5. 全称量词 ∀x：对所有输入一次性判定，不需要逐个枚举——这就是 SMT 扫描仪比人工敲墙快的原因。

$$\forall x$$

所以 Dafny 的“自动”不是魔法：它把“抓 bug”变成“解方程”。扫描仪找到裂缝（反例）就报错，找不到就盖章通过。这有点像医院里的 CT 扫描——医生不是用肉眼看一个个细胞，而是让机器把所有组织切面成像，病灶自然无所遁形。

Lean 依赖类型

第二位检察官 Lean 出身不同。如果说 Dafny 是巡逻的巡检员，Lean 更像一位榫卯匠人：它不满足于“证明某栋楼是安全的”，而是把“安全证明”本身做成一件可以被检查的实物。这个“实物”，在 Lean 里叫证明项（proof term）。

Lean 的核心秘密是“依赖类型”（dependent type）和“命题即类型”（propositions as types，即柯里-霍华德对应）。一个命题，比如“对所有正整数 n，1+2+…+n = n(n+1)/2”，在 Lean 里就是一种类型；而这个命题的证明，就是该类型的一个值。构造出这个值，等于完成证明；而这个值能否被构造，由 Lean 的类型检查器说了算。

这带来一个奇妙的结论：写证明就是写程序，检查程序就是检查证明。类型检查器像榫卯质检员，一块一块核对：你的“证明木块”是否严丝合缝地嵌进了“命题榫槽”。精益（Lean）里常见的归纳类型（如自然数、列表）是这种结构的基石，它允许程序员用递归方式定义数据，用归纳方式证明性质。

$$\displaystyle A \land B \;\cong\; A \times B$$

1. 合取 A ∧ B：命题逻辑中的“且”，要求 A 和 B 同时成立，好比两面承重墙都要安全。

$$A \land B$$

2. 笛卡尔积 A × B：类型的乘积，即“(A 的证明，B 的证明)”这个有序对，好比两个木件拼成一件作品。

$$A \times B$$

3. 同构 ≅：两个结构在数学上完全对应，可以互相转化，因此证明合取命题等价于构造乘积类型的值。

$$\cong$$

4. 整体含义：证明“且”只需提供两个部分的证明——验证 A 和验证 B 各一条路径，合起来就是完整的验收。

$$A \land B \sim A \times B$$

Lean 的哲学从这个等式可见一斑：它不信任“肉眼验收”，只信任“亲手拼装”。你把证明逐块拼出来，类型检查器逐块复核，任何一块不合卯，验证立刻失败。这种“证明即实物”的特性，让 Lean 能验证比 Dafny 更复杂的数学定理——这也是它在数学界和形式化方法领域备受推崇的原因。

定理证明方法

榫卯匠人怎么干活？有两种姿势。第一种是直接构图，在 Lean 里叫证明项模式（term mode）：你亲手写出完整的证明表达式。第二种更常用，叫策略模式（tactic mode）：你用一串策略（tactic），比如 intro、apply、exact，像解谜一样把目标逐步拆解，Lean 在后台帮你补全细节。对不擅长写原始证明项的人来说，策略模式友好得多。

解谜的关键招式之一是归纳证明（induction）。盖楼时，你想证明“每一层的安全承诺都成立”，只需两步：先证明第 0 层成立（基础情形），再证明“如果第 n 层成立，第 n+1 层也成立”（归纳步）。这两步一旦完成，整栋楼的安全就由“递推链条”自动传递，不需要你逐层检查。

递归定义与归纳证明是一对搭档：你用递归定义描述函数（比如计算阶乘），用归纳法证明它的性质（比如 factorial n 恒大于 0）。Lean 还内置自动化工具，比如 simp 能自动化简代数式，omega 能自动处理线性不等式——这就像老匠人手里有一本“常用榫卯速查表”，平凡工序一翻即得。归纳法本身在 Lean 中也是一个内建模板，对应自然数的归纳类型。

$$\displaystyle \text{ind}:\; P(0) \rightarrow \big(\forall n.\; P(n) \rightarrow P(n+1)\big) \rightarrow \forall n.\; P(n)$$

1. P(0)：基础情形——第 0 层的安全承诺成立，相当于第一块多米诺骨牌被推倒。

$$P(0)$$

2. 归纳步 ∀n. P(n) → P(n+1)：任意一层成立则下一层也成立，相当于骨牌之间的间距恰好能让上一块推倒下一块。

$$\forall n.\; P(n) \rightarrow P(n+1)$$

3. 整体连接 →：两个前置证明义务（基础 + 归纳步）都满足后，结论自动推出。

$$\rightarrow$$

4. 结论 ∀n. P(n)：所有楼层全部成立——你省掉了逐层检查的体力活，因为递推链条把安全传给了每一层。

$$\forall n.\; P(n)$$

这个公式的全部要点是：用两个短小的证明，换取无限层的安全。Lean 的策略模式就是这个链条的施工手册——每一条 tactic 是一道工序，最终作品（证明项）被类型检查器验收。匠人推倒第一块骨牌，剩下的交给数学。

AI 代码验证应用

回到开头的 AI 施工队。今天的大模型能飞速生成代码，但和施工队一样，偶尔会敲掉承重墙：数组越界、空指针、边界条件错误。传统单元测试像验收员抽查，可大模型生成的代码千变万化，测试用例永远跟不上。这时候，两位数学检察官就派上了用场。

验证语言给 AI 代码交付提供了“最后一道闸门”：让 AI 生成代码时同时生成“合同”（Dafny 规范或 Lean 规范），然后自动验证。如果验证通过，代码才能合并进主干；如果发现反例，把反例作为反馈喂回给大模型让它修改——这就是“生成-验证-修复”闭环。换句话说，AI 负责速度和创意，验证器负责底线。

实践中已有三种落地姿势：在 CI/CD 流水线里集成 Dafny 验证，守住安全关键函数（余额计算、权限校验）；用 Lean 形式化验证智能合约这类“一旦出错损失巨大”的组件；以及用验证器批量生成反例，作为高质量训练数据反向改进模型。要注意的是，形式化验证的对象不是“模型的思考过程”，而是“模型产出的每一段代码”——我们证明的是代码遵守合同，而不是模型的意图。

$$\displaystyle \forall c \in \text{Gen}(T):\; \text{Verify}(c, \text{Spec}_{T}) \Rightarrow \text{Deploy}(c)$$

1. Gen(T)：大模型针对任务 T 生成的全部候选代码，好比施工队一夜之间起的所有楼层方案。

$$\text{Gen}(T)$$

2. ∀c：每个候选都要过闸，没有豁免——这正是验证与测试的区别，测试可能漏检，验证不放过任何一个。

$$\forall c$$

3. 合同 Spec_T：任务 T 的形式化规范，包含前置条件、后置条件和循环不变量，相当于项目的完整验收标准。

$$\text{Spec}_{T}$$

4. 验证 Verify(c, Spec_T)：验证器检查候选 c 是否兑现合同，等价于数学检察官对每一层楼逐条核对图纸。

$$\text{Verify}(c, \text{Spec}_{T})$$

5. 上线部署 ⇒ Deploy(c)：只有验证通过的代码才允许上线，把“AI 生成得快”和“数学保证得稳”焊死在一起。

$$\Rightarrow \text{Deploy}(c)$$

当一个错误的代价是飞机失事、合约被盗、患者误诊时，这道数学闸门就不是可选项，而是交付的底线。施工队负责速度，检察官负责质量——AI 时代最可靠的交付方式，正是这两者的组合。

AI 应用场景

Python 演示

# 迷你验证器: 用穷举搜索演示 Dafny 验证器的核心思想 - 寻找反例 def make_contract(pre, post):    """Return a decorator checking pre/post conditions around a function."""    def decorator(func):        def wrapper(*args):            if not pre(*args):                raise ValueError("precondition failed: %s" % (args,))            result = func(*args)            if not post(*args, result):                raise RuntimeError("postcondition violated: %s -> %s" % (args, result))            return result        return wrapper    return decorator  @make_contract(pre=lambda x: x >= 0, post=lambda x, r: r == x * x)def square(x):    return x * x  def buggy_max(a):    """Return a wrong max: all-negative arrays produce 0, violating post."""    m = 0    for v in a:        if v > m:            m = v    return m  def max_post(a, r):    return all(v <= r for v in a) and any(v == r for v in a)  def find_counterexample(func, pre, post, cases):    """Check inputs against the contract and return the first counterexample."""    checked = 0    for case in cases:        args = case if isinstance(case, tuple) else (case,)        if not pre(*args):            continue        checked += 1        result = func(*args)        if not post(*args, result):            return ["fail", args, result, checked]        # 此输入通过检查, 继续下一组    return ["pass", None, None, checked]  if __name__ == "__main__":    print("square(4) =", square(4))    try:        square(-1)    except ValueError as e:        print("square(-1) rejected:", e)     print("buggy_max([-3, -2, -1]) =", buggy_max([-3, -2, -1]), "(expected -1)")    cases = [([-3, -2, -1],), ([0, 5, -1],), ([2],), ([9, 8, 7],)]    status, bad_args, bad_result, count = find_counterexample(        buggy_max, lambda a: len(a) > 0, max_post, cases    )    print("verification:", status, "| counterexample:", bad_args,          "| wrong output:", bad_result, "| inputs checked:", count)

1. def make_contract(pre, post):把前置/后置条件打包成装饰器，相当于 Dafny 的 requires 与 ensures 语法。
2. raise ValueError("precondition failed: %s" % (args,))前置条件不满足立即拦下，好比地基不合格不允许开工。
3. raise RuntimeError("postcondition violated: %s -> %s" % (args, result))后置条件违反立即报警，好比完工后验收不过关。
4. @make_contract(pre=lambda x: x >= 0, post=lambda x, r: r == x * x)声明 square 的合同：输入非负，输出等于 x 的平方。
5. def find_counterexample(func, pre, post, cases):验证器核心：逐条检查输入，寻找反例，对应 Dafny 的自动证明流程。
6. if not pre(*args):跳过不符合前置条件的输入，因为“没资格”并不构成违约。
7. if not post(*args, result):发现反例：前置满足但后置被违反，这就是 Dafny 报告 bug 的依据。
8. return ["fail", args, result, checked]找到反例立即报告，对应 Dafny 在行内标红的错误信息。
9. return ["pass", None, None, checked]全部输入都兑现合同才算验证通过，对应 SMT 求解器返回“不可满足”。

常见误区

面试题