偶买噶，1.8亿行证明啊，Claude几周就写完，还一口气挖出数百个bug！
就在今天，Anthropic官方发文：他们的「前沿红队」（Frontier Red Team）联手一家专做软件安全证明的公司Theorem，发布了一项新研究。
Claude用了几周时间，给123个开源软件库的239个测试入口，写出了约1.8亿行证明 来验证软件的安全。
写证明的过程中，Claude还顺手找到了数百个bug。
其中一些bug，按Anthropic的说法，躲过了数万亿次测试，藏了很多年。
Anthropic表示，这是第一次大规模用AI在汇编层面，对真实的生产软件做形式化验证。
以前要顶级专家团队熬好几年才干得完的活，这回被Claude做成了流水线。
◽以前专家熬20年的活，Claude几周写完证明
先说软件圈平时怎么找bug。
最常用的办法叫模糊测试：往程序里灌海量随机数据，看哪一条能把它弄崩溃，就好比有一栋楼，然后派一大群人进楼里乱跑乱跳，看哪里会塌。
Google的OSS-Fuzz平台就是常年给上千个开源项目做模糊测试。
这办法很好用，但有个死穴：输入无穷无尽。
今天灌了一百万条没出事，明天第一百万零一条照样可能出事。
它永远只能说“我试过的都没事”，说不了“所有输入都没事”。
另一种办法叫形式化验证。
还是这栋楼，不进去跳，也不靠运气。而是请结构工程师拿图纸算：每根梁多粗、压多少重量、会不会把旁边的柱子压垮。
一根一根算完，最后说出一句话：按这张图纸施工，这栋楼不会塌。
这个“拿图纸一步步算完”的过程，就是形式化验证。
放到程序上，要验证的问题就是把“这个程序对任何数据都不触发这类 bug”写成一道数学命题，再一步一步严格证明。
一旦证明成立，就不用再一条条去试了。因为它覆盖的是全部可能性，不是抽样的结果。
问题是，它太贵了。
Anthropic 举了个例子：seL4 操作系统内核，写代码花了 2 人年，形式化验证却花了 20 人年。
所以过去几十年，这种办法基本只用在空客航电这类出了事就要命的代码上。
这一次，Claude 换了个思路。
题目不用自己出了。 开发者在 OSS-Fuzz 上写好的测试入口，标准就是“程序一旦出问题，就说明有 bug”；“这个入口收到任何数据都不会出问题”直接就是现成命题。
不算图纸，该算盖起来的楼。 代码要过编译器，会改写、会优化，图纸和实物不完全一样。
所以团队把库和测试编译成 RISC-V（一种芯片指令集）机器码，再用 Theorem 的芯片和系统模型生成命题。
剩下的交给 Claude 写证明，写完由检查器 Rocq 逐行核对，错一步都通不过。
规模是这样的：一份证明通常就有 60 万行，对应的程序中位数只有约 1.8 万条机器指令。
123 个库、239 个入口加起来，约 1.8 亿行。
这么多证明，人根本看不过来，好在也不需要人看。
开发者只需要信任三样东西：芯片和 Linux 的形式模型、命题本身的写法，以及 Rocq 检查器。
剩下的 1.8 亿行，全由机器把关。
可问题来了：要是证着证着，证不下去了呢？
◽证明卡住的地方，正好藏着 bug
答案很简单：证不通的地方，往往就藏着真 bug。
有些程序本身就有漏洞，“不会出错”这个命题根本不成立，Claude 自然也证不出来。
团队干脆放手让 Claude 自己处理：发现 bug，自己打补丁，再重新生成命题，接着往下证。
就这样，Claude 一路挖出了数百个 bug。
而且不少是模糊测试几乎不可能撞上的。
模糊测试工具塞进程序的数据，通常不超过 1MB。
Claude 证明的范围，却覆盖到了 64MB。
于是，下面这些 bug 被挖了出来：
一个解压器的计数器会下溢，导致内存越界写，但只有输入约 20MB、结构还特别刁钻时才会触发。
一个图像解码器的越界读，需要 64MB 的输入，外加 2GB 以上的内存。
Claude 还重新发现了 libexpat 的已知漏洞 CVE-2026-56132，要深层嵌套的输入才能触发。
还有的 bug 根本不会让程序崩溃。
在证明某个库内存安全时，Claude 注意到，它有一个“限制应用能加载哪些文件”的功能，并不是每次都生效。
当然，让 AI 自己改代码，也有被它钻空子的风险。
Claude 理论上可以把程序改成“什么都不干”，这样就永远不会出错，证明也能轻松通过。
团队的应对是：每打一个补丁就扣分；能证明补丁只影响了极少数输入，才给加分。 所有补丁也都记录在案，逐一审计。
除了这 123 个库，Anthropic 还用同样的思路做了几个别的实验。
其中一个是验证一款常用的 PDF 阅读器，一周找到的安全 bug，相当于这个软件平时一年收到的报告量。
还有一个，在一款常用的关键应用里，挖出了一个潜伏十年以上、此前从没人发现的逻辑 bug。
◽Claude 写证明越来越便宜，但证明过不等于零 bug
1.8 亿行证明，听着就贵。
Anthropic 也承认，一套证明可能要花掉上亿 token，这是目前最大的瓶颈。
不过，账在变好看。
团队用真实的 OSS-Fuzz 代码搭了 36 个小型验证任务，Opus 5.5 证完其中一半，比 Opus 5 少用了约 40% 的 token。
而且证明还能“抄作业”。
不同程序的证明里，有大量重复的部分，比如 C 运行时、内存检查工具的初始化。让多个 agent 共享工作区、互相复用证明，token 又能再省 17%，有些单独证不出来的任务也证出来了。
现在，Theorem 已经公开了一部分证明，还发布了一个 Claude skill，帮开发者上手验证自己的代码。
它同时开放了 OSS Verify：符合条件的开源项目，可以免费跑这套流水线。
不过吧，“验证过”不等于“没 bug”。
这一点，Anthropic 在原文里专门写了一节。
这批证明有几条明确的边界：
它证明的是在 RISC-V 芯片上跑、用特定方式打包的版本。而大家手机和电脑里，多数是 ARM 和 x86 芯片。 它只覆盖了部分入口，不代表整个库。 它只保证程序不崩溃、内存不越界，不保证程序算出来的结果是对的。
但这已经是很大的一步。
过去几年，AI 找漏洞的本事越来越强。Linux 内核最近一次，就披露了 1000 多个漏洞。
找bug变便宜了，攻击也跟着变便宜了。 防守方只靠发现一个补一个，越来越跟不上。
这一次，Claude给出了另一种可能：
不只找bug，而是在给定条件下，直接证明这条路上没有bug。
Anthropic在文末写道，形式化验证很快会像今天的模糊测试一样，成为几乎所有生产软件的标配。
能不能成真，要看接下来有多少开源项目真的排队接入。
但至少这一次，防守方先拿到了一件能规模化的武器。
