用Claude做形式化验证：为123个开源库写出证明
对OSS-Fuzz中123个库的机器码做形式化验证：Claude用Rocq写了1.8亿行证明，顺带发现了数百个漏洞。
本文的其他语言版本：العربيةDeutschEnglishEspañolFrançaisItaliano日本語Polski
10月22日，Anthropic的Frontier Red Team与Theorem公司发布了一项研究：Claude为OSS-Fuzz项目中的123个开源库编写了形式化的安全证明。这些证明针对的是编译后的RISC-V代码，而不是源代码。据作者介绍，这是首次借助AI在如此规模上对生产软件进行汇编级的形式化验证。
用Claude做形式化验证是怎么回事？
形式化验证是一种数学证明，证明程序对任意可能的输入都具备某种性质，而不仅仅是对测试过的那些输入。问题在于，这在过去需要专家投入多年时间。研究中给出的对比是：验证seL4内核花了约20人年，而编写它只用了2人年。
研究中的流程如下：
- 起点是OSS-Fuzz中已有的模糊测试（OSS-Fuzz是Google的项目，持续不断地用随机数据轰炸各种库）。
- 将库连同测试一起编译成RISC-V可执行文件。
- 基于Theorem提供的RISC-V处理器和Linux进程语义，自动生成规约：程序必须始终正常退出，不出现内存错误，也没有断言失败。
- Claude编写证明，再由Rocq证明检查器确认证明满足规约。
- Claude一旦遇到漏洞，就修补代码，重新生成规约，并从头构建证明。
这一保证覆盖所有小于64 MB的输入，以及所有建模范围内的系统响应和内存布局（前提是在RISC-V和Linux上运行的静态链接、单线程程序）。
Anthropic公布了哪些数字？
- 123个库中的239个入口点。
- Rocq证明合计约1.8亿行；一个典型证明约60万行，对应的程序中位数为1.8万条RISC-V指令。
- 整个工作耗时几周。
- 在36个小任务上，Opus 5.5证明了一半，消耗的token比Opus 5少约40%；在共享工作区协作的智能体比单独工作时少用17%。
有意思的是，为cpp-httplib写证明时，需要证明libc++中红黑树的深度受对数约束，因为只有这样才能排除std::set析构函数中的栈溢出。
Claude发现了哪些漏洞？
据作者介绍，这一流程发现了数百个经历多年模糊测试仍未被发现的漏洞。文章中的例子包括：
- 解压器中计数器下溢导致的缓冲区越界写入，但只在约20 MB、结构罕见的输入下才会触发。
- 图像解码器中的缓冲区越界读取，需要64 MB的输入和超过2 GB的内存。
- 只有在对同一文件的两个句柄按特定顺序调用时才会出现的缓冲区越界读取。
- 重新发现了libexpat中的CVE-2026-56132（需要深度嵌套的输入）。
- 一个逻辑漏洞：限制文件访问的函数并非总能生效，尽管程序并没有崩溃。
此外还有三项额外实验。Claude编写了RFC 1950的形式化规约，并在x86二进制文件上证明Linux内核中的zlib正确实现了它。它还用Rust构建了一个Python子集解释器，在170万个随机程序中，有99.95%的情况下行为与CPython一致。而尝试验证一款流行的PDF阅读器时，一周内发现的安全漏洞数量相当于通常一年的报告量。
这与PHP2Shell和Bank of America使用Claude Mythos是同一个方向：AI模型能发现人类和传统工具多年都没有发现的漏洞。只不过这一次，结果不只是一个补丁，而是一份证明。
需要注意什么？
第一，“已验证”意味着什么。作者明确写道，形式化验证并不意味着代码没有漏洞（原文为“»Formally verified« does not mean »bug-free.«”）。证明的可靠程度取决于规约、RISC-V和Linux模型，以及Rocq检查器本身。
第二，适用范围。这些证明针对的是使用musl的静态链接、单线程RISC-V二进制文件，而我们大多数人是在x86或ARM上配合glibc运行代码。它们也不覆盖死代码，以及调用库的程序自己破坏内存的情况。
第三，成本。单个证明可能消耗数亿个token，作者自己也称这是主要限制。
部分证明已经发布在GitHub上（oss-verify-proofs），同时公开的还有RISC-V与Linux语义。其余部分暂缓公开，因为可能暴露尚未修补的漏洞。
常见问题
什么是形式化验证？
它是一种由程序检查的数学证明，证明代码对所有输入都具备某种性质，例如永远不会越界写入缓冲区。测试和模糊测试只检查选定的情况。
经过验证的库就没有漏洞了吗？
不是。证明只保证在所描述的模型内（RISC-V、Linux、输入小于64 MB、单线程）不会崩溃。漏洞可能藏在规约里、机器模型里，或者在这个范围之外。
我能验证自己的项目吗？
Theorem运营着OSS Verify，这是一项面向部分开源项目的免费计划。与OSS-Fuzz类似，由项目维护者提交包含project.yaml、Dockerfile和build.sh文件的pull request来申请。需要做好把构建迁移到静态riscv64二进制文件的准备。