Anthropic 用 Claude 自动验证现有代码的正确性

Anthropic 与 Theorem 让 Claude 为 123 个开源库生成约 1.8 亿行形式化证明代码，并通过 Rocq 自动检查。Claude 在验证过程中发现数百个缺陷，其中包括一个潜伏十余年的逻辑错误；但证明仅适用于特定处理器架构、单线程程序和低于 64 MB 的输入，单次证明最高消耗数亿 tokens，且正式验证不等于完全无错误。