当 AI 开始用数学证明代码：Anthropic 与 Theorem 如何改写软件零缺陷的工业账本

要怎么保证一段程序在任何情况下绝对不死机？

跑几万亿次测试够不够？

不够。

谷歌给全球上百个核心开源软件做自动化测试，每天灌入天文数字的随机畸形数据。

跑了整整好几年，代码里依然不断被揪出内存破坏和崩溃漏洞。

因为测试跑得再多，也只能说明你试过的输入没出事。

它永远回答不了一个问题：万一某个极端情况你没测到呢？

在计算机科学里，能彻底解决这个问题的，只有形式化验证。

它不用随机数据去撞大运。

它把代码当成数学题，用严格的符号逻辑，一步步推导出程序在任何合法输入下都不可能崩溃。

听起来很完美。

但在过去几十年里，它几乎只活在航天飞机、核电站控制和绝密军工里。

原因只有一个：太贵了，贵到人类根本写不起。

世界上最著名的一个高安全微内核叫 seL4，核心代码也就一万行 C 语言。

为了给这一万行代码写出完整的数学证明，顶尖计算机科学家团队硬生生耗费了整整二十个人年。

二十年顶尖专家的工时，才换来一万行代码的安全保证。

现实里的开源基础库动不动几十万行，没人耗得起这种成本。

绝大多数工程师只能接受现实：只要代码还在跑，里面就一定有漏洞。

但事情最近起了变化。

Anthropic 联手专门做形式化验证的机构 Theorem，把这道世纪难题扔给了 Claude。

在几个星期的时间里，Claude 写出了大约一亿八千万行形式化证明代码。

它一口气覆盖了 123 个主流开源代码库，拿下 239 个关键入口。

在 RISC-V 汇编和 Linux 进程这个最底层的执行级别上，直接给出了严密的数学保证：

只要输入数据在 64 MB 以内，这些程序在单线程静态运行中，绝对不会发生任何内存越界、断言失败或者意外崩溃。

一亿八千万行？

写过代码的人听到这里，第一反应肯定是怀疑。

大语言模型经常胡说八道，它写出来的一亿多行证明，谁敢信？

谁又能一行一行去肉眼审查？

这恰恰是整个机制最巧妙的地方。

根本不需要人类去审查。

Claude 写的是专门用于数学验证的 Rocq 形式化证明语言。

在形式化证明的世界里，有一个铁面无私的独立裁判：证明内核。

这个内核的代码非常精简，只认最纯粹的逻辑推理公理。

AI 可以在前面天马行空地写推导，但所有的证明最终都要送进这个内核编译。

只要推导里有一丝逻辑跳跃、断层或者幻觉，内核立刻报错拦截。

只要内核顺利通过编译，在数学上这就叫已证明定理，铁证如山。

也就是说，AI 依然可能产生幻觉，但数学验证器拥有绝对的否决权。

更绝的是写证明的过程。

数学证明不是做选择题。

如果程序本身就带着漏洞，逻辑链条在数学上是无论如何都闭合不上的。

Claude 在推导过程中，经常遇到怎么写都证明不了的死胡同。

退回去一查，证明思路并没有错，是被测的开源代码里真有潜伏很深的缺陷。

靠着这种数学推导的倒逼，Claude 在这批被全世界测过无数遍的开源库里，硬生生挖出了几百个隐藏极深的深层缺陷。

它把发现的漏洞标了出来，顺手打了补丁，然后接着把剩下的数学证明推导完毕。

那这是不是意味着，以后所有软件都可以一劳永逸了？

现实的工程限制依然摆在眼前。

最直接的门槛是算力消耗。

机器推导数学证明极其耗费资源，某些复杂一点的底层程序，光验证一个入口就吃掉了一亿多个标记。

另一个限制是应用场景。

这次的数学证明是在明确边界下成立的：RISC-V 架构、Linux 静态二进制、单线程，外加 64 MB 的输入大小。

真要面对现实生产环境里错综复杂的多线程并发和网络环境，状态空间会以天文数字膨胀。

但它彻底改写了一笔算了几十年的经济账。

以前给一万行代码做证明，要搭进去二十个人年，把形式化验证变成了只有航天和密码学才用得起的奢侈品。

现在的模式是：人类定义好安全规约，大模型在几周内批量生成上亿行数学逻辑，再由一个极小的验证器一秒敲定。

天价的顶尖人力，变成了可预测、可扩展的算力开销。

当写数学证明的边际成本不断被压低，我们用了几十年的软件开发规则，正在从靠测试碰运气，慢慢走向拿数学做保证。