形式化方法卷 · 用数学证明"系统是对的"

一句话

"测试能证明有 bug，但永远不能证明没 bug。"形式化方法（Formal Methods）用数学严格证明系统的性质：模型检查自动穷举状态空间，定理证明器像数学证明一样推理，程序验证用逻辑保证代码符合规格。它是可靠性要求最高领域（分布式共识、加密、编译器、航空/核工业、区块链）的黄金标准——TLA+ 验过 Raft、Coq 验过 CompCert 编译器、seL4 用 Isabelle/HOL 证明了 OS 内核。

思想链

[你写了个分布式共识算法]
  └─> 测试跑了 1000 次都过 → 但并发/网络故障组合无穷, 测不完
        └─> 模型检查 (TLA+): 穷举"小规模状态空间", 找反例
              └─> 写规格 + 不变量, 自动验证: 活锁/死锁/不满足性质
                    └─> 但要证明"代码实现 = 规格" → 需要更强的工具
                          └─> 定理证明 (Coq/Lean): 证明器人机交互证明
                                └─> Curry-Howard: 命题=类型, 证明=程序
                                      └─> 程序验证: Hoare 逻辑/符号执行
                                            └─> 编译器被证明 (CompCert)
                                              └─> 内核被证明 (seL4)
                                                    └─> 安全关键系统的护城河

每一层工具解决"可靠性"的不同粒度：测试给信心、模型检查给反例、定理证明给正确性证明、程序验证把证明连到真实代码。

你将带走什么

读完应能：

说清测试、模型检查、定理证明三者的区别与适用场景。
用 TLA+ 写一个简单系统（如互斥锁）的规格并跑 TLC 模型检查。
理解 Coq/Lean 的依赖类型与 Curry-Howard，知道定理证明器和"智能代码编辑器"的区别。
理解 Hoare 三元组和程序验证的核心思路，知道符号执行、形式语义是什么。
知道哪些工业系统真用形式化方法（TLA+/Coq/Isabelle/seL4），以及为什么只在关键处用。

章节结构

与其余部分的接口

本卷章节	接口
TLA+ / 模型检查	分布式 §共识（Paxos/Raft 用 TLA+ 验证）、并发 §一致性、DSA §图搜索
Coq / Lean	理论 §形式语言/自动机、编译 §类型系统/HM、数学 §逻辑
程序验证	编译 §SSA/语义分析、软件工程 §代码质量、数学 §Hoare 逻辑基础

这卷不是什么

不是一本 Coq/Lean 完整教程（那需要单独成书）。给的是"心智模型 + 最小可跑示例"。
不是说测试没用。形式化方法解决的是测试覆盖不到的（并发组合、无穷输入、安全关键）。
不是所有项目都该上。它成本高，只在正确性代价极高时用——这是关键判断。

什么时候用

场景	用哪个
分布式算法（共识/复制/时钟）	TLA+ 模型检查
加密协议 / 密码实现	定理证明 + 程序验证
编译器 / 内核 / 调度器	Coq / Isabelle 证明
区块链共识 / 智能合约	模型检查 + 符号执行
普通 CRUD 应用	不用（测试足够）

下一篇: 1. 模型检查与 TLA+: 穷举状态空间找反例.

Keyboard shortcuts

Computer Science Notes