Dafny：让编译器用数学证明你的代码是对的
验证感知的编程语言 Dafny 全解析：边写代码边写规格（requires/ensures/invariant），编译器用 Z3 自动证明正确性；Dafny → Boogie → Z3 三层引擎、可编译到 Java/Go/Python 多目标、与 Coq/Lean 的自动 vs 交互之分，以及 AWS 用它重写每秒 10 亿次授权引擎的工业案例。
上篇聊了 AI-Native SDLC——让 agent 把代码写得越来越快。但写得快从来不等于写得对。 当越来越多代码由模型生成，一个老问题反而更尖锐：你怎么确信这段代码真的满足它该满足的东西？
测试能覆盖有限样本；而 Dafny 走得更远——它是一门「验证感知」的编程语言， 你边写代码边写规格（前置条件、后置条件、循环不变式），编译器用 SMT 求解器自动把「代码满足规格」证明出来。不是「在这些测试下通过了」，而是「对所有可能输入，数学上成立」。
一、先说它是什么：边写边证
Dafny 的官方定义很精确：一门内置规范构造、并配有一个静态程序验证器的验证感知语言。 它把复杂的自动推理和熟悉的编程习惯绑在一起，让开发者能写出「相对规格而言可证明正确」的代码。
关键区别就一句话：验证是编译的一部分，不是事后测试。你在写代码时，验证器实时查错、给反例、确认规格被满足。比如一个求最大值的函数，规格是这样写的：
method Max(a: int, b: int) returns (m: int)
ensures m >= a && m >= b // 返回值不小于两个输入
ensures m == a || m == b // 返回值必须是其中之一你不用写测试去枚举输入，验证器直接证明：无论 a、b 取什么整数，返回值都满足这两条。 这就是它和「看起来对」的本质差距。
二、从微软研究院到 AWS 授权引擎
Dafny 由 Rustan Leino 在微软研究院于 2008 年启动，前身是 ESC/Modula-3、ESC/Java、Spec# 一脉的验证研究。 今天它由社区组织 dafny-lang 维护（MIT 许可，约 3.5k star，最新 v4.11.0），Leino 本人现在 AWS 工作，并在 2023 年出了 MIT Press 专著《Program Proofs》。
但真正让 Dafny 不只是学术玩具的，是 AWS 的旗舰案例：
- 授权引擎每秒调用 10 亿次，原先用 Java 写，要演进又必须向后兼容；
- AWS 选择用 Dafny 重写新引擎（而非去证明旧代码），再编译回 Java；
- 耗时约 4 年（~2020–2024），2024 年无事故上线，性能提升 3 倍；
- 全程用差异测试 + 影子测试，对 10¹⁵ 量级的真实样本做了比对；
- 成果写成 ICSE 2025 论文《Formally Verified Cloud-Scale Authorization》。
核心经验就一句：对关键系统，重写一遍带证明的代码，比给旧代码补证明更划算。
三、编程模型：把规格写进代码
三个最常用的规范构造：
| 构造 | 关键字 | 含义 |
|---|---|---|
| 前置条件 | requires | 调用者必须保证成立（如「除数非零」） |
| 后置条件 | ensures | 函数返回时必须成立（如「结果最大」） |
| 循环不变式 | invariant | 每次循环前后都保持为真，用来证循环正确 |
还有 ghost 代码：只参与规范和证明、不进最终编译（幽灵变量、幽灵函数）。 看一个完整的二分查找，规格把「数组有序、返回下标对得上 key、找不到时确实没有」一次性写死：
method BinarySearch(a: array<int>, key: int) returns (result: int)
requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j] // 数组已排序
ensures -1 <= result < a.Length
ensures 0 <= result ==> a[result] == key
ensures result == -1 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
var low := 0;
var high := a.Length;
while (low < high)
invariant 0 <= low <= high <= a.Length
invariant forall i :: 0 <= i < low ==> a[i] < key
invariant forall i :: high <= i < a.Length ==> key < a[i]
{
var mid := low + (high - low) / 2;
var midVal := a[mid];
if (midVal < key) {
low := mid + 1;
} else if (key < midVal) {
high := mid;
} else {
result := mid;
return;
}
}
result := -1;
}注意不变式里那两行 forall：它们精确刻画了「low 左边都比 key 小、high 右边都比 key 大」。 验证器据此自动推出函数整体正确——你要做的不是补测试，而是把不变量想清楚。
四、验证引擎揭秘：Dafny → Boogie → Z3
你写的程序不会直接被「证明」，而是经过三层翻译：
| 层 | 是什么 | 职责 |
|---|---|---|
| Dafny | 你写的程序（代码 + 规格） | 翻译成下面的中间语言 |
| Boogie | 中间验证语言（IVL，微软研究院出品） | 用语义保持的翻译，再生成一阶逻辑「验证条件」 |
| Z3 | SMT 求解器（同样出自微软研究院） | 自动判定验证条件是否可满足——绝大多数情况无需你手动介入 |
这正好对比出验证和测试的天壤之别：
| 维度 | 测试 | 验证 |
|---|---|---|
| 覆盖范围 | 有限输入样本 | 所有可能输入 |
| 保证级别 | 「在这些测试下通过」 | 「数学上证明正确」 |
| 失败反馈 | 测试输入 | 反例（最小的破坏情形） |
| 开销发生地 | 运行时 | 编译时 |
补充一点：Z3 这类 SMT 求解器对「小改动导致证明突然失败」很敏感（证明不稳定）。 实战里靠多写不变式、用 assert 当路标、调 {:fuel} / {:trigger} 来控制展开与量化实例化来稳住它。
五、验证完还能跑：编译到多语言
Dafny 不是停在「证明完就完事」——它把验证过的代码编译成真实可部署的程序。 稳定支持的目标包括 C#、Java、JavaScript、Go、Python（C++ 仍实验性），命令就像：
dafny verify program.dfy # 只验证
dafny build --target:java program.dfy # 编译为 Java
dafny run program.dfy # 验证并直接跑工具链还包括 VSCode 扩展（边写边证、错误高亮、反例展示）、语言服务器（Emacs/Vim 也能用）、以及标准库与数学引理集。 一个坑要记牢：通过 {:extern} 调用目标语言函数（FFI）时，那部分代码不被验证—— 边界处需要额外的测试或人工保证。
六、Dafny vs 其他验证工具
常拿来比较的「证明系」语言，差异主要在「自动 vs 交互」：
| 工具 | 类型 | 交互性 | 可编译目标 |
|---|---|---|---|
| Dafny | 自动验证 | 低（自动） | 多目标 |
| Coq / Lean | 交互式证明 | 高（手动推演） | 无 |
| F* | 混合 | 中 | 无 |
| Why3 | 自动验证 | 低 | 无 |
| SPARK | 自动验证 | 低 | Ada |
Dafny 的甜点在于：大多数情况自动证完，验证完还能编译成多种语言，且有 AWS 这种生产级案例。 它和 Rust 也不冲突——Rust 在编译期保证「不崩溃」（内存安全、无数据竞争），Dafny 证明「做对了事」（业务逻辑正确），二者互补。
七、何时用，何时不用
适合：
- 安全关键系统——加密、授权、协议，错一次的代价极高；
- 核心算法——排序、搜索、图算法，需要数学级正确性；
- 长期维护的代码——规格即文档，重构时有验证兜底；
- 有合规要求的行业（航空、金融）。
不适合：
- 性能极度敏感、要手调汇编级优化的代码（生成码未必最优）；
- 快速原型——写规格本身要时间，迭代反而慢；
- 与大量未验证代码交互（FFI 边界会漏）；
- 并发程序（Dafny 主要验证顺序程序，并发需额外工具如 Civl）；
- 简单 CRUD——测试就够，验证是杀鸡用牛刀。
小结
把这篇收成三句话：
Dafny 是一门验证感知语言：你边写代码边写规格，编译器用 Z3 把「代码满足规格」自动证明出来。 它不是测试，而是对所有输入的数学证明；并且证明完还能编译成 Java/Go/Python 等真实部署。 AWS 用它重写了每秒 10 亿次调用的授权引擎——验证早已走出象牙塔。
- 验证超越测试。测试是「在这些输入下正确」，验证是「在所有输入下正确」； 代价是你要先把不变式想清楚，而不是堆测试用例。
- 它不是学术玩具。AWS 用 Dafny 重写授权引擎，4 年、3 倍性能、零事故上线—— 对关键系统，「重写带证明」往往比「给旧代码补证明」更划算。
- 和 AI 写代码是同一道题的两面。Agent 让代码变多、变快，正确性反而更稀缺； 把规格写进语言的 Dafny，正好指向「机器生成、机器证明」那条路。
想动手：官网 dafny.org， 仓库 github.com/dafny-lang/dafny， 另有在线教程、参考手册与 Leino 的《Program Proofs》。