Claude狂写1.8亿行证明，万亿次测试漏掉的Bug，被AI一锅端

全球软件中的缺陷，是否将被Claude彻底清除？

在短短48小时内，全球发生了27起重大网络攻击，如今人们纷纷传言，“最黑暗的十月”已经来临。

清晨，Anthropic前沿红队团队与Theorem Labs联合发布了一份重要报告——他们让Claude深入到底层汇编指令（RISC-V），对真实的生产级开源代码库发起了全面攻击。

在短短几周内，Claude成功拿下了123个开源代码库中的239个测试入口的形式化验证，生成了1.8亿行Rocq数学证明代码，并全部通过机器核验！

谷歌平台运行了上万亿次测试都未能发现的隐藏漏洞，连同潜伏超过十年的高危逻辑缺陷，甚至x86处理器硬件本身的真实错误，都在这次大规模清理中暴露无遗。

更令人惊讶的是，在一个流行的PDF阅读器中，Claude在一周内挖掘出的安全漏洞，直接相当于它通常一整年的报告量。

这次，Claude将查找Bug、修复Bug和验证修复连接成一个流程，展开了一场“数学级”的缺陷清除行动。

席卷全球的网络安全危机，或许真的有了解决之道。

万亿次测试遗漏的Bug

被数学方法逼出

过去十年，开源世界最依赖的防线之一，是谷歌在2016年推出的OSS-Fuzz。这种方法称为模糊测试，通过向程序入口批量输入半随机数据，观察哪些输入会导致程序崩溃。它累计运行了上万亿次测试。

但模糊测试本质上是在迷宫中碰运气。它的输入通常被限制在1MB以内，只要还有一条路径未被探索，那里的Bug就能一直隐藏。

研究团队这次将测试入口改写为一道数学命题：在设定条件下，小于64MiB的任意输入都不会触发约定的崩溃，包括断言失败和ASan内存检测工具能捕捉的错误。

Claude的任务就是证明这一点。一次运行成功不算数，规定范围内的每一种输入、每一条可能的路径，都必须被证明不会触发上述错误。

如果证明卡住，要么是Claude还未找到证法，要么是程序确实存在Bug。发现Bug后，Claude会自行打补丁，然后继续证明。

于是，那些躲在测试无法触及的角落里的Bug，终于现形了。

某个解压器中隐藏着一处计数器下溢，会将数据写入内存边界之外，但只有输入约20MB且排布极为罕见的数据才会触发。

研究团队表示，仅尝试证明的过程，就揪出了数百个Bug。

测试与证明之间的差距有多大？研究人员在Claude用Rust编写的Python解释器中故意埋了7个Bug。随机测试放过了其中5个，而证明则一个都没有放过。

运行391行代码，生成63万行证明

这批证明是在最底层完成的。

Claude证明的对象是编译后真正在CPU上运行的RISC-V机器码。源代码与编译出的程序可能不完全一致，只有验证到机器指令，证明的才是实际运行的程序。

为此，Theorem先将RISC-V指令和Linux进程的行为写成数学模型，目前的证明就建立在这套模型之上，限定在单线程、静态链接、固定内存预算的环境中。

验证到这一层，工作量开始爆炸。JSON解析库cJSON的一个解析入口仅有391行C代码，Claude却为其写了63万行Rocq证明。

膨胀上千倍的原因在于，证明需要覆盖整个进程。C程序的启动、内存分配器、printf、内存检测工具自身的运行时，都需一并证明，与cJSON本身相关的仅占十分之一。

整个项目中，Claude累计写了约10亿行证明，最终约1.8亿行通过检查。其中超过一半是由Claude为自己编写的工具自动生成的。

最后把关的是Rocq证明检查器，它按逻辑规则逐步验算，一份证明需要30分钟到几个小时的CPU时间。检查器确认的是证明符合规范，人类仍需审查规范和机器模型是否对应真实需求。

模型写得再流畅，若过不了检查器，就一行都不算数。写出如此规模的证明，在过去是难以想象的工程量。

传奇微内核seL4，编写代码仅用2人年，但为其完成形式化验证却花了整整20人年。因此，几十年来，这种级别的安全保证只有空客飞控等关乎人命的代码才用得起。

而这一次，123个开源库，Claude只用了几周。

Claude为芯片编写了一套数学

顺手揪出硬件Bug

要说Claude的证明能挖掘得多深，看看cpp-httplib就知道了。

为了排除递归过深、撑爆栈内存的可能性，Claude追进了C++标准库libc++的红黑树，在机器码上证明这棵树的高度始终被限制在对数级别。树的高度受控，销毁时的递归层数才有上限，才能继续证明栈空间不会被耗尽。

它先将zlib压缩格式的标准写成形式化规范，再证明Linux内核自带的zlib实现完全符合该规范。

这次，证明是在x86机器码上完成的。而x86指令集的数学模型是由Claude完全自主编写的。

这套模型精准到何种程度？在模型中一条指令一条指令地单步推演，能在Linux内核上完整启动Ubuntu的用户态。

在编写模型的过程中，Claude发现了x86官方参考文档中的数百处错误，还找出了少量隐藏在CPU硬件本身的Bug。

从软件一路验证到芯片，AI已经在帮助人类重新核对整台计算机的基础。

证明速度每两个月翻一番

1.34亿美元的验证路线图

形式化验证最大的门槛是成本高昂，一份证明往往需要消耗数亿token。如今，这笔费用正在快速下降。

Anthropic用36个小型验证任务进行了测试，Opus 5.5完成其中一半所需的token，比Opus 5少了约40%。

Theorem测试了今年5月至9月发布的7款前沿模型，验证速度大约每两个月翻一番。

而且，证明可以复用。

Agent们共享工作区后，同一组任务少花费了17%的token。libcups、freerdp、libzmq这几个看似无关的项目，共用了运行库等底层代码，因此大段证明都是从已验证的部分复制过来，稍作修改即可使用。

顺着这个思路，Theorem以Nix软件生态为样本计算了一笔总账。

在Nix软件生态中，只需9MB的共享基础库，就能覆盖三分之二机器码的全部依赖。仅OpenSSL一个库，就出现在近1.6万个软件包的运行依赖中。

按当前价格，将OpenSSL完整验证一次约需22万美元，摊到每个下游软件包，仅约14美元。

Theorem推算，如果验证能力保持每两个月翻倍，并按每年1亿美元的预算推进，到2027年底，总成本约1.34亿美元，就有望将Nix生态95%的机器码纳入证明。

作为对比，GovAI估计，全球网络犯罪相关损失、应对和防御支出，每年合计约5000亿美元。

全球网安至暗48小时，让数学来兜底

Linux内核是全球测试最严格的软件之一，9月的一份Debian内核安全公告就列出了1000多个漏洞。前沿大模型已能将几个看似无害的小Bug串联成一条致命的攻击链。

寻找Bug的AI越来越强，依靠人类逐个打补丁已无法跟上其速度。

论文作者之一Aengus Lynch写道，“对互联网来说，这是一段可怕的日子。我相信，这是一束希望之光。”

他还相信，终有一天，Theorem会将所有关键软件都进行形式化验证。

现在，首批25个库、60个入口的证明已在GitHub公开，任何人都能下载并亲手验算。

编写代码的机器越来越多，人类也正在走通一条路，让支撑数字世界的关键代码都附上一份数学证明。

参考资料：

https://x.com/AnthropicAI/status/2113390212911083894?s=20

本文来自微信公众号“新智元”，作者：ASI启示录，编辑：摩西 桃子，36氪经授权发布。