到第 09 篇为止，本系列把形式化方法的概念骨架、工具操作与可信基底都说清楚了。本篇离开理论，看四个被广泛引用的真实大型形式化项目：CompCert、seL4、Four Color Theorem、Mathlib4。

每个案例按同一个模板梳理：

  1. 它证了什么。
  2. 代价多大（人月、行数、时间跨度）。
  3. 信任面在哪里。
  4. 对工程或数学意味着什么。

读完本篇之后，"形式化能在工程里干到多深"这件事不再抽象——四个案例给出了四种不同形态的答案。

CompCert：一个被形式化验证的 C 编译器

证了什么：CompCert 是一个 C 子集（接近 C99，但去掉部分边角语义）的优化编译器，从 C 源代码编译到 PowerPC、ARM、x86、RISC-V 汇编。它在 Coq 里证明了一条语义保持定理：

若源程序 S 没有未定义行为，则编译后的目标程序 T 的所有可观察行为都是 S 的可观察行为的子集。

形式化的"正确"在这里被精确定义成"源语言形式化语义与目标语言形式化语义之间的精化关系"。CompCert 给两端都写了形式化语义（small-step 操作语义），并对中间 12 道 IR、约 20 个 pass 逐一证明语义保持。

代价：

  • 时间跨度：约 2005 启动，2008 第一篇主论文，至今仍在维护。
  • 规模：约 10 万行 Coq 代码（证明 + 规约），其中代码本体约 30%，证明约 70%。
  • 主要作者：Xavier Leroy 与团队（INRIA），早期约 6 人年完成第一版核心 IR pass 的语义保持证明；项目持续近 20 年，扩展到多 ISA 后端、新优化与更多 C 特性，累计投入远超首版。
  • 商业化：Absint GmbH 提供商业授权与支持，被用于航空、航天、汽车的安全关键软件。

信任面：

  • Coq 内核（10K 行，TCB）。
  • 源 C 子集的形式化语义（约 4K 行，TCB——因为"程序是不是符合用户原意"由这套语义裁判）。
  • 目标汇编的形式化语义（约 3K 行，TCB）。
  • 用 OCaml 提取出的最终可执行编译器（提取过程 TCB，OCaml 编译器 TCB）。
  • 不在 TCB 内：所有 IR 与 pass 的实现，它们都被证明语义保持。

工程意义：

  • CompCert 的中端在 Csmith 等编译器模糊测试基准下未被发现编译 bug（Yang et al. 2011 Finding and Understanding Bugs in C Compilers：Csmith 在 11 个月数千万随机程序的测试里在 GCC / LLVM 中找到数百个崩溃与错码 bug，在 CompCert 中端为零）。这是"对一段非平凡软件证明深层正确性"在可观测维度上的有力证据，但要注意：零 bug 是统计意义上的"未被找到"，不是"被证明永远没有"——CompCert 真正证明的是语义保持，模糊测试覆盖的是"语义保持是否能在实际工作负载里持续成立"。
  • 这是 Coq 在工业上"非数学领域"最有说服力的应用，也是后续验证编译器项目（CakeML、Cogent、Vellvm）的范式参考。
  • 它揭示了形式化的代价模型：证明大约是代码 2-3 倍体量，时间是项目工期 3-5 倍。
  • 它也提醒：形式化"正确"只覆盖被形式化的那部分。CompCert 不证明编译器没有内存泄漏、不证明它跑得快、不证明它处理所有 C 边角。

CompCert 是回答"形式化的工程价值是不是空话"时最常被引用的反证。

seL4：一个被形式化验证的微内核

证了什么：seL4 是 L4 系列的一个微内核（约 8700 行 C 加 600 行汇编）。NICTA / Data61 团队在 Isabelle/HOL 里完成了四层叠加证明：

  1. 抽象规约 → 可执行规约的精化：抽象的"内核应该做什么"与一份高层 Haskell 风格规约一致。
  2. 可执行规约 → C 实现的精化：高层规约与 C 代码语义一致。
  3. 二进制 = C 编译产物：GCC 编译出的二进制确实是被验证的 C 源码（用 binary verification 工具验证）。
  4. 安全性质：保密性（信息流不能从高等级泄到低等级）、完整性（低等级写不到高等级）、可用性（高优先级任务能调度到）。

合在一起得到一条惊人的结论：在 ISA 模型、硬件正确性、无侧信道、启动初始化序列正确等前提成立时，这块内核的二进制不会因实现错误违反上述安全性质。这是迄今为止人类构建过的最高保证操作系统组件。前提里任何一条被打破——例如 Spectre 类微架构漏洞、ROWHAMMER、未建模的外设行为——都落在证明覆盖范围之外。

代价：

  • 时间跨度：约 2004 启动，2009 完成核心证明，至今扩展中。
  • 规模：内核约 9000 行，证明约 20 万行 Isabelle 脚本（约 22:1 的证明/代码比）。
  • 主要作者：Gerwin Klein、June Andronick、David Cock 等十余人。
  • 工程投入：核心验证约 20 人年，加上配套工具链（二进制验证、自动化）共约 50+ 人年。

信任面：

  • Isabelle/HOL 内核（HOL 比依值类型 TCB 略大，但有 LCF 风格"小内核+证明项"架构）。
  • 抽象规约（描述内核应做什么，TCB）。
  • C 源码的形式化语义（用 Norrish 的 C 形式化，TCB）。
  • 汇编层的形式化语义（TCB）。
  • 硬件模型（什么是 ARM/x86 指令的精确语义，TCB）。
  • 不在 TCB 内：C 编译器（被 binary verification 旁路）、内核本身的实现。

工程意义：

  • 验证后的 seL4 被用于无人机、自动驾驶、卫星、医疗设备的安全关键路径，价值数十亿美元。
  • 它把"我们能形式化验证多复杂的系统"的天花板抬到操作系统内核级。
  • 它的证明/代码比 22:1 也提供了"成本上限"参考：对极高保证场景值，对常规商业软件不可能。
  • 它公开了二进制验证工具链（包括反汇编 + 等价性证明），推动了整个行业。

seL4 是回答"形式化能不能用在操作系统级"时唯一的肯定答案。

Four Color Theorem：用计算机做数学证明的早期典范

证了什么：四色定理说"任何平面地图可以用四种颜色着色，使相邻区域颜色不同"。1976 年 Appel 与 Haken 用计算机辅助首次给出证明：把所有平面图归约到约 1900 个"不可避免可约配置"，再用计算机检查每个配置可被简化。

这个证明引起争议：数学界主流接受 Appel-Haken 证明，但仍有持保留意见者，核心理由是没有人能完整复核计算机部分——计算机程序是用普通编程语言写的，没有形式化保证。

Georges Gonthier 在 2005 年用 Coq 完整形式化了四色定理证明。所有"不可避免可约配置"的检查在 Coq 里被改写成可执行函数，证明本身被压成 Coq 项，Coq 内核机械验证全部 60K+ 行证明。

证了什么的精确版本：

在 Coq 形式化的图论框架内，平面图可被四色着色这件事被 Coq 内核接受为定理。

代价：

  • 时间跨度：2000-2005，约 5 年。
  • 规模：约 60K 行 Coq 脚本，加上重写 Appel-Haken 的可约性配置检查器（约 600 个配置）。
  • 主要作者：Georges Gonthier 一人主导，约 5 人年。
  • 副产品：催生了 SSReflect tactic 库，成为 Coq 形式化大规模数学的标准武器。

信任面：

  • Coq 内核。
  • Coq 中"平面图"、“着色”、"颜色相邻"等定义。
  • 不在 TCB 内：原 Appel-Haken 的具体计算机程序（被完全替换）、所有可约性配置的检查逻辑。

工程意义：

  • 首次完整把一个"靠计算机辅助才成立"的著名数学定理压进形式化框架。
  • 解决了数学社区对原证明"不能完整人工复核"的疑虑。
  • 证明了形式化框架可以承载"现实数学规模"的论证，激励了后续 Mathlib、Liquid Tensor Experiment、PolyMath 等大型形式化项目。
  • 副产品 SSReflect 至今是 Coq/MathComp 生态的核心。

四色定理形式化是"形式化方法用在纯数学"的早期里程碑。

Mathlib4：社区驱动的大规模数学库

证了什么：Mathlib4 是 Lean 4 的数学标准库，由 Lean 社区维护。覆盖从基础代数（群、环、域、模、范畴）到拓扑、测度论、泛函分析、微分几何、数论、概率论、组合等。

它不是单一定理而是一个生态：

  • 基础结构（约 300+ 类型类，从 Monoid 到 LieAlgebra）。
  • 标准代数定理（约 10 万条）。
  • 微积分基础与流形理论。
  • 部分前沿数学，比如 Liquid Tensor Experiment 验证了 Peter Scholze 的核心引理（2021）。

代价：

  • 时间跨度：Mathlib（Lean 3 版）2017 启动，Mathlib4（Lean 4 版）2022 启动，2023 完成移植。
  • 规模：2024 年中约 130 万行 Lean 代码，1.6 万定义、13 万定理；社区每周新增数千行，当前估计约 130-160 万行（具体以 leanprover-community/mathlib4 主分支为准）。
  • 贡献者：超过 500 人，长期核心 50+ 人。
  • 完全开源、社区驱动，没有单一商业资助。

信任面：

  • Lean 4 内核（10K 行 C++）。
  • Mathlib 的所有公理使用都在 Mathlib.Init.Data.Quot 等基础文件里集中（Classical.choice、propext、Quot.sound）。
  • 每个定理可通过 #print axioms 追溯公理使用。

工程意义：

  • 是迄今为止规模最大的形式化数学库，影响了 Coq、Agda、Isabelle 等其他生态的发展方向。
  • 提供"现代数学怎样在形式化语言里组织"的活样本（type classes、bundled vs unbundled、自动 universe polymorphism、tactic 框架）。
  • 推动 Lean 4 成为新一代证明助手的事实标准。
  • 被 Microsoft、Google、Bloomberg 等公司用于内部形式化项目。

Mathlib4 的存在改变了"形式化数学是孤立的小项目"这一刻板印象——它是日活贡献者数十人、覆盖大半个本科数学的工业级库。

Feit-Thompson 定理：一个长证明的形式化

证了什么：Feit-Thompson 定理（奇阶定理）说"每个奇数阶有限群都是可解的"。原始证明 1963 年发表，长达 255 页，是 20 世纪群论的里程碑。

2012 年 Georges Gonthier 团队在 Coq + SSReflect 中完整形式化了这条定理，使用 MathComp 库（Mathematical Components）。

代价：

  • 时间跨度：约 2008-2012，约 4 年。
  • 规模：约 17 万行 Coq + SSReflect 脚本，包含约 4000 条定义、15000 条定理。
  • 主要作者：Gonthier 团队（Microsoft Research）十余人。
  • 副产品：MathComp 库成为代数形式化的事实标准之一。

信任面：Coq 内核 + 群论基本定义。

工程意义：

  • 把"长且复杂的纯数学证明"也证明可以形式化。
  • 暴露了原证明里若干被忽略的小细节（虽然没有发现根本错误）。
  • 推动了对 Coq tactic 与 dependent type class hierarchy 的工程化研究。

Feit-Thompson 形式化是"形式化能不能跟上数学规模"的肯定答案。

四个案例放在一张表里看

项目 证什么 工具 代码量 证明/代码比 时间 TCB 关键项
CompCert C 编译器语义保持 Coq 10 万行 ~2.5:1 6 人年首版核心 IR + 20 年累计扩展 Coq 内核 + 源/目标语义
seL4 微内核安全性质 Isabelle/HOL 9K C + 20 万 Isabelle ~22:1 约 25-30 人年核心 + 配套工具链 Isabelle 内核 + C/汇编/硬件语义
Four Color 四色定理 Coq 60K 极高（替换 Appel-Haken 全部） 5 人年 Coq 内核 + 图论定义
Mathlib4 大规模数学库 Lean 4 约 130-160 万行 无单一证 500+ 人持续 Lean 4 内核 + 3 条公理
Feit-Thompson 奇阶定理 Coq + SSReflect 17 万行 极高 4 年 / 6 位主要作者 + 协作十余人 Coq 内核 + 群论定义

读这张表的几条经验：

  1. 证明/代码比通常在 2-25:1 之间。这意味着形式化成本远高于普通开发——约等于"重写一份"再加"再写一份证明"。
  2. TCB 关键项有共性：都包含证明助手内核 + 被建模对象的形式化语义。语义本身是 TCB，建模错的话验证再多也没用。
  3. 跨度都是年级。形式化不是冲刺，是长跑。任何"几个月内全部形式化"的诺言都不可信。
  4. 小团队也能做世界级项目（CompCert 早期 6 人年、Gonthier Four Color 5 人年）。形式化项目高度依赖少数 deep expert。
  5. 副产品价值往往超过定理本身。SSReflect、MathComp、Mathlib、CompCert IR 设计都成为各自生态的基础工具。

形式化能干到多深

把上面五个案例归类：

层 案例 形式化的对象
数学 Four Color, Feit-Thompson, Mathlib 公理化数学体系内的定理
算法 / 数据结构 Mathlib 中可执行片段、Coq 中 RB-Tree 等 程序逻辑与不变量
编译器 CompCert, CakeML, Compiler in F* 语义保持
操作系统 seL4, CertiKOS 内核行为与安全性质
协议 Verified TLS, Tamarin 模型 协议安全性质
硬件 Kami, Catalyst, Verified RISC-V 处理器/硬件正确性

每往下一层，TCB 中的"被建模对象语义"就越接近物理。到硬件层，TCB 里必须有 ISA、电路、时序的形式化，这些建模本身的代价高得吓人。形式化能到的深度由两件事卡：

  • 被建模对象有没有清晰的语义可写。
  • 团队是否能负担 5-25:1 的证明/代码比。

工程项目要落地形式化，第一件事不是"选择工具"，而是"先判断要形式化什么、信什么、值不值"。

模式提炼

模式 内容
证明/代码比通常 2-25:1 形式化成本远高于普通开发；选场景比选工具重要
TCB 包含被建模对象的语义 建模本身写错，验证再多也没用
工业级项目都是年级 不要相信"几个月全部形式化"的承诺
副产品有持久价值 SSReflect / MathComp / Mathlib 是案例本身之外的最大遗产
形式化的"深度"由建模与人力决定 数学 → 算法 → 编译器 → 操作系统 → 协议 → 硬件，越往下成本越爆

给读者的练习

  1. 找一个你熟悉的开源组件（数据库、序列化库、Web 框架），估计若要形式化"它对接口的所有承诺"，证明/代码比可能落在多少。
  2. 读 CompCert 主论文 Formal verification of a realistic compiler, CACM 2009 前三节，看作者怎样划定"被验证的部分"与"被信任的部分"。
  3. 想清楚：seL4 验证的"安全性质"不包括什么（提示：性能、能耗、与外部硬件的并发交互、热失效）？
  4. 在 Mathlib4 仓库里翻一翻 Mathlib/Topology/Basic.lean 与 Mathlib/Analysis/Calculus/Deriv/Basic.lean，感受"现代数学被形式化时的代码密度"。

衔接到下一篇

本篇展示了"形式化能干到多深"。下一篇换姿势谈"哪些场景不值得形式化"——形式化的局限、与传统测试/模型检查/类型论的关系、什么样的工程问题更适合 fuzzing 而非证明、F*/Liquid Haskell/Dafny 等"轻量形式化"工具的位置。

第 12 篇收束系列：把视角拉回日常工程，给读者一份"作为日常工具的形式化"路线图。

参考资料