# 50 年后再看《反对形式化验证》：AI 写代码时代，老论点还站得住吗？

> 原标题：The Case Against Formal Verification, 50 Years Later

- 来源：Hacker News 首页
- 发布时间：2026-08-16T20:38:58.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/51054
- 原文：https://ivan-gavran.github.io/0-social-processes-paper

## 摘要

Ivan Gavran 翻出一篇 1979 年的老论文，那篇论文当年断言程序的形式化验证注定失败。他对照今天 AI 写代码的现状，一条条重新审视。原文说全自动验证器不太可能实现，但现在大模型驱动的工具正在补上这个缺口，比如 Igor Konnov 已经在 Lean 里证明了 Ben-Or 协议的安全性。关于“规格说明会被实现污染”的担忧，现在反而倒过来...

## 推荐理由

这篇博客没在推销什么，就是翻出一篇 1979 年的老论文，拿今天的 AI 编程和自动验证工具一条条对答案。原文说全自动验证器不太可能实现，但现在大模型驱动的工具确实在补这个缺，比如正文里提到的 Lean 证明案例。关于“规格说明会被实现污染”的旧担忧，现在反而倒过来了——AI 写的代码逼着人先把规格说清楚。文章有历史纵深、有具体案例，不是公关稿。因为是个人博客，权威性上我会打个折，但观点和切入角度够硬，对做工程和做工具的人都实用。

## 锐评

Ivan Gavran 这篇博文不是在喊“形式化验证赢了”，而是做了一次冷静的对照检查。他拿1979年那篇经典反对论文里的三条核心论点，一条条放到2026年AI辅助编程的背景下看还成不成立。

第一条说数学证明本质上是社会过程，博文直接认了，说这没错，但这不是反对验证本身的理由。第二条关于规格说明的担忧更有意思。老论文说规格说明和实现会互相污染，Gavran 反而觉得现在有了AI代理写代码，人类作为“什么算正确”的最终裁判，角色反而更清晰了——AI可以改代码、出证明，但规格说明的修改必须由人来拍板。第三条说全自动验证器不太可能实现，现在大模型驱动的工具正在补这个缺口，文中举了 Igor Konnov 在 Lean 里证明 Ben-Or 协议安全性的例子。

不过 Gavran 也承认，老论文里说“现实世界乱糟糟的系统经常不值得验证”这一点至今成立。他的整体判断很克制：搜索热度确实在飙升，但主流采用还没到。这篇博文的价值在于把一场持续了五十年的争论拉回地面，不吹不黑，信息量刚好。