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

Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 为 Google OSS-Fuzz 中 123 个开源库的测试程序生成约 1.8 亿行数学证明代码，由 Rocq 自动校验，过程几乎不需要人工审查。