Anthropic用Claude形式化验证123个开源库
Anthropic与Theorem合作，用Claude为OSS-Fuzz项目中的123个开源库完成239项证明，并发现数百个漏洞。
据aitimes.com报道，Anthropic于10月22日宣布，公司与形式化证明专业机构Theorem合作，使用Claude对谷歌OSS-Fuzz项目中登记的123个开源库的安全属性进行了形式化验证。
Claude为这123个库的239个测试入口完成了证明，显示在不超过64MB的所有输入下测试均能正常终止，不出现内存安全错误或断言失败。生成的证明以Rocq证明助手格式计共1.8亿行，中位数证明对应约1.8万条RISC-V指令的二进制程序。
Anthropic表示，Claude在证明过程中发现了数百个漏洞，随后修复代码并重新证明修复结果，例如某解压器中的计数器下溢和某图像解码器中的越界读取。此次工作还重新发现了libexpat XML解析器库中的CVE-2026-56132。
Anthropic称，这是首次在汇编代码层面对生产软件的安全属性进行大规模AI验证。公司公开了部分证明和用于验证的模型，Theorem则提供支持，帮助将该流程应用于其他开源项目。
另一项实验中的模型对比
在另一项实验中，Opus 5.5完成了36项验证任务中的一半，所用token比Opus 5少约40%，多个智能体协作使token用量再降低17%。
形式化验证过去主要应用于航空电子系统和操作系统内核等安全关键软件，因为其需要大量时间和专业知识。例如，seL4微内核的实现约耗时2人年，而形式化验证约需20人年。
快速问答
Anthropic用Claude验证了多少个开源库？
123个，来自谷歌OSS-Fuzz项目，共完成239个测试入口的证明。
这次验证发现了哪些漏洞？
Anthropic称发现数百个漏洞，包括某解压器的计数器下溢和某图像解码器的越界读取，并重新发现了libexpat中的CVE-2026-56132。