Anthropic称Claude已证明123个库的安全属性

Anthropic 于 2026 年 10 月 22 日发表研究称，在与 Theorem 的合作中，Claude 针对 123 个开源库的 239 个模糊测试入口点，在 RISC-V 汇编代码层面生成了经机器验证的安全属性形式化证明，并修复了发现的漏洞。方法是把库中可编译的模糊测试转化为形式化规格说明，规定任何小于 64 MB 的输入都不会使测试崩溃，由 Rocq 证明检查器验证。Anthropic 称，证明共约 1.8 亿行 Rocq 代码，过程中发现了数百个漏洞，其中许多不太可能被模糊测试器发现，包括 libexpat 中的 CVE-2026-56132 和一个潜伏十余年的逻辑漏洞。