AI 让形式化验证重回主流：50 年前的反对理由还成立吗

形式化方法工程师 Ivan Gavran 在文章 The Case Against Formal Verification, 50 Years Later 中，重新审视了 1979 年经典论文《Social Processes and Proofs of Theorems and Programs》。当年的作者认为，程序验证无法像数学证明那样自动建立社会信任；近半个世纪后，AI 编程让其中一些成本判断发生变化，但最难的问题仍然留在原地。

一句话结论：AI 可以更快地写证明、修证明，却不能替人决定软件“应该做什么”；形式化验证真正复兴的前提不是自动出现一个绿色对勾，而是把人的意图变成可审查规格。

1979 年论文的核心反对意见不是“数学没用”。它质疑的是一种完整验证幻想：现实需求本来是非正式的，把它翻译成规格本身就可能出错；规格与实现很难真正独立；真实系统持续变化，无法像小算法那样被整齐描述；即使机器宣布验证通过，团队也未必理解系统。

这些批评到今天仍然成立。一个支付系统可以被证明严格执行了规格，但如果规格漏掉退款、汇率或权限边界，证明只会更可靠地执行错误要求。监控、限流、故障恢复、代码评审和同行信任也不会因为 Lean 文件通过编译而消失。

AI 改变的是经济账。Agent 生成代码越快，人越难逐行建立理解，正确性验证就越容易成为交付瓶颈。反过来，模型也能根据编译器和证明器返回的确定错误持续修改候选方案。与“测试失败了，但不知道是否覆盖关键路径”相比，形式规格能给 Agent 一个更明确的闭环。

这并不意味着形式化验证已经进入普通团队的默认工作流。原文也承认，目前看到的只是 Lean 学习、规格语言和端到端验证项目增加等早期信号。更现实的路径是部分采用：先证明协议状态机、权限不变量、资金守恒或并发安全等高风险性质，而不是试图为整个业务世界写一份完美公理。

关键事实

• 讨论对象：1979 年《Social Processes and Proofs of Theorems and Programs》
• 原始批评：规格翻译、社会信任、自动化、真实系统复杂度和完整可靠性
• 新变量：AI Agent 同时扩大了代码理解缺口，也降低了生成和修复证明的成本
• 证据边界：这是一篇工程分析，不是形式化验证已普及的市场统计

OC 判断

先别急着宣布形式化验证赢了。AI 确实让证明器更容易被使用，但也让“规格由谁批准”变得更重要。可以把实现和证明交给 Agent，不能把正确性的定义也一起外包。最有价值的变化，是团队开始把关键不变量写成机器可检查的工程资产。

为什么重要

• 对开发者：验证工具可能从专业岗位工具变成 Agent 工作流中的自动反馈器。
• 对团队：规格评审会比逐行审查 AI 生成代码更重要，但不会更省思考。
• 对企业：应优先验证损失高、边界稳定的性质，而不是追求“全部已证明”的标签。

参考来源

• The Case Against Formal Verification, 50 Years Later