Anthropic 发布研究文章称，其与 Theorem 合作，利用 Claude 为 123 个 OSS-Fuzz 开源库的 239 个入口点完成了二进制层面的形式化证明：在指定运行条件下，对任意小于 64 MB 的输入，相关程序都能正常退出，不触发证明范围内的内存安全错误或断言失败。尝试证明的过程还发现了数百个漏洞，其中包括模糊测试难以触发的问题。
形式化验证需要先定义程序应满足的规格，再证明程序始终遵守这些要求。Anthropic 在文中举例，seL4 操作系统内核的实现耗费了 2 人年，形式化验证则耗费了 20 人年。
此次项目从已有的模糊测试入手，将开源库及测试编译成 RISC-V 可执行文件，再结合 Theorem 的 RISC-V 指令和 Linux 进程语义，生成「测试不会崩溃」的规格。Claude 负责写证明，Rocq 证明检查器负责核对。
据 Anthropic 披露，团队用几周完成了上述验证，证明总计约 1.8 亿行 Rocq 代码；典型证明约 60 万行，对应二进制的中位长度为 18,000 条 RISC-V 指令。Claude 发现漏洞后会修补代码，系统据此重新生成规格，再由 Claude 继续证明。
Anthropic 列举了一个解压器中的计数器下溢问题：它会导致越界写入，但需要约 20 MB、具有特定罕见布局的输入才能触发。另一个图像解码器的越界读取问题，则需要 64 MB 输入和超过 2 GB 的内存。
文章指出，模糊测试器通常将输入限制在约 1 MB，这使上述问题难以通过模糊测试发现。Claude 还重新发现了 libexpat 中需要深度嵌套输入才能触发的 CVE-2026-56132。
Anthropic 强调，「经过形式化验证」不等于「没有漏洞」。此次证明针对运行于 RISC-V CPU 和 Linux、链接 musl libc、具有固定内存预算的单线程静态二进制。证明的可信性仍依赖形式模型、定理陈述和 Rocq 检查器。
覆盖范围也有限：ASan 无法检测所有内存安全问题，团队没有验证每个库的全部入口点；即使验证全部测试入口，也不意味着覆盖整个库。
生成证明的成本同样是限制。Anthropic 称，证明可能需要数亿 token 才能产出。在发布方的 36 个小型验证任务测试中，Opus 5.5 完成一半任务所需的 token 比 Opus 5 少约 40%；让智能体共享工作区、复制彼此证明后，所需 token 减少了 17%。
Anthropic 已公开部分证明及相关 RISC-V、Linux 进程语义。Theorem 则提供为其他开源项目运行同一流程的服务，并发布了帮助开发者验证自身代码的 Claude skill。
