Anthropic用Claude为123个开源库生成约1.8亿行形式化证明代码
Anthropic前沿红队与Theorem合作，让Claude将崩溃测试转译为数学问题并自行修复发现的数百个漏洞；公司称流程几乎无需人工复核，但证明仅在特定处理器架构、单线程、输入小于64MB的条件下成立。
AI解读：Anthropic公布的工作对象是已有代码而非新写代码：Claude把Google OSS-Fuzz项目中123个开源库的测试程序转译为数学问题，分析编译后的机器码并生成证明，再由独立程序Rocq自动校验。
“形式化验证等于无错”不成立。Anthropic承认证明只在严格条件下有效：特定处理器架构、单线程程序、输入小于64MB；而这些库实际运行在别的硬件和配置上。
成本边界同样明确：单个证明消耗可达数亿token，Anthropic未公布项目总成本。“完全自主”指证明生成环节，所用工具与形式化基础由Theorem的人工构建。
来源中可核对的效果包括：借验证发现并自行修复数百个漏洞，在一个常用PDF阅读器的验证中一周内发现的安全漏洞数量相当于该软件通常一整年的报告量，另有一处逻辑错误十余年未被发现；这些是个案，不能外推为整体缺陷率。
Anthropic称，其前沿红队与合作伙伴Theorem让Claude承担形式化验证中的证明工作，在数周内为Google OSS-Fuzz安全项目中的123个开源库生成了约1.8亿行数学证明代码。
流程是先由Claude把崩溃测试转译为数学问题，再分析编译后的机器码并生成证明，最后由独立验证程序Rocq自动检查。Anthropic称这一过程几乎不需要人工复核，并将证明生成称为“完全自主”，同时说明所用工具和形式化基础由Theorem的人工构建。
发现的漏洞与已知案例
Anthropic称，Claude在生成证明过程中遇到数百个漏洞，并被允许自行修复。研究者表示，其中许多漏洞常规测试难以发现，只在特定条件下才出现，例如异常大的输入文件或特定的访问顺序。
来源给出的个案包括：在验证一个广泛使用的PDF阅读器时，团队一周内发现的安全漏洞数量与该软件通常一整年的报告量相当；另一处逻辑错误十余年未被发现。Anthropic还称，即使完整证明最终未能成立，验证尝试本身也能暴露真实漏洞。
适用范围与限制
Anthropic承认，“形式化验证”不等于“没有错误”。证明只在严格条件下成立：特定处理器架构、单线程程序、输入小于64MB。实际中这些库运行在不同硬件和配置上。
成本方面，单个证明可消耗数亿token，Anthropic未公布项目总成本。来源另提到一次较小规模测试显示证明可复用，且Opus 5.5完成一半证明所用token比Opus 5少约40%。