1996 年 6 月 4 日，阿丽亚娜 5 号首飞在点火序列开始约 40 秒后解体。调查委员会追溯出一条比"整数溢出"更完整的失效链：惯性基准系统仍在执行一段升空后已无必要的对准软件；阿丽亚娜 5 与阿丽亚娜 4 的早期轨迹不同，使一个表示水平偏差的 64 位浮点值超出 16 位有符号整数范围；这次转换没有异常保护，两套采用相同软硬件的冗余系统又以相同方式先后停机；诊断数据随后被飞行控制系统当成姿态数据。
问题不只是某一行代码，也不只是"新火箭更快"。调查报告特别指出，阿丽亚娜 5 的轨迹数据没有进入惯性系统的需求与规格分析，系统级测试也没有覆盖这条失效路径。这里同时出现了需求边界错误、复用假设失效、同源冗余和异常处理设计缺陷。
两年前，另一桩著名的"数学 bug"已经敲过警钟：1994 年，英特尔奔腾处理器的浮点除法单元（FDIV）在某些高精度除法上返回错误结果，根源是芯片内部查找表里漏填的少数项。事件最终迫使英特尔召回芯片，并在 1995 年 1 月计提 4.75 亿美元损失——这是英特尔历史上第一次 CPU 召回。一个未被穷尽验证的算术单元，代价以亿美元计。
形式化方法的核心承诺正是：在明确的模型、规约与假设下，用机器可检查的推理说明某些性质对全部被建模情形成立，而不只是说明"在我试过的输入上没出问题"。 这个限定很重要：证明可以穷尽模型中的情形，却不会自动修正遗漏的需求、错误的环境假设或模型外的实现。
破除误解：测试不等于证明
软件测试能找到 bug，但不能证明没有 bug。即使对一个函数测试了一百万种输入，仍然可能存在第一百万零一种输入触发错误。
形式化验证则不同：它可以对规约所量化的全部输入与执行证明一个具体性质成立。这里的"全部"不是整个现实世界，而是类型、内存模型、并发语义、故障模型等假设界定出的集合。代价是：你必须精确说明"哪些输入算合法""什么行为可观察""允许哪些故障"以及"正确"究竟是哪一个性质。
Dijkstra 说过一句被反复引用的话："测试只能证明 bug 的存在，不能证明其不存在。"（Program testing can be used to show the presence of bugs, but never to show their absence.）
核心工具一：Hoare 逻辑
1969 年，Tony Hoare 发表了《计算机程序设计的公理基础》（An Axiomatic Basis for Computer Programming），提出了以他命名的逻辑系统：
Hoare 三元组 表示：若程序状态满足前置条件 $P$，执行程序 $C$ 后，状态将满足后置条件 $Q$。
例如，对于整数交换程序： - 前置条件： - 后置条件：
这套逻辑有一套推理规则，允许把复杂程序的正确性分解为子程序的正确性。现代程序验证工具（如 Dafny、Why3）都基于此思想。
核心工具二：模型检验
模型检验（Model Checking）由 Clarke、Emerson 和 Sifakis 在 1980 年代初独立发展，三人因此获得 2007 年图灵奖。
它的思路是：把系统及环境抽象为状态迁移模型，把性质写成时序逻辑公式（如 CTL、LTL），再搜索可达状态。有限状态模型可以被穷尽；无限系统则通常需要有界化、抽象或符号表示。如果性质被违反，工具返回的是模型中的反例路径，工程师还要判断它能否映射到真实设计。
| 工具 | 用途 |
|---|---|
| SPIN | 并发协议验证（贝尔实验室） |
| CBMC | C 程序有界模型检验 |
| NuSMV / nuXmv | 硬件与协议验证 |
| TLA+ | 分布式系统规约（Leslie Lamport 设计，AWS 大规模使用） |
模型检验的局限是状态爆炸：系统状态数随变量数指数增长，真实软件往往无法完整枚举。符号模型检验（用 BDD 或 SAT 求解器紧凑表示状态空间）部分缓解了这一问题。
工业界的真实战果：形式化方法早已不只属于航空航天。亚马逊云服务（AWS）的工程师在 2015 年的 CACM 论文《How Amazon Web Services Uses Formal Methods》中报告：他们用 TLA+ 为多个核心系统写规约并做模型检验，在 DynamoDB 的复制与成员管理协议里发现了 3 个需要长达 35 步执行轨迹才能触发的深层 bug，又在 S3 后台数据再分布、EBS 卷管理中各发现若干 bug。这些都是只在罕见时序交错下才出现、传统测试与代码评审几乎无法捕捉的错误。一位 DynamoDB 工程师事后表示，早知道有 TLA+，他会从一开始就用它。这说明：对于并发与分布式系统，"先把设计证明对、再写代码"正在成为大型科技公司的实际工程实践，而不只是教科书里的理想。
核心工具三：定理证明助手
交互式定理证明器（Interactive Theorem Prover）允许用户在机器的辅助下构建数学证明：
- Coq / Rocq（INRIA）：使用依赖类型理论，支撑了 CompCert 多个编译阶段的语义保持证明
- Isabelle/HOL：使用高阶逻辑，支撑了 seL4 微内核从抽象规格到 C 实现的功能正确性证明
- Lean 4：微软研究院，近年在数学社区获得广泛关注，菲尔兹奖得主 Peter Scholze 曾用它验证一个复杂数学证明
2009 年，seL4 项目发表了形式化系统研究中的里程碑成果：在明确假设下，机器检查了抽象规格与约 8700 行 C 内核实现之间的功能正确性精化关系。它证明的是内核实现遵循模型规定的行为，并由此排除模型覆盖范围内的一批运行时错误；它并不自动证明驱动、应用、硬件、启动代码或用户需求全部正确。后来扩展的安全性与二进制层证明也各有自己的可信计算基与适用版本，不能用一句"整个操作系统已无 bug"概括。
幕后引擎：SMT 求解器
上面这些工具大多不是"从零手写证明"，而是把繁琐的逻辑判定交给一个底层引擎——SMT 求解器（Satisfiability Modulo Theories，可满足性模理论）。
它在布尔可满足性（SAT）之上，叠加了对整数、数组、位向量等"理论"的判定能力，能自动回答"这组约束有没有解"。微软研究院从 2006 年起开发的 Z3 是其中最有影响力的一个。
Hoare 逻辑风格的验证器（如前面提到的 Dafny）会把程序的"验证条件"翻译成逻辑公式，再交给 Z3 等求解器判定。程序员仍要提供规约、循环不变式或关键引理；工具负责自动化其中可判定或启发式可解的部分。求解器返回 unknown、超时或依赖未经检查的公理时，都不能等同于证明成功。
一份证明究竟保证了什么
阅读"已形式化验证"的项目时，可以沿着五层保证边界逐层追问：
| 层级 | 要问的问题 | 常见遗漏 |
|---|---|---|
| 目标性质 | 证明的是功能正确性、内存安全、保密性，还是活性？ | 把一种性质误写成"没有 bug" |
| 形式模型 | 输入、时间、故障与攻击者能力如何建模？ | 现实环境超出模型 |
| 精化链 | 抽象规格如何连接到源代码、编译器和二进制？ | 只验证设计，未验证实现 |
| 可信计算基 | 证明内核、求解器、编译器、硬件中哪些必须被信任？ | 证明脚本通过不代表所有工具都无错 |
| 运维边界 | 配置、密钥、依赖、部署和人机操作是否在范围内？ | 正确组件被错误配置 |
CompCert 很能说明这种边界意识。它的重要保证是语义保持：在编译成功时，生成代码的可观察行为由源程序语义约束。但项目手册也明确区分了已证明的编译阶段与预处理、解析、汇编、链接等外部或未完全验证环节。"验证过的编译器"是强而具体的保证，不是从需求到芯片的无限担保。
一个典型的现代战场是智能合约。2016 年 6 月 17 日，以太坊上的 The DAO 因一个"重入"（reentrancy）漏洞被攻击，约 360 万枚以太币（当时约 6000 万美元）被抽走——合约在更新余额之前就转出资金，使攻击者得以在同一笔交易里反复提款。
智能合约的公开状态与高额资产使形式规约特别有价值，但"证明不会重入"仍需说明调用模型、外部合约假设和升级机制。现实工程通常把形式验证与代码审计、模糊测试、属性测试、运行时监控和权限设计组合使用，而不是用一份证明替代所有防线。
如何选择验证强度
不是每个系统都需要从规格到机器码的完整证明。更实用的做法是按风险和性质选择工具：
| 问题 | 优先方法 | 能得到什么 |
|---|---|---|
| 输入边界与不变量经常出错 | 类型系统、契约、属性测试 | 低成本排除一类错误并寻找反例 |
| 并发时序难以靠测试重现 | TLA+、Alloy、模型检验 | 探索设计状态空间与反例轨迹 |
| 算法或安全性质必须对全部输入成立 | 演绎验证、SMT | 相对于程序语义的性质证明 |
| 可信基础设施需要高保证 | 交互式定理证明、精化证明 | 更强保证与更显式的假设链 |
| 实现含大量环境与第三方组件 | 测试、审计、监控与局部形式化 | 覆盖模型外风险并控制成本 |
先写出最危险的失效性质，再决定需要多强的证据，通常比先选一个证明工具更有效。
代价与争议
成本高度不均：补一个类型约束、写一个属性测试和完成微内核精化证明，不应被放在同一个成本数字里。成本取决于规约稳定性、自动化程度、团队经验、代码规模以及要证明的性质。高保证项目仍主要集中在安全关键和基础设施领域，但轻量方法已经广泛进入普通开发。
规约本身可能错误或不完整：形式化方法只能证明软件满足被写下的规约。规约遗漏关键场景时，证明仍可能完全有效，却没有覆盖用户真正关心的风险。规约评审、需求追踪、测试和事故分析因此仍不可替代。
与变化的张力：规约和实现都变化时，证明需要维护；但这不意味着形式化与迭代开发必然不兼容。可执行规格、自动模型检验和持续验证可以进入 CI，关键是把证明义务限制在稳定且高风险的接口与不变量上。
中间道路：但"全有或全无"是个伪命题。基于性质的测试（property-based testing，如 Haskell 的 QuickCheck，2000 年提出）就是一种轻量级折中——开发者像写规约一样写下程序应满足的"性质"，工具再自动生成大量随机输入去试图证伪它。它给不出"对所有输入都成立"的数学保证，却能以极低成本逼近形式化方法的思路，因此被广泛集成进日常工程。
跨域连接
- 类型系统：类型检查是自动化程度最高、覆盖性质最窄的形式方法：不用人写不变式就能排除一整类错误，代价是能表达的性质有限。整条工具谱系正沿着"自动化换表达力"这条轴排列，选点比选工具更重要。推论是：想让检查器多证一点，就得多写一点规格，天下没有白来的保证。
- 人工智能与形式化证明：证明与程序是同一件事的两面，于是证明检查器就是类型检查器。反过来，机器也开始为人类把关那些长到无人能通读的数学证明——共同体接受一个证明的依据，正从"专家可读"转向"证明内核可信"。
- 维特根斯坦：规约本身也是一段文字，它是否忠实表达了意图，无法在系统内部证明。这正是规则遵循难题的工程形态：证明可以完全有效，同时完全没覆盖用户真正在意的风险——遗漏的需求不会让任何检查器报错。推论是：规约评审、需求追踪与事故复盘，无法被任何证明工具替代。
- 循证医学：机器证明、模型检查、属性测试、单元测试构成一条证据强度谱，与循证医学的证据分级同构，也共享同一个陷阱：最高级的证据只对被严格定义的问题成立，把它外推到未被定义的场景就失效。
- 风险与不确定性：验证强度应按失效后果分配，而不是"能证就证"。在低后果场景做完整精化证明，边际收益低于把同样人力投进测试与监控；真正该先问的不是用什么工具，而是最危险的失效性质究竟是哪一条。同理，属性测试这类轻量手段之所以流行，正因为它以极低成本逼近了同一种思路。
参考文献
- Hoare, C. A. R. An Axiomatic Basis for Computer Programming. CACM 12(10), 1969.
- Clarke, E., Grumberg, O., Peled, D. Model Checking. MIT Press, 1999.
- Klein, G. et al. seL4: Formal Verification of an OS Kernel. SOSP, 2009.（seL4 验证原始论文）
- Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
- Leroy, X. Formal Verification of a Realistic Compiler. CACM 52(7), 2009.（CompCert 编译器验证）
- Newcombe, C. et al. How Amazon Web Services Uses Formal Methods. CACM 58(4), 2015.（TLA+ 在 AWS 生产系统的应用）
- de Moura, L. & Bjørner, N. Z3: An Efficient SMT Solver. TACAS, 2008.（SMT 求解器，程序验证的底层引擎）
- Lions, J.-L. et al. Ariane 5 Flight 501 Failure: Report by the Inquiry Board. 1996.（事故链与系统级测试缺口）
- CompCert Project. CompCert C: A Trustworthy Compiler — User's Manual.（语义保持定理与验证边界）