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

The Case Against Formal Verification, 50 Years Later

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

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