#Anthropic

Anthropic 用 Claude 自动为现有代码生成形式化证明

Anthropic 前沿红队与 Theorem 合作，让 Claude 对 Google OSS-Fuzz 中 123 个开源库的测试程序做形式化验证，几周内产出约 1.8 亿行数学证明代码，由 Rocq 独立校验。Anthropic 称该流程几乎不需要人工复核，Claude 在生成证明过程中发现并自行修复了数百个缺陷，包括一个十余年未被发现的逻辑错误。