AWS 用 939 行 TLA+ 抓出 DynamoDB 35 步深坑，形式化验证到底卡在哪

一段只有 1919 个控制状态的图灵机程序，折算成 Python 也就 100 到 200 行，人类现有的数学基石（ZFC 公理系统）就已经永远无法证明它会不会停机。软件工程师 Ron Pressler 在尝试为新版 Galaxy 做形式化规范与验证时，被网上那种只要换个好工具就能轻松写出正确软件的论调惹毛了。他在 2016 年 7 月 23 日发出了一篇阅读时长约 45 分钟的硬核长文，把计算机科学的祖师爷们请出来挨个点名，核心判断只有一个，软件正确性的高昂代价就像热力学里降低熵增必须消耗能量一样，属于无法逃避的计算自然法则。

这盆冷水泼得够狠，但只泼对了一半。Pressler 把理论计算机科学里的最坏情况算得明明白白，却在程序语言理论（PLT）的逃生通道上滑了坡，也低估了工业界在不可判定性夹缝里套利的手艺。就在他写下这篇长文的前一年，AWS 团队已经在《Communications of the ACM》（58 卷第 4 期，66-73 页）上晒出了自 2011 年起的实战账本，7 个团队在 10 个复杂系统里用 TLA+ 和 PlusCal 配合 TLC 模型检验器捉虫，其中仅用 939 行 TLA+ 给 DynamoDB 建模，就揪出了一个潜伏 35 个高级步骤的致命数据丢失 Bug。

墓碑上的豪言与计算的热力学铁律

1930 年，数学家希尔伯特在哥尼斯堡发表退休演讲，喊出了后来刻在他墓碑上的名言，我们必须知道，我们必将知道。他想把所有数学形式化，做到一致、完备且可判定，也就是找到一个通用算法来判定任何形式化命题的真伪。讽刺的是，就在演讲前一天，哥德尔宣布了第一不完备定理，直接端掉了希尔伯特纲领的前两根柱子；到了 1936 年，邱奇和图灵各自证明了停机问题，把第三根柱子（可判定性）也彻底砸碎。

Pressler 顺着这条脉络，给指望全自动验证工具的程序员列出了一张绝望清单：

• 停机问题与可达性.不存在通用算法能判定任意程序是否停机，进而也无法判定任意程序能否到达某个特定状态。
• 莱斯定理（Rice's theorem）：对于部分函数的任何非平凡语义属性，都不存在通用算法能判定任意程序是否具备该属性。哪怕只是想写个工具自动判断一段代码输出的是不是输入的平方，理论上都做不到。
• 忙碌海狸函数（Busy Beaver）：一个只有 6 个控制状态的双符号图灵机，停机前最多能跑超过 $7.4 \times 10^{36534}$ 步。无论动态运行还是静态推导，证明程序停机的最小证明长度函数，增长速度都超过任何可计算函数。
• Cook-Reckhow 定理：当且仅当 NP=coNP 时，才存在对所有重言式都有多项式有界证明的命题证明系统。换句话说，只要 NP 不等于 coNP，哪怕你只是验证一个有限状态的程序属性，演绎证明的长度在最坏情况下也会发生指数级爆炸。

基於这些铁律，Pressler 抛出了两个极度悲观的推论，一个是语言抽象通常无法在验证中被利用，因为几行紧凑的高级代码背后照样是天文数字的状态空间；另一个是正确性无法分解，把代码拆成模块能让人类好读，但组件交互的验证依然是算力黑洞。

拿着莱斯定理当大锤，砸歪了哪颗钉子

Pressler 的理论科普写得极扎实，但他把可计算性理论当成大锤砸向现代强类型系统（比如依赖类型）和组合式验证时，却砸偏了准星。如果莱斯定理真的封死了一切，那今天的 Rust 借用检查器、Haskell 类型系统乃至 Idris、Lean 这些定理证明器，难道都是违背热力学的永动机？

问题出在他把对任意程序既可靠又完备的自动判定，直接等同于了工程上的软件验证。程序语言理论学者看这篇长文，一眼就能挑出三个逻辑滑坡。

第一个滑坡是忽略了不完备性逃生通道。莱斯定理只禁止同时做到可靠（Sound，没报错就一定安全）和完备（Complete，安全的程序一定不报错）。所有的静态类型检查器干的都是同一笔交易，死保可靠性，主动放弃完备性。编译器只放行一个受限的程序子集，宁可错杀一万个实际上安全但写法刁钻的合法程序，也绝不放过一个类型错误的程序。只要肯拒绝好程序，莱斯定理的封锁线当场失效。

第二个滑坡是混淆了证明搜索与类型检查。Pressler 看到依赖类型可能产生无穷的具体类型，就推导出无限复杂性和不可判定。这在逻辑上根本站不住脚，自然数有无穷多个，但判定两个自然数相不相等完全是可判定的。在依赖类型系统里，让机器自己去大海捞针找证明（证明搜索）或者不写注解硬猜（完全类型推导）确实不可判定；但一旦程序员老老实实写上类型注解，采用双向类型检查（Bidirectional type-checking），机器干的活就从自己想证明降维成了拿着答案对卷子，这在计算上完全是可判定的。

第三个滑坡是把特定参数化模型检验的困难，夸大成了正确性无法分解。早在几十年前，霍尔逻辑（Hoare logic）的序列规则就已经证明了正确性完全可以组合推理。模块化真正的痛点从来不是数学上不能组合，而是连接两个模块的那条契约（中间断言与循环不变量）无法靠机器廉价地自动生成，必须消耗人类工程师的脑力去构造。

• 结论.计算理论证明的是全自动、零成本、通用银弹的破产，而现代类型系统与形式化工具的本质，正是用程序员手工写注解和契约的确定性脑力，去置换机器状态空间爆炸的指数级算力。

AWS 的 TLA+ 账本：怎么在自然法则的夹缝里套利

既然理论允许通过受限模型和人工介入来绕开死胡同，那在真金白银的工业界，这笔账到底划不划算？

《孙子兵法》讲，水因地而制流，兵因敌而制胜。AWS 的工程师没有愚蠢到拿形式化工具去死磕几百万行底层 C 或 Java 生产代码，而是把火力全部集中在最容易出人命、测试最难覆盖的顶层分布式算法与并发状态机设计上。看看 AWS 披露的这本投入产出账：

这组数字直接把形式化验证从象牙塔拉进了工程算盘。一个逃过了广泛代码审查和压力测试的 DynamoDB 数据丢失隐患，触发路径长达 35 步，靠写集成测试去撞大运，概率跟中彩票差不多；而用 939 行 TLA+ 把高层状态机画出来，TLC 模型检验器暴力穷举状态空间，直接把最短反例拍在工程师脸上。更有说服力的是学习成本，AWS 工程师反馈，从零上手学习并应用 TLA+，通常只需要 2 到 3 周就能在项目里产出有用结果。

但 AWS 的账本同样验证了 Pressler 警告的另一面，天下没有白吃的午餐。在内部锁管理器的 223 行 PlusCal 无锁结构建模中，工程师只检查了安全性（Safety，即不会发生坏事），没有检查活性（Liveness，即好事最终一定会发生），结果就老老实实漏掉了一个活性 Bug。而且 TLA+ 验证的只是高层抽象设计，至于程序员把设计翻译成几万行 C++ 或 Java 代码时写出了指针越界或逻辑手滑，模型检验器根本管不着。

算力穷举不了无限的图灵机，但足够在百行状态机里堵死致命漏洞。

• 风险.把高层设计验证当成底层代码免死金牌，或者在建模时漏写活性与公平性约束，会让团队在虚假的安全感中放过线上死锁与饥饿故障。

回看希尔伯特墓碑上那句我们必将知道，还有那个只有 1919 个控制状态却连 ZFC 公理系统都束手无策的微型图灵机，Pressler 提醒得对，程序员确实该对计算的自然法则保持敬畏。指望靠一个新语言或新工具就躺着写出零 Bug 的软件，纯属痴人说梦。但敬畏自然法则，不等于在工程上躺平。造桥的工程师不会因为热力学第二定律说万物终将熵增，就不去计算钢梁的承重极限；写基础架构的程序员，也不该拿停机问题和莱斯定理当挡箭牌，拒绝在核心分布式状态机上花两三周写那几百行救命的 TLA+。