Anthropic 称 Claude 能自动形式化验证代码安全性

Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 对 Google OSS-Fuzz 中 123 个开源库的测试程序做形式化验证，几周内产出约 1.8 亿行证明代码。Claude 并未编写新代码，而是把崩溃测试翻译成数学问题、分析编译后的机器码并生成证明，再由独立验证程序 Rocq 自动检查；据 Anthropic 说，这一流程几乎不需要人工复核。生成证明过程中 Claude 遇到数百个 bug 并获准自行修复，例如在验证一个广泛使用的 PDF 阅读器时，一周内发现的安全 bug 数量与该软件通常一整年报告的数量相当，还发现了一个十余年未被察觉的逻辑错误。Anthropic 承认形式化验证不等于无错，证明仅在特定处理器架构、单线程程序和小于 64MB 输入下成立，单条证明可能消耗数亿 token。