形式化验证的困境与出路：50年争论给工程师的启示

一场跨越半个世纪的争论

1979年，计算机科学家 Richard DeMillo、Richard Lipton 和 Alan Perlis 发表了一篇极具争议的论文《Social Processes and Proofs of Theorems and Programs》，公开质疑形式化验证（Formal Verification）作为软件正确性保障手段的可行性。形式化验证是一种使用数学方法严格证明系统行为符合预定规约的技术——与传统测试不同，测试只能通过有限用例发现错误的存在，而形式化验证试图证明错误的不存在（对所有可能的输入）。这一区别源自 Edsger Dijkstra 的著名论断：「测试只能证明 bug 的存在，而无法证明 bug 的不存在。」

形式化验证的思想根源可追溯到20世纪60年代末的「软件危机」时期。1968年NATO软件工程会议首次正式提出软件危机的概念——当时大型软件项目频繁超支、延期且充满缺陷。Dijkstra在1972年图灵奖演讲《The Humble Programmer》中系统阐述了结构化编程和程序正确性证明的理念。Tony Hoare于1969年提出了Hoare逻辑（也称Floyd-Hoare逻辑），为程序的形式化推理提供了公理化基础：通过前置条件、后置条件和循环不变量，可以对程序的每一步进行严格的数学推导。Robert Floyd则更早提出了用断言注释流程图来证明程序正确性的方法。这三位先驱共同奠定了程序验证的理论基础。

半个世纪后，这场争论重新回到人们的视野——在近期一篇引发 Hacker News 热议的文章《The Case Against Formal Verification, 50 Years Later》中，作者重新审视了当年的批评，并对照当下的技术现实进行了反思。

这场讨论在社区收获了 74 个赞与 62 条评论，说明形式化验证这个看似小众的话题，依然触动着软件工程师群体的神经。它涉及一个根本性的问题：我们究竟能否用数学的严格性来保证软件的正确性？

Hacker News 上关于形式化验证的讨论

当年的核心批评：社会过程与规约困境

时代背景与作者阵容

要理解这篇论文的分量，需要了解其作者和时代背景。Alan Perlis 是图灵奖的第一位获得者（1966年），以编程语言研究闻名；Richard Lipton 后来在计算复杂性理论和密码学领域做出重要贡献；Richard DeMillo 则在软件工程和网络安全领域有深入研究。他们发表这篇论文的时代背景是：1970年代「程序验证」运动正处于高潮，Dijkstra、Hoare、Floyd 等人大力倡导用数学方法保证程序正确性，学术界弥漫着一种乐观情绪，认为形式化方法即将彻底解决软件危机。正是在这样的学术氛围中，三位重量级学者投下了一颗「炸弹」。

数学证明依赖社会过程

DeMillo 等人当年最尖锐的观点在于：数学定理之所以被信任，并非因为其形式化的推导链条无懈可击，而是因为它经历了一个「社会过程」——被大量数学家反复阅读、检验、引用和修正。一个证明的可信度来自于人类群体的共识。

这个观点与数学哲学中的社会建构主义立场有深刻关联。数学家 Imre Lakatos 在《Proofs and Refutations》（1976年）中通过对欧拉多面体公式证明历史的考察，展示了数学证明如何在不断的反驳与修正中逐渐完善——一个定理的「正确性」不是一次证明就确定的，而是在数学共同体的持续对话中逐渐确立的。事实上，即便在纯数学领域，错误的证明也并不罕见：Kempe在1879年对四色定理的「证明」被接受了11年才被发现有错误；Voevodsky（2002年Fields奖得主）曾公开表示自己发表的论文中有些证明后来被发现有缺陷，这促使他转向形式化数学。

而程序的形式化证明恰恰缺少这种社会过程。一份长达数百页、充满机械符号的程序正确性证明，几乎没有人愿意去阅读，更不用说去验证。它冗长、乏味、不具备数学证明那种可传播、可讨论的美感。因此，作者认为这种证明无法获得真正的信任。

规约本身可能是错的

另一个经典批评是：形式化验证只能证明「程序符合规约（specification）」，但无法保证「规约本身是正确的」。如果你对系统的形式化描述有误，那么再严谨的证明也只是在证明一个错误的东西。换句话说，验证并没有消除人为错误，只是把它从代码转移到了规约上。

这个问题在哲学上有着深刻的根源——它类似于维特根斯坦关于规则遵循的悖论：我们如何确保对规则的表述本身是无歧义的？在软件工程的语境下，这意味着无论我们的验证工具多么强大，「理解需求」这一本质困难始终无法被自动化。

历史上不乏规约错误导致灾难的案例。1996年阿丽亚娜5号火箭首飞爆炸，根本原因不是代码不符合规约，而是从阿丽亚娜4号继承的惯性导航软件的规约假设（关于水平速度的数值范围）在新火箭的飞行剖面下不再成立。软件忠实地执行了规约——在超出范围时抛出异常并关闭自身——但规约本身基于错误的环境假设。这正是DeMillo等人警告的问题的现实体现：形式化验证可以保证代码与规约的一致性，但无法保证规约与现实世界之间的一致性。

半个世纪后，形式化验证的现状如何

工具的成熟改变了游戏规则

文章及评论区的核心分歧在于：当年的批评在今天是否依然成立。反对者指出，1979年时形式化验证几乎完全依赖手工推导，而如今我们拥有 Coq、Isabelle、Lean、TLA+、Dafny 等强大的机器辅助证明工具。机器检查器（proof checker）承担了「阅读证明」的繁重工作，人类只需信任一个相对小而经过充分检验的验证内核。

现代定理证明器通常基于一个极小的「可信计算基」（Trusted Computing Base）设计。以 Coq 为例，它基于归纳构造演算（Calculus of Inductive Constructions），其核心类型检查器仅有数千行代码，所有证明最终都由这个小内核验证。归纳构造演算由Thierry Coquand和Gérard Huet在1980年代发展而来，其理论基础是Curry-Howard对应（也称命题即类型、证明即程序）：逻辑命题对应类型，证明对应程序，证明的验证对应类型检查。这意味着在Coq中，「证明一个定理」和「编写一个具有特定类型的程序」在数学上是同一件事。这个优美的对应关系使得程序验证和数学证明在统一的框架下进行。

Lean 4 由微软研究院开发，近年来因其在数学形式化（如 Mathlib 库，已包含超过 10 万个定理）中的广泛应用而备受关注。Isabelle 则采用 LCF 架构，通过 ML 类型系统保证只有经过核心推理规则验证的定理才能被构造。LCF架构由Robin Milner在1970年代于爱丁堡大学开发，其核心设计哲学是将定理表示为一种抽象数据类型，只有通过有限的几个核心推理规则才能构造新的定理值。这种设计借助ML类型系统的封装性，在架构层面保证了即使用户编写的策略（tactic）代码有bug，也不可能产生错误的定理。HOL Light的内核仅约400行OCaml代码，是目前最小的可信计算基之一。TLA+ 由 Leslie Lamport（2013年图灵奖得主）设计，专注于并发和分布式系统的规约与模型检查。

这在一定程度上回应了「社会过程」的批评——我们不再需要人类去逐行审阅证明，而是把信任转移到了经过社区长期验证的证明核心上。CompCert 编译器、seL4 微内核等真实工程案例，证明了大规模形式化验证在关键系统中是可行的。

里程碑式的工程验证案例

CompCert 是一个经过完全形式化验证的 C 编译器，由 Xavier Leroy 团队在法国 INRIA 开发，使用 Coq 证明了从 C 源代码到 PowerPC/ARM/x86 汇编的编译过程保持语义等价。这意味着如果源程序满足某个性质，编译后的目标代码也一定满足该性质——从根本上消除了编译器引入 bug 这一整类问题。在一项著名的对比研究（由 Yang et al. 使用 CSmith 随机程序生成器进行）中，研究者对多个 C 编译器进行模糊测试，发现 GCC 和 LLVM 都存在大量错误编译的情况，而 CompCert 的验证部分从未出现过此类问题。这项研究不仅验证了CompCert的可靠性，也深刻揭示了即便是最成熟的工业级编译器，其正确性也远没有人们想象的那样可靠。

seL4 是由澳大利亚 NICTA/Data61 团队开发的微内核操作系统，其完整的功能正确性证明耗费约 20 人年，证明代码量约为实现代码的 10 倍（约 20 万行证明对应 8700 行 C 代码）。seL4 的验证涵盖多个层次：从抽象规约到Haskell原型的精化（refinement），再从Haskell原型到最终C实现的精化，每一步都经过机器检验的证明保证语义保持。seL4 已被部署在军事无人机的通信系统、自动驾驶平台以及关键基础设施中，是形式化验证从学术走向工业的标志性案例。2020年起，seL4基金会在Linux基金会下运营，推动其在更广泛的工业场景中应用。

但根本性质疑并未消失

然而，支持原论文的一方认为，工具的进步并没有触及问题的本质。规约正确性的问题依然存在——你依然需要用某种语言描述「什么是正确」，而这个描述本身无法被验证。此外，形式化验证的成本依然高昂：seL4 微内核的验证花费了数十人年的工作量，这种投入对绝大多数软件项目而言是不现实的。

评论区有观点指出，现代软件的复杂度、外部依赖和快速迭代节奏，使得完整的形式化验证在工程上越来越不切实际。一个典型的现代 Web 应用可能依赖数百个第三方库、与多个外部服务交互、且每周甚至每天都在发布新版本——在这种环境下维护完整的形式化证明几乎是不可能的。形式化证明的一个核心挑战是「证明维护」：当代码变更时，相关证明往往也需要相应修改，而证明的修改工作量可能远超代码本身的修改。在seL4项目中，团队报告称有时对C代码的微小改动会导致数千行证明需要重构。真正被广泛采用的，反而是更轻量的形式化方法，比如类型系统、静态分析、模型检查和属性测试。

折中路线正在成为主流

有意思的是，这场争论的真正启示或许不在于「验证是否可行」，而在于「验证应该做到什么程度」。业界的实践趋势给出了一个务实的答案：

类型系统：Rust、Haskell 等语言用类型系统在编译期消除大量错误，本质上是一种轻量级的形式化保证。Rust 的所有权系统（Ownership System）和借用检查器（Borrow Checker）基于仿射类型和区域类型的理论，在编译期保证内存安全和数据竞争自由，无需运行时垃圾回收。微软研究表明其产品中约 70% 的安全漏洞属于内存安全问题，Google的Chrome团队也报告了类似的比例——Rust 的类型系统从设计上消除了这一整类缺陷。这是形式化方法「下放」到日常工程实践的典型案例：程序员无需编写显式证明，类型系统自动强制执行安全性质。从类型理论的角度看，越强大的类型系统能编码越多的程序性质——从简单的类型安全（Java、C#）到依赖类型（Idris、Agda）可以表达任意命题——但随之而来的是类型注解和编程复杂度的增加。Rust选择了一个精妙的平衡点：足够强大以保证内存安全，又不至于让日常编程变得过于繁琐。
模型检查（Model Checking）：TLA+ 等工具用于验证分布式系统的设计逻辑，Amazon 等公司已将其纳入工程流程。模型检查由 Edmund Clarke、Allen Emerson 和 Joseph Sifakis 发明，三人因此获得 2007 年图灵奖。与定理证明不同，模型检查通过穷举状态空间来自动验证系统性质——其最大优势是全自动，无需人类提供证明策略；但面临的最大挑战是状态空间爆炸问题：一个包含n个布尔变量的系统可能有2^n个状态，对于实际系统而言这个数字往往是天文数字。1980年代Ken McMillan发展的符号模型检查技术，使用二元决策图（BDD）紧凑表示巨大的状态集合，使得模型检查能处理10^120甚至更多状态的系统。Amazon Web Services 的工程团队自 2011 年起使用 TLA+ 验证 DynamoDB、S3、EBS 等核心服务的分布式协议设计，并公开报告称 TLA+ 帮助他们发现了多个仅通过传统测试难以捕获的微妙并发 bug——这些 bug 可能需要特定的事件时序组合才能触发，传统测试几乎不可能覆盖。Intel 在 1994 年 Pentium FDIV 浮点除法 bug 造成约 4.75 亿美元损失后，也大幅增加了对形式化方法的投入，现在其处理器设计流程中广泛使用模型检查和定理证明来验证浮点运算单元和缓存一致性协议。
属性测试（Property-based Testing）：介于测试与证明之间，用随机输入验证程序性质，兼顾成本与效果。最早由 Haskell 社区的 QuickCheck 工具推广（由Koen Claessen和John Hughes于2000年开发），现已扩展到几乎所有主流编程语言（如Python的Hypothesis、Rust的proptest、JavaScript的fast-check）。与传统单元测试手动指定输入输出不同，属性测试要求开发者描述程序应满足的通用性质（如「排序后的列表应保持元素不变」「加密后解密应得到原文」「序列化后反序列化应得到原对象」），然后自动生成大量随机输入验证这些性质。当测试失败时，QuickCheck风格的工具还会自动「缩减」（shrink）失败案例，找到触发bug的最小输入，大幅降低调试难度。虽然它无法提供数学证明级别的保证，但在实践中能以极低成本发现大量边界情况的 bug。从理论视角看，属性测试可以被视为对全称量化命题的概率性验证——它不能证明「对所有输入性质都成立」，但可以在统计意义上增加我们的信心。

这些方法并非追求「绝对正确」，而是在成本与可靠性之间寻找平衡点。DeMillo 等人当年反对的，其实是那种试图为整个程序提供完整数学证明的宏大理想，而这种理想在今天确实已被更务实的方法所取代。形式化方法的光谱非常宽广——从最轻量的类型检查到最重量的全程序验证，工程师可以根据系统的关键程度选择合适的位置。安全关键系统（SIL 4/DO-178C Level A）可能需要接近完全验证，而普通业务应用可能只需要良好的类型系统加上全面的测试覆盖。

对今天工程师的启示

这场跨越50年的争论提醒我们：软件正确性从来不是一个非黑即白的命题。形式化验证既不是万能的银弹，也不是毫无价值的学术玩具。它在航空航天（如 Airbus 的飞行控制软件使用 Astrée 静态分析器，该工具基于抽象解释理论，可以证明程序不存在运行时错误如除零、溢出等）、操作系统内核、加密协议（如 TLS 1.3 的 miTLS 实现经过 F* 语言验证，Project Everest 项目旨在提供完全验证的 HTTPS 栈）等高风险领域证明了自己的价值，但对大多数应用而言，成本收益比仍然不划算。

更重要的启示或许是：无论多么严格的验证，都无法替代对「我们究竟想要什么」的清晰思考。规约正确性问题的持久存在，恰恰说明工程的核心难题往往不在于「如何正确地构建」，而在于「构建什么才是正确的」——这正是 Fred Brooks 在《没有银弹》（1986年）中区分的「本质复杂度」与「偶然复杂度」：形式化验证能帮助我们消除偶然复杂度中的错误，却无法触及本质复杂度中的认知挑战。Brooks认为软件的本质困难在于概念结构的复杂性——规约、设计、需求理解——而非其表达形式的复杂性，后者可以通过更好的工具缓解，前者则是不可约减的。

半个世纪过去，这篇老论文的价值不在于它是否「预言正确」，而在于它逼迫每一代工程师去认真思考：我们对软件正确性的信任，究竟建立在什么之上。在 AI 辅助编程日益普及的今天，当代码生成越来越多地由机器完成，这个问题或许比以往任何时候都更加紧迫——我们是否需要新一代的形式化方法来验证 AI 生成的代码？

事实上，大语言模型与形式化验证的交叉正在成为活跃的研究方向。Google DeepMind的AlphaProof在2024年国际数学奥林匹克中展示了AI辅助定理证明的潜力，能够在Lean中自动发现和构造复杂的数学证明。Meta的研究团队也开发了基于LLM的自动定理证明系统。另一个方向是使用形式化方法验证AI系统本身——例如验证神经网络的鲁棒性（证明对输入的微小扰动不会改变输出分类）。然而，对于大型语言模型这样具有数千亿参数的系统，我们甚至难以写出有意义的形式化规约——「生成的代码应该是正确的」这个看似简单的要求，在形式化层面几乎无法精确表述。这正是DeMillo等人50年前指出的规约困境在新时代的回响。

这场始于1979年的对话，远未结束。