形式化验证的反驳，50年后重审

事件概述

随着 AI 编程工具的爆发，形式化验证（Formal Verification）这个曾经被视为“极少数场景才有用、甚至被认为不切实际”的领域，意外迎来了新热度。Google Trends 显示，近两年 “formal verification / formal methods” 的搜索量大幅上升。Lean 语言的学习者增多，新的规格语言不断涌现，甚至出现像 Signal Shot 这样试图端到端验证大型应用的项目。

在这一背景下，Ivan Gavran 在 2026 年发表文章，回顾了 1979 年 DeMillo、Lipton 和 Perlis 的经典论文《Social Processes and Proofs of Theorems and Programs》。那篇论文曾断言“程序验证注定失败”，并质疑其能否真正影响人们对程序的信心。Gavran 重新审视了其中的六个核心论点，逐一对照 2026 年的技术进展，看看哪些已被推翻，哪些依然成立。

关键技术点

原文论文的六个论点，以及 Gavran 的逐条评论，构成了文章的主体：

数学证明本质上是社会过程：证明不是终点，而是与同行交流的起点，真正让定理可信的是整个数学共同体的内化和应用。Gavran 认为这无可反驳，但程序验证并不需要完全复刻数学的过程。
规格说明存在根本性缺陷：自然语言的不精确需求转换为形式规格时，本身就是非形式化的过程，可能丢失信息。另外，规格若不能独立于实现，就容易“对齐”代码而不是对齐真实需求。Gavran 反驳说，规格比实现更接近人类直觉，现代规格语言（如 Quint）支持交互式探索边界情况。对于“规格独立性”问题，他认为现在有 AI 编码代理参与，人类作为最终仲裁者调整规格，反而更有优势。
全自动验证遥不可及：1979 年的作者认为全自动验证器几乎不可能出现。Gavran 承认完全自动化仍有距离，但 LLM 驱动的工具正快速缩小这个差距，并引用了 Igor Konnov 用 Lean 证明 Ben-Or 协议安全性的实验。
即使全自动验证可行，也可能有害：如果验证器只输出“已验证/未验证”，程序员可能不理解程序，也削弱其他防御手段的意义。Gavran 认为这建立在最坏假设上，是比较薄弱的论点。
真实系统太混乱，难以规格化：算法可以写出简洁规格，但真实系统规格常常临时、不稳定且混乱。Gavran 承认并非所有系统都需要验证，但随着软件进入关键基础设施和金融领域，风险升高；同时，若要相信 AI 编码代理能产出我们想要的东西，就必须能把“想要什么”尽量精确表达出来。
软件可靠性远不止验证：验证不是全部，系统还需要测试、监控、运维等。Gavran 认为这正是形式化验证需要与其他工程手段结合的原因，但不能因“验证不万能”而否定其价值。

对数据科学 / AI Agent 落地的意义

这篇文章对当前 AI Agent 落地有直接启发性：

AI 编码代理的可信度：AI 生成的代码往往超出人类逐行审查的能力，形式化验证提供了一种补救手段。文章指出，AI 代理让“理解代码”更难，但也让“验证代码”更快，这是一体两面的机遇。
规格说明的价值提升：让 AI 代理正确工作，前提是能清晰描述意图。形式化规格正好是“描述意图”的精确手段，即使不做完整验证，规格撰写的技能也会成为 AI 工程中的核心能力。
验证流程的人机分工：Gavran 强调，人类是最终仲裁者，规格变更只能由人来决定。这为“人类监督 + AI 生产代码 + 形式化工具辅助验证”的协作模式提供了依据。

我的技术点评

这篇“50年后重审”写得很有价值，不是因为它的结论有多么激进，而是因为它把经典异议放到今天的语境下逐条检验。原始的 1979 年论文其实并不反对所有形式化方法，只是反对“完全验证”作为普遍实践。Gavran 的梳理显示，六条反对意见中，有的依然有效（如规格转换的信息丢失），有的已经被技术演进削弱（如自动化的不可行性），有的则因 AI 代理的出现而改变了讨论框架。

最值得注意的是第二条和第五条。规格独立性的问题，在 AI 代理承担代码生成后反而迎刃而解——因为代理输出可验证的证明并不影响人类对规格的权威。而“系统太乱没法规格化”的问题，在 AI 时代变成了“你必须学会规格化，否则只能靠运气使用 AI”。这是一个反常识但合理的推论。

当然，Gavran 自己也承认，目前看到的只是早期兴趣迹象，形式化验证能否成为软件工程常规部分尚无定论。但至少，这篇文章提醒我们：旧争论并非过时，而是需要在新的技术条件下重新思考。对于关注 AI Agent 可信性和软件正确性的研究者，这值得一读。

原文链接

The Case Against Formal Verification, 50 Years Later - Ivan Gavran