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

新智元报道

全球软件的bug，要被Claude端掉了？

短短48小时，全球就爆了27起重大网络攻击，现在人们都在疯传，「最暗十月」来了。

一早，Anthropic前沿红队团队联手Theorem Labs发布了一份重量级报告——

他们让Claude深入到底层汇编指令（RISC-V），向真实的生产级开源代码库发起总攻。

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

谷歌平台跑了上万亿次都没撞出来的隐秘漏洞，连同潜伏十余年的高危逻辑死角，甚至x86处理器硬件本身的真实缺陷，在这场大清剿中悉数现形。

更夸张的是，在一个热门的PDF阅读器中，Claude一周挖出的安全漏洞，直接顶得上它通常一整年的报告量。

这一次，Claude把找Bug、修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

编辑：摩西 桃子