AREX Feed Article
Anthropic 发布新研究：与 Theorem Labs 合作用 Claude 为 123 个开源库证明机器码级安全性质
Anthropic 于 10 月 21 日在旗下 Frontier Red Team 博客发布，宣布与形式化验证公司 Theorem Labs 合作，用 Claude 在数周内为来自 Google OSS-Fuzz 项目的 123 个开源库、239 个模糊测试入口点证明了安全性质：这些证明作用在编译后的 RISC-V 机器码上，结论是在每一种被建模的 Linux 响应与内存布局下，程序对任何小于 64 MB 的输入都会正常退出，不触发内存安全错误或断言失败。博文称，全部证明约合 1.8 亿行 Rocq 代码；据作者所知，这是首次在汇编代码层面用 AI 对生产软件进行的大规模形式化验证。
10 月 22 日（北京时间 23 日早晨），Anthropic 官方账号 推介这项研究：「形式化验证能证明代码不存在特定类别的 bug，但历史上它只对小代码库可行，或需要大量专家时间」，而随着 AI 模型的进步，「这一局面开始改变」。按博文给出的口径，写证明的过程本身还发现并修复了数百个 bug——其中一些多年来躲过了数万亿次测试。
把现成的测试套件变成待证规范
形式化验证的做法，是把代码变成数学模型，再证明它永远满足一组事先写好的安全规则；规则一旦得证，能违反规则的 bug 就被排除在外。麻烦在于写证明：博文说，证明往往比原代码长出许多倍，写证明又需要极稀缺的专门技能——seL4 操作系统内核实现花了 2 个人年，形式化验证它却花了 20 个人年，因此这项技术过去基本只出现在空中客车航电代码这类安全攸关场合。这篇研究的出发点则是：即便像 Linux 内核这样测试极其充分的软件也有 bug——它部署在数十亿台设备上，最近披露的漏洞超过 1,000 个，而前沿模型正越来越擅长把多个看似无害的漏洞串成严重利用链。
另一重困难是「正确」难以定义：PNG 解码器有明确规范可依，文本编辑器或浏览器「正确」意味着什么则说不清。Theorem Labs 的做法是绕开这个问题，直接把开源库现成、可编译的测试套件当作规范，规则只有一条——这套测试永远通过。落到模糊测试（fuzzing，让测试引擎向代码入口点灌入海量半随机输入以制造崩溃的测试方法）上：输入越多越能逼近 bug，但输入空间无穷大，跑再久也无法穷尽所有路径。研究团队把 OSS-Fuzz 数百个项目的模糊测试改写成一条机器码层面的规范：对任何小于 64 MB 的输入，这个入口点都不会崩溃。规范一旦得证，继续对这个入口点做模糊测试就成了多余动作。
流程本身也机械化了：开源库和它的模糊测试先编译成 RISC-V（一种与 x86、ARM 同类的处理器指令集架构）可执行文件；可执行文件、Theorem 提供的 RISC-V 指令与 Linux 进程形式语义，加上「不崩溃」这一待证性质，机械地合成出证明必须满足的规范；Claude 负责写证明，Rocq 证明内核负责检查证明是否成立。OSS-Fuzz 还会自动给 C/C++ 程序插上 AddressSanitizer——一个让内存错误在发生瞬间即崩溃并报告的编译器插桩工具，而内存错误正是软件漏洞的主要来源之一。几周跑下来，这条流水线为全部 239 个入口点拿到证明，单个证明典型约 60 万行，被证二进制的中位长度为 18,000 条 RISC-V 指令。需要人信任的只剩少数「可信组件」：RISC-V 与 Linux 进程的形式模型、被证定理的表述、Rocq 检查器本身，外加它依赖的硬件、操作系统和 OCaml 编译器；剩余 bug 要么藏在这些组件里，要么落在证明范围之外。
写证明的过程，同时是抓 bug 的过程
让 Claude 停下来等人修 bug 再继续证明不现实，团队干脆授权它自己修：打上补丁、用新代码重新生成规范、接着证明。为防「奖励投机」（reward hacking）——比如把程序改写成平凡地永不崩溃，好让规范变得可证——团队对任何补丁扣分，给能证明「补丁改变了哪些输入、改变的范围有多小」的做法额外加分，并记录、审计每一处补丁。
尝试写证明的过程发现了数百个 bug，其中很多是模糊测试几乎不可能碰到的——模糊测试的输入通常不超过 1 MB，还依赖代码覆盖率来引导搜索。文中列举的案例包括：某个库自带的解压器副本存在计数器下溢，可导致越界写入，但只在约 20 MB、且布局罕见的输入上触发；一个图像解码器的越界读取需要 64 MB 输入和 2 GB 以上内存；另一个库的越界读取要对同一文件的两个句柄按特定顺序调用；libexpat 中则重新发现了需要深度嵌套输入的 CVE-2026-56132。不崩溃的纯逻辑错误同样有：某个库用来限制应用可加载哪些文件的功能，并不总是被执行。
对团队来说，这套流程的价值不完全取决于证明最终是否完成：光是尝试，就能产出必须修复的真实漏洞。
红黑树、zlib 与一个 Rust 版 Python 解释器
「不崩溃」只是底线。博文指出，真实项目的模糊测试往往断言更高层的性质：编码解码往返一致、幂等性、代数定律、与参考实现等价。以 LZO 压缩算法为例，其模糊测试断言「先压缩再解压，结果等于原文」——证明这个测试永不崩溃，就等价于证明这条性质成立。
有些性质是证明过程倒逼出来的。要完成 cpp-httplib 的证明，必须排除 std::set 析构函数因递归过深导致栈溢出的可能；递归深度受树高约束，于是 Claude 得在机器码层面证明 libc++ 的红黑树再平衡算法确实把树高控制在对数级别。
博文还给出三组延伸实验。其一，zlib：让 Claude 为定义 zlib 文件格式的 RFC 1950 写形式规范，再证明 Linux 内核中的 zlib 实现符合规范——这次直接在 x86 编译产物上证明，依据是 Claude 自己生成、经过大量测试的 x86 指令集形式语义；团队称这种全自动生成的语义虽无法保证完美，但按它单步执行可以启动一个 Ubuntu 用户态，还顺带找出了官方参考文档里的数百处错误和硬件本身的少量 bug。同样的流程又套用在另外六个广泛使用的库上，发现了一些无法利用的角落案例 bug，正在向上游提交。其二，让 Claude 用 Rust 实现一个大子集的 Python 解释器，并用验证工具 Verus 证明它符合一篇学术论文概括的 CPython 语义；随后拿 170 万个随机生成的 Python 程序实测，99.95% 的用例与 CPython 行为完全一致，差异都是已知角落案例。其三，团队在对几个广泛使用的关键应用验证简单安全性质时发现了一批问题：其中一个应用里藏着一个潜伏十余年、此前未知的逻辑 bug；在对一个广泛使用的 PDF 阅读器的验证中，一周找到的安全 bug 相当于通常一年的报告量。
成本曲线：新模型省四成 token，证明可以互相搬
博文把「证明动辄消耗数亿 token」列为主要限制，同时给出两条正在起效的降本曲线。一是模型本身：团队用真实 OSS-Fuzz 代码搭了 36 个小型验证任务，Opus 5.5 用比 Opus 5 少约 40% 的 token 证明了其中一半。二是复用：证明和软件一样由更小的证明递归构成，越小的证明越容易复用——在允许代理互相复制已完成证明的共享工作区里，完成同样任务比单干省 17% 的 token；34 个完成的证明中有 30 个，单干代理花的 token 更多；另有 2 个证明，单干代理根本没能完成。
博文配图：36 个验证任务中由单个代理在给定 token 预算下完成的任务份额，Opus 5.5 与 Fable 5.1 的曲线整体高于 Opus 5。
复用在 OSS-Fuzz 工作里同样成规模：大部分证明内容是所有程序共有的部分（C 运行时初始化、AddressSanitizer 的运行时），不同程序的证明高度重叠，代理团队索性复制别家已完成的证明再改写适配。
博文配图：三个程序的证明构成。深蓝色块与已有证明保持相同，libcups 的新增部分是其自身函数的证明。
博文拿 Lean 生态的共享数学库 Mathlib 作参照：近 30 万条定理、700 多名贡献者，每个新证明都建立在已有成果之上；OSS-Fuzz 工作中也积累了类似的证明库。
「已验证」不等于「没有 bug」
博文用专门一节给结论降温：「形式化验证过」不等于「没有 bug」。证明检查器只能确认编译后的程序满足规范，却无法确认规范是否符合现实——被验证的代码真出了错，通常意味着规范或对机器语义的假设与现实有出入。博文列出的边界很具体：这批证明针对以 musl libc 静态链接的单线程 RISC-V 二进制，而多数人实际在 x86 或 ARM 上动态链接 glibc 运行这些库；AddressSanitizer 检测不了所有内存安全问题；团队也没有验证每个库的全部入口点，就算全部验证，死代码仍在覆盖之外；调用方误用库函数造成的内存破坏，同样不在这批证明之内。按作者的说法，好处是剩余 bug 的藏身范围被大幅收窄，而加固这几个可信组件，比逐行调试全部被证代码要可控得多。
Theorem 的路线图：验证整个 Nix 生态
Theorem 一侧同步确认了这次合作，其写道：「在与 Anthropic 的合作中，我们在汇编代码层面为 100 多个开源库证明了安全性质，并发现了多年测试都漏掉的 bug。」这家公司把同一能力做成了对外服务，的表述是：「告诉我们需要验证的性质，我们将交付一份可在 CI 中检查的证明。」据 Anthropic 博文，Theorem 还愿意为其他开源项目运行同一套验证流程，并发布了一个帮助开发者验证自己代码的 Claude skill；Anthropic 团队自己也公开了这批证明的子集、RISC-V 与 Linux 形式语义和此前未公开的可信组件，明确欢迎独立验证——可能暴露未修复漏洞的证明不在发布之列。
Theorem 在 9 月 29 日的（10 月 19 日更新）里，把 nixpkgs——Nix 生态的软件包集合——当作「验证所有软件」的蓝本：nixpkgs 约 150 GB 机器码、超过 12 万个二进制；其中仅 9 MB 的共享库，就是三分之二代码的完整依赖集。按其估算，若模型在验证能力上的提升快于整体——其补充的评测显示，5 月至 9 月模型在软件验证上的表现约每两个月翻一倍——到 2027 年底，以约 1.34 亿美元验证 nixpkgs 中 95% 的机器代码是可及的目标。复用是这笔账成立的关键：OpenSSL 位于近 1.6 万个软件包的运行时依赖闭包里，按当前费率证明它一次约 22 万美元，平摊到每个复用的包约 14 美元。
这 1.34 亿美元和 2027 年底的时限，都建立在 Theorem 自己标注的条件上：模型在验证能力上的提升要快于整体能力。条件是否成立，决定这套流程是停在已证完的 123 个库，还是铺向整个 nixpkgs。