Anthropic 用 Claude 自动验证现有代码，正确性证明受严格条件限制

Anthropic 与 Theorem 使用 Claude 为现有软件自动生成数学正确性证明，并在验证过程中发现数百个缺陷。项目采用 Google OSS-Fuzz 中 123 个开源库的测试程序，数周内生成约 180 million 行证明代码，由 Rocq 自动检查；据 Anthropic 称，过程几乎不需要人工复核。