第 10 篇展示了 CompCert、seL4、Four Color、Mathlib4、Feit-Thompson 五个把形式化推到极致的项目。它们也共同暴露了一件事：形式化的代价非常高，证明/代码比常在 2-25:1，时间跨度通常以年计，依赖少数 deep expert。

本篇接着这条线，回答"什么时候不该上形式化"。判断的边界与判断的成本本身同等重要：错用形式化的项目要么半途而废，要么变成一份维护负担巨大的"科研作品"。

本篇分四部分：形式化能给的与不能给的、与传统验证手段的关系、典型决策维度、几条可操作的判断准则。

形式化能给的与不能给的

能给的：

  • 对被建模部分的深层正确性保证。证完后该部分的实现错误被排除到内核 + 模型外。
  • 一致的接口：能用同一种语言（Lean / Coq）同时写程序、写规约、写证明、写元理论。
  • 跨变更的稳健性：每次修改 Lean 都重新检查全部依赖；不存在"改完忘补测试导致 regression"这种事。
  • 公开的信任面：通过 #print axioms 与代码评审可精确审计相信了什么。

不能给的：

  • 对未被建模部分的保证。CompCert 不证编译器跑得快、不证它处理所有 C 边角；seL4 不证它不被功耗副信道泄密。
  • 对模型本身正确性的保证。如果建模时把"调度公平"定义错了，证完仍然是错的——只是错得整齐。
  • 对实现外部环境的保证。硬件 bug、电源故障、用户传入的奇怪输入超出规约范围——这些事形式化不挡。
  • 对理解力代价的免疫。被验证的 100 行代码经常需要 1000 行证明，团队后续维护人需要看懂前 1000 行才能动后 100 行。

总结成一句：形式化收紧"被建模部分的实现正确性"，但放大"建模成本"与"被建模边界"的判断责任。

形式化与传统验证手段的关系

形式化不是单兵作战。下面这张表把它放进现代验证组合拳里：

手段 主要发现什么 主要成本 适合阶段
单元测试 已知输入下的回归 写测试用例的时间 持续
集成测试 模块边界的契约破坏 测试基础设施 持续
模糊测试 (fuzzing) 未预期输入下的崩溃 CPU、语料维护 持续
静态分析 (lint、Coverity 等) 已知反模式（空指针、未初始化） 配置规则、噪音管理 持续
类型系统（Rust、TypeScript 等） 内存安全、空值、类型错误 学习曲线、表达力限制 编码时
模型检查（TLA+、Spin） 状态空间内违反性质的执行 状态空间爆炸、抽象正确性 设计阶段
SMT 求解（Z3、CVC5） 谓词逻辑约束可满足性 求解器超时、可判定性边界 嵌入到工具
形式化证明（Coq / Lean） 任何被建模性质的反例都不存在 高（2-25:1） 关键组件

每种手段都覆盖一个不同的"已知未知 ↔ 未知未知"象限。形式化处理的是"已知未知"中性质明确、可被穷尽验证的那一格。它不能取代任何一种其他手段，反过来其他手段也取代不了它。

工程上一个常见误区是把形式化当成"超级测试"：以为它更全面，所以可以替代单元测试。事实是相反的：形式化对被建模的性质给出完全保证，但不会自动发现你没写进规约的问题。所以单元测试、fuzzing、监控、代码评审在有形式化的项目里仍然必须保留。

seL4 验证完之后，开发团队仍然跑大规模 fuzzing 与压力测试。理由：形式化只证了"安全性质"，没证"在硬件极端工况下不被外部干扰"。

与模型检查的关系

模型检查（TLA+、Spin、NuSMV）与定理证明（Coq、Lean）都自称"形式化方法"，但定位不同：

维度 模型检查 定理证明
工作机制 在有限或抽象状态空间里穷举 在类型系统里写出构造性证明
自动化 高（按一个按钮就跑） 低（很多步骤需人写 tactic）
反例 给出具体反例路径 不直接给反例，但能定位失败的子目标
状态空间限制 必须有限或可符号抽象 无限制（可证无限对象的性质）
表达力 LTL/CTL 等模态逻辑 类型论可表达任何数学命题
适用场景 协议、并发、调度 编译器、操作系统、数学
学习曲线 中（TLA+ 几周入门） 高（Lean / Coq 几个月起步）

工程上两者经常组合使用：

  • 设计阶段用 TLA+ 写规约，模型检查找反例（Amazon S3、DynamoDB、Cosmos DB 都这样做）。
  • 关键实现用 Coq / Lean / F* 证明实现符合规约（CompCert、seL4 都这样做）。

如果项目只能选一种，选哪种取决于：

  • 性质是否能写成有限状态空间内的 LTL/CTL 公式 → 选模型检查。
  • 性质是否需要谈"对任意大的 n"、“对任意自然数序列” → 必须定理证明。
  • 团队是否有 deep expert → 没有就别上定理证明。

与轻量形式化工具的关系

在 Coq / Lean 这种"重型"工具之外，存在一组轻量形式化工具：

工具 定位 特点
F* 依值类型 + 自动化 Microsoft Research，被用于 HACL* 加密库
Dafny 程序契约 + SMT 写普通命令式语言加 requires/ensures，工具自动证
Liquid Haskell 类型精化（refinement types） Haskell 加一层后缀，编译期检查
Frama-C C 语言契约 + SMT/Coq 在 C 注释里写 ACSL 规约，工具尝试证
Why3 / SPARK Ada 子集 + 多后端 用于航空电子，工业标准 DO-178C 接受
TLA+ 状态机规约 设计阶段验证，Amazon/Microsoft 广泛使用

这些工具的共性：用 SMT/SAT 自动化掉大部分工作，把人留在"写规约"这一步。代价是表达力弱于完全的依值类型，覆盖性质有限（往往要可判定 fragment 内）。

对工程项目来说，选择顺序通常是：

  1. 先用普通类型系统（Rust、Kotlin、TypeScript）覆盖绝大多数错误。
  2. 关键代码段补 Dafny / F* / Liquid Haskell，靠 SMT 自动化获得契约级保证。
  3. 最后才考虑 Coq / Lean。

跳过前两层直接上 Coq 通常是误判：很多场景轻量工具就够了。

哪些场景值得上形式化

下面这组场景在工业实践中已经被证明值得：

  • 安全关键软件：航空电子（DO-178C Level A）、汽车（ISO 26262 ASIL D）、医疗（IEC 62304 Class C）。一次失效后果不可承受。
  • 加密协议与原语：TLS、Signal、HACL*。一旦实现错误，影响所有依赖者。
  • 编译器与运行时：CompCert、CakeML。一次 codegen bug 可能让所有下游程序无声错误。
  • 操作系统内核：seL4。一次内核漏洞可被无限利用。
  • 区块链共识与智能合约：Ethereum 早期 DAO bug 损失 6000 万美元。形式化验证 Solidity 合约已成主流。
  • 数学定理：Four Color、Feit-Thompson、Liquid Tensor Experiment 等。
  • 会计与监管合规核心：错一次数字赔不起，监管要求可追溯。
  • 军事控制软件：错误的代价同上。

哪些场景不值得

下面这组场景反复被尝试形式化、反复被证明 ROI 很差：

  • 快速原型：需求三周一变，形式化跟不上节奏。
  • UI 与前端：交互、视觉、用户体验的"正确"难以形式化。
  • 业务规则频繁变动的中后台：每次形式化的产出半年后过期。
  • 大型微服务集群的端到端流程：跨服务、跨数据库、跨网络的状态空间不可枚举；用混沌工程 + 监控更现实。
  • 依赖众多第三方 SaaS 的胶水代码：第三方接口不形式化，自己形式化是单方面承诺。
  • AI/ML 模型本身的"正确性"：模型行为本身没有精确规约。可以形式化训练管线、特征提取、安全护栏，但不能形式化"模型理解了用户意图"。
  • 遗留代码大重写：先模块化、先单元测试、先静态分析，再考虑形式化。

一种常见的失败模式：团队读完 CompCert / seL4 论文，想把自己的"核心业务"形式化。结果三个月后规约改 17 次，证明全部作废，团队转回普通开发。误区在于把"核心业务"等同于"值得形式化"——前者关乎组织优先级，后者关乎规约稳定性与失效后果。

几条可操作的判断准则

把上面的讨论压成几条问句。每个问句若是"否"，就降低形式化的优先级；若是"是"，就提高。

  1. 失效后果是否不可承受？（人命、巨额损失、监管失败）
  2. 规约是否稳定？（接下来 1-3 年大概率不会大改）
  3. 被建模对象是否有清晰语义？（编译器 IR yes，UI 交互 no）
  4. 团队是否有 deep expert？（至少 1-2 人有 3 年以上 Coq/Lean/F* 实战）
  5. 是否已经尝试过更轻量的手段并仍然不够？（类型系统、单元测试、fuzzing、SMT）
  6. 是否能承受 2-25:1 的证明/代码比与年级时间跨度？

六条都是"是"，可以认真考虑形式化。任何一条"否"，先解决那条再说。

渐进式落地：从契约到证明

不必一上来全栈 Coq。一种渐进路径：

  1. 写下规约文档。哪怕只是 Markdown，把"这段代码必须满足什么"写清楚。
  2. 加运行时断言。assert、invariant、契约。让规约能在测试里被发现违反。
  3. 接 SMT 工具。把契约写进 Dafny / Liquid Haskell / F* 的语法，让 SMT 自动尝试证明，剩下的人工补。
  4. 关键路径转 Coq / Lean。SMT 处理不了的属性（涉及任意大对象、涉及深层数据结构归纳）才进入定理证明。
  5. 持续审计 TCB。#print axioms、grep sorry、依赖更新策略。

每一步都给项目额外保证，但成本递增。提前停在合适的层级比硬上 Coq 现实得多。

模式提炼

模式 内容
形式化不替代其他验证 它是组合拳里"覆盖被建模部分"的那一拳，其他拳不能省
选场景比选工具重要 失效后果、规约稳定性、被建模对象清晰度三件事决定值不值
轻量工具先于 Coq F*、Dafny、Liquid Haskell、TLA+ 通常能覆盖大半需求
证明/代码比是硬成本 通常 2-25:1，预算与人月必须按这个比例算
渐进式比一步到位现实 规约 → 断言 → SMT → Coq，分层落地

给读者的练习

  1. 拿你正在做或熟悉的一个项目，按"六条判断准则"打分。如果总分不及格，写出哪一条是决定性短板。
  2. 找一段你认为"非常关键"的代码（约 100-500 行）。估算如果用 F* / Dafny 给它写契约 + 证明，需要多少工时。再估算用 Coq / Lean 做完全证明的工时。
  3. 想清楚：为什么 Amazon 用 TLA+（模型检查）做协议设计，但不直接对实现用定理证明？反过来 seL4 为什么不只用 TLA+？
  4. 读 Amazon 团队的 Use of Formal Methods at Amazon Web Services，理解一个超大规模工业组织怎样选择 TLA+ 而非 Coq。

衔接到下一篇

本篇说清楚了"不该做什么"。系列还差最后一篇收束：把视角拉回普通工程，给读者一份"作为日常工具的形式化"路线图。

第 12 篇会把 Liquid Haskell、F*、Dafny、TLA+、Lean 4 摆在同一张连续谱上，回答两个收尾问题：

  • 一个普通工程师在不进研究院、不写编译器的前提下，可以怎样把形式化的思维带到日常代码里？
  • 这个系列结束后，读者下一步该往哪里走？

参考资料