一个被学界判了近五十年"缓刑"的技术方向,最近突然热起来了。Google Trends 上"formal verification"的搜索曲线在最近两年明显翘头,学 Lean 的人变多,新的规范语言接连冒出来,甚至有团队在做端到端验证真实生产系统——Signal Shot 项目从今年4月20日启动,目标是用 Lean 证明 Signal 协议本身及其 Rust 实现的正确性。这不是玩具项目,是拿一款几亿人在用的加密通讯软件当靶子。
反常的地方在于,这波热闹的源头能一路追到1979年一篇论文,而那篇论文的结论恰恰是"形式化验证注定失败"。DeMillo、Lipton、Perlis 三人合写的《Social Processes and Proofs of Theorems and Programs》里说得很直接:程序验证没办法像数学证明那样,通过同行反复检验建立起真正的信任,这条路走不通。五十年后,AI 编程逼着人们重新翻出这份判决书。
一份1979年的判决书,四条罪状
这篇论文的论证不是笼统反对"证明程序",而是给出了几条具体理由。
论点一:程序证明想模仿数学证明,但数学证明本身也不是"证完就完事"——真正让人信一个定理的,是同行反复检验、和其他分支互相印证的社会过程,程序证明缺这个过程。
论点二:把模糊的现实需求翻译成形式化规范,这个翻译步骤本身是不可验证的,出错概率不低;更麻烦的是,规范和实现在迭代开发里很难保持独立,写着写着两者就互相污染,你以为在验证,其实只是在自我印证。
论点三:全自动验证器基本造不出来,人力投入省不掉。
论点四:就算造出来了,一个只会吐"VERIFIED / NOT VERIFIED"的黑箱,反而会让程序员失去对系统的理解,也会削弱人们做监控、限流这些额外防线的动力。
四条里,前一条基本不算真反对——程序证明本来就不需要照搬数学的社会过程,这是打了个稻草人。真正致命的是二、三、四。
AI 到底改写了哪一条
先说没变的:论点二关于"翻译不可验证"这半段,AI 没有解决,只是给了更好的工具——像 Quint 这样的规范语言,能交互式跑一遍规范的边界情况,帮你更早发现"这规范其实不是你想要的那个意思"。但这终究是辅助排查,不是消灭了这个风险。
真正被改写的,是"规范与实现难以独立"那半段。以前的逻辑是:开发迭代快,规范和代码互相迁就,越写越像左手证右手。有了编码代理之后,分工反而清楚了——代理负责写代码、写证明,人负责改规范。规范要不要动,永远是人拍板。这个角色分离本身,就在回应当年那个"互相污染"的老指控:污染的前提是规范和实现的修改权混在一起,现在这条边界被重新划清了。
论点三这条正在被快速啃,但还没啃完。人力投入在下降是真的——用 LLM 辅助生成证明、辅助建模,已经有具体案例:有人记录了用 AI 辅助在 Lean 里证明 Ben-Or 协议安全性的过程,速度明显快于纯手工。但"辅助生成证明"和"全自动验证器"之间,还隔着一段真实的距离,这道题只做对了一半。
论点四依然是最弱的一条,靠的是"验证器一上线大家就会放松警惕"这种最坏假设,既没有实证支持,也不太符合工程团队的真实行为模式。
乐观叙事和没解决的硬骨头
Signal Shot 这类项目愿意在生产级协议上砸资源,背后的口径很清楚:AI 让写证明的成本降下来了,而 AI 写代码的速度又让"能不能机器验证正确性"变得更迫切——一个降门槛,一个提需求,两头一起把形式化验证往前推。这个成本论确实站得住,写证明确实比五年前容易了。
但成本论解决不了那个更根本的问题:规范本身可能就是错的。你验证得再严丝合缝,验证的也只是"代码符合规范",而不是"规范符合你真正想要的东西"。这条线,恰恰是1979年那篇论文论点二里最结实的部分,今天依然悬着。
- 风险.验证通过只能证明"代码没有偏离规范",不能证明"规范本身没有理解错需求"——这道题AI目前帮不上太多忙。
半局已下,尚未言胜。
孔子说"名不正则言不顺",放在这里也合适:形式化验证这波热闹里,很多人把"AI降低了证明门槛"偷换成了"验证问题已经解决",名实不副,判断就容易走偏。Signal Shot 这类项目值得盯,但它现在是一个早期信号,不是一个已经兑现的答案——真正决定这股热潮能不能撑住的,是全自动验证器能不能真正落地,以及有没有更多主流商业软件愿意跟进做端到端验证。这两件事,目前都还看不清。