形式验证赢了吗，1979年那篇论文说的不算！
2026年8月，软件工程师们正在疯狂学习一门叫Lean的编程语言，谷歌趋势显示过去两年“形式验证”和“形式方法”的搜索量出现巨大飙升，各大AI实验室纷纷发布能自动生成证明的模型，Mistral AI推出了Leanstral，AxDafny在DafnyBench基准上跑出92.7%的验证成功率，OpenAI的下一代模型Astra则在10个悬而未决的数学难题上取得突破，每个结果都附带了Lean 4证明证书！
形式验证——这个被嘲笑了五十年的软件正确性保证手段——似乎终于熬出头了，但事情真的这么简单吗！
1979年，三位计算机科学家在《ACM通讯》上发了一篇题为《社会过程与定理及程序的证明》的论文，他们在文中说了一句在今天听来简直狂妄的话：“程序验证注定失败，我们看不出它怎么能影响任何人对程序的信心。”
五十年过去了，说这话的人有的已经离世，形式验证不仅没死，反而活成了他们最想不到的样子，可那些老论点真就全过时了吗，还是说它们依然戳在验证社区的痛处上！
数学证明不是终点而是起点
1979年的论文抛出的第一个论点其实挺聪明，作者说：别把程序验证想象成“写完证明就完事了”，就算在数学界，一个定理被证明出来也不过是第一步；真正让一个数学结论“可信”的，是后续整个社会过程——其他数学家消化这个证明，把它和其他数学分支连接起来，拿它去解释物理现象；这一整套流程，才是数学知识被接受的真正机制。
这个观察在今天依然成立，2026年8月1日，OpenAI宣布Astra模型在10个数学问题上取得突破，每个结果都附带Lean 4证明证书，但问题接踵而至：谁来检查这些证明，谁来确认证书没有造假，谁来把这些结果嵌入已有的数学知识体系！
Lean的创造者Leonardo de Moura给出过一个非常漂亮的回答，他说：你不需要信任整个Lean——那是个庞大的程序，功能不断增加，没人能给出完整的规格说明；你只需要信任它的内核，这个内核大约只有5000行代码，小到任何人都能自己从头写一个；而且已经有人用Lean本身写了一个叫Lean4Lean的内核，证明了它相对于Lean语义的正确性，还有人用Rust和其他编程语言实现了独立内核。
你看，这就是把“社会过程”压缩到了一个极小的、可验证的范围内：你不需要信任一个庞大的系统，不需要依赖某个权威机构来“认证”你的证明，你只需要信任这5000行代码——或者更准确地说，你只需要信任“多个独立实现都指向同一个结果”这个事实，这不恰恰是论文作者想要的“社会过程”吗，只不过这个“社会”现在包括了机器！
规格说明永远无法完全描述你想要的东西
论文的第二个论点更狠，他们说：现实世界的需求是模糊的、非正式的，一群人有共同的理解，但这种理解没法精确写下来；把这个模糊的需求翻译成形式化规格说明，这个过程本身就是非形式化的、未经验证的；在这个翻译过程中，大量信息会丢失或被误解，这个论点至今无人能驳倒。
2026年，我们有了更先进的规格说明语言比如Quint，可以交互式地检查规格说明的所有边界情况，但翻译问题依然存在：你写下一行形式化逻辑，它和你脑子里那个“我想要的东西”之间，永远隔着一层解释的迷雾。
更麻烦的是论文作者的第二个子论点：规格说明只有独立于实现才有价值，但在软件开发的迭代过程中，规格说明和实现会互相影响、互相“污染”；到最后，你只是在让规格说明和实现保持一致——如果两者都犯了同样的错误呢！
de Moura在播客里说了一句话：“我已经不再写测试了，我写性质，然后AI替我证明。”这句话背后藏着一个深刻的变化：过去，规格说明是写给人类看的——用来沟通、用来对齐理解；现在，规格说明越来越多地是写给AI看的——用来告诉AI“你要生成什么”。
这反而让规格说明的“翻译问题”变得更尖锐了：如果你连和人类同事对齐需求都费劲，你怎么保证你写给AI的规格说明就是你真的想要的！
全自动验证的坑正被AI疯狂填平
1979年的论文作者说：全自动验证器极不可能被造出来，五十年后回头看，这个判断既对又错。
说它对，是因为到今天为止，真正意义上的“全自动”——你扔一段代码进去，机器二话不说告诉你“对”或“错”——依然不存在；人类 effort 仍然是验证过程中不可或缺的部分，你要么得亲自写证明，要么得构建一个适合模型检查的抽象模型。
说它错，是因为AI正在以前所未有的速度填这个坑，2026年6月，研究者发布了AxDafny——一个基于大语言模型的智能体框架，能够迭代生成Dafny代码实现、不变式、断言和终止论证；在DafnyBench基准上，AxDafny验证了725/782个实例，成功率92.7%，比此前最强的证明提示基线高出6.5个百分点。
同一时期，OpenProver系统将大语言模型驱动的自动定理证明与Lean 4形式验证整合在一起，Mistral AI发布了Leanstral——一个专门为Lean 4设计的开源AI智能体；2026年8月1日，OpenAI的Astra模型不仅在10个数学问题上取得突破，而且每个结果都附带了Lean 4证明证书，发布在GitHub上，“任何人用一台笔记本电脑就能独立验证”。
注意这句话：“任何人用一台笔记本电脑就能独立验证”——这就是AI正在做的事情：它不是在取代人类验证者，它是在把验证的成本降到几乎为零；过去需要一个数学家花几个月才能检查的证明，现在一台笔记本电脑几分钟就能跑完。
验证通过就万事大吉是最危险的假设
论文的第四个论点可能是最被低估的，作者说：就算全自动验证真的实现了，一个只会回答“验证通过”或“验证失败”的机器，对程序员理解程序毫无帮助；更危险的是——一旦程序被“验证”了，程序员可能就不再做其他层级的防御了，比如监控、限流之类的手段，这个论点在今天看来尤其刺眼。
Lean的de Moura在解释验证原理时举了一个非常具体的例子：想象程序里有一个数组，10个格子，编号0到9；程序用一个叫i的变量来记录“取第几个格子”；如果i变成了10或者更大，程序就去取一个不存在的格子——这就是越界访问。
在C语言里，编译器不会拦你，只有程序跑到那一行的时候才会出事；在Lean中，你可以写一条数学语句，声明“索引变量i的值大于等于0且小于10”，Lean会要求你证明这条语句为真，证明不了，代码就过不了检查。
这听起来很美好，但问题来了：如果Lean告诉你“验证通过”，你是不是就可以省掉所有的运行时检查、所有的监控、所有的防御性编程！
2026年，软件正在进入关键基础设施和金融世界， stakes 越来越高；一个被“验证”过的程序如果因为规格说明写错了而出事——谁来负责！Lean的内核可以验证你的证明是否正确，但它验证不了你的规格说明是否反映了真实世界的需求。
de Moura自己也承认这一点，他说验证过程就像在源代码上方叠加了一层“第二个软件层”，专门用来描述和验证程序的行为；但这层软件本身也是人写的，人的错误永远在循环里。
真实世界太乱验证不了但世界在变
论文第五个论点说：算法可以有整洁的规格说明，但真实世界系统——那些跟硬件交互、跟网络通信、跟用户行为打交道的系统——规格说明是临时拼凑的、不稳定的、一团乱麻，这个论点在今天依然成立：你试试给一个电商网站写一份完整的形式化规格说明，试试给微信写一份！
但有两件事变了，第一，软件正在进入那些“非验证不可”的领域：CERN在用形式验证做粒子加速器设施的安全关键系统，牛津大学的研究者在做CHERIoT-Ibex处理器的形式验证；这些系统出错的代价不是“用户骂两句”，而是设备损坏、数据丢失、甚至人身伤害。
第二，AI编码智能体正在改变游戏规则：如果你希望一个AI智能体写出你想要的代码，你最好能精确地描述你想要什么；这不一定要用形式化规格说明——但精确描述意图这件事，本身就越来越重要了。
AxDafny的研究者做了一个非常聪明的对比实验：他们把验证通过的程序编译成Python，在原始测试框架下运行；结果发现，大部分执行失败不是因为程序逻辑错了，而是因为资源限制——Dafny的规格说明保证的是功能正确性，而不是渐进复杂度。
换句话说：验证通过的程序，跑起来可能超时，验证解决不了一切问题。
验证只是可靠性拼图中的一块
论文最后一个论点，可能是唯一一个作者和今天的验证社区能达成共识的，作者写道：“让程序正确的愿望是建设性的、有价值的；但验证的单一视角忽视了其他方面的价值——接受类似数学证明的正确性标准、或类似真实工程结构的可靠性标准；在经济限制内追求可工作性、通过复用成功设计来引导创新、信任同行社区的功能——所有让工程和数学真正起作用的机制，都在对完美可验证性的徒劳寻找中被遮蔽了。”
这段话写于1979年，2026年读起来依然精准：形式验证不是魔法棒，它不能解决需求模糊的问题，不能替代代码审查，不能取代测试——de Moura引用了Dijkstra那句经典的话：“程序测试可以用来表明存在bug，但永远不能证明bug不存在。”但这句话的另一面是：测试依然能找到验证找不到的问题——比如性能问题，比如用户体验问题。
AxDafny在DafnyBench上验证了92.7%的实例，但剩下那7.3%呢，为什么验证不了，是规格说明写错了，还是AI生成的证明有漏洞，还是验证器本身有bug，没人知道，这事悬着呢。
一个还没完的实验
2026年8月1日，OpenAI发布Astra模型的Lean 4证明证书时做了一件非常有意思的事：他们把证书放在了GitHub上，声明“任何人用一台笔记本电脑就能独立验证”。
但问题来了：谁来验证“验证者”！
Lean的内核只有5000行代码，理论上小到任何人都能自己写一个；Mario Carneiro用Lean本身写了一个Lean4Lean内核，证明了它相对于Lean语义的正确性，还有人用Rust实现了独立内核，多个独立内核——这是确保结果正确的最好方式。
但“多个独立内核”这个策略本身，依赖的是什么，依赖的是有人愿意花时间去写第二个、第三个内核，依赖的是社区对这些内核的持续审查和维护，依赖的是——回到论文的第一个论点——一个社会过程。
2026年，形式验证的工具前所未有的强大，AI让证明生成前所未有的快，但那个根本问题依然悬在那里：谁来检查检查者，谁来证明证明者的正确性！
Lean的de Moura说“我写性质，然后AI替我证明”，但谁检查性质本身对不对——这个问题，1979年的论文作者问过，2026年，我们还是没有完美答案，而下一个实验已经在路上了。