Anthropic用Claude验证开源软件安全
先了解这件事
AI 综述
2026年10月23日，Anthropic在X上表示，其与Theorem Labs合作，使用Claude在数周内为超过100个真实世界开源库证明安全属性；Anthropic称，传统形式化验证过去主要适用于小型代码库或需要大量专家时间，AI模型正在改变这一限制，研究全文发布于其官网。稍早于当日，The Decoder报道称双方利用Claude，为Google OSS-Fuzz中的123个开源库测试程序生成约1.8亿行数学证明代码，并由Rocq自动检查，以验证程序安全性。两则报道均未披露更多合作细节、验证结果或后续安排。
报道时间线
10月23日
- Anthropic 用 Claude 自动生成代码形式化证明并验证安全性
Anthropic 与 Theorem 合作，让 Claude 为 Google OSS-Fuzz 中 123 个开源库的测试程序生成约 1.8 亿行数学证明代码，并由 Rocq 自动检查。
- Anthropic 与 Theorem Labs 用 Claude 大规模验证开源软件安全属性
Anthropic 与 Theorem Labs 合作，使用 Claude 在数周内为超过 100 个真实世界开源库证明安全属性。Anthropic 表示，传统形式化验证过去主要适用于小型代码库或需要大量专家时间，AI 模型正在改变这一限制。研究全文发布于 anthropic.com/research/forma…。