Anthropic 用 Claude 实现大规模形式化验证：1.8亿行证明覆盖123个开源库

Anthropic 与形式化验证公司 Theorem 合作，利用 Claude 对 123 个真实开源软件库进行了 RISC-V 汇编代码级的安全性质证明，据称为首次大规模将 AI 形式化验证应用于生产级软件的机器码层面。团队将 Google OSS-Fuzz 的模糊测试自动转化为形式化规约，即证明该测试对任何小于 64MB 的输入都不会崩溃，再由 Claude 撰写证明，由 Rocq 证明检查器机械化核验。数周内，Claude 为 239 个测试入口完成了约 1.8 亿行 Rocq 证明，单个证明平均约 60 万行，覆盖中位长度 1.8 万条指令的二进制程序。在尝试证明的过程中，Claude 发现并修复了数百个漏洞，其中包括模糊测试几乎不可能触发的深层缺陷，如需约 20MB 特定构造输入才能引发的越界写入，并再次发现了 libexpat 中的 CVE-2026-56132。团队还验证了 Linux 内核中的 zlib 实现、用 Rust 编写的 Python 解释器等项目，并在一款广泛使用的 PDF 阅读器中，一周内发现了一整年数量的安全漏洞。研究同时指出局限：证明依赖对 CPU 与操作系统语义的建模假设，且规约范围有限，形式化验证并不等于零漏洞。

事件分析

核心观点：AI 既能在汇编层自主找漏洞，也能自主证明代码无漏洞，形式化验证正从二十年专家工程变成模型可量产的工业能力。