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

　　编辑：摩西桃子