Anthropic联合Theorem用Claude形式化验证发现深层漏洞

Anthropic 联合 Theorem 利用 Claude 模型对现有软件进行形式化验证，在数周内生成了约 1.8 亿行数学证明代码，覆盖了 Google OSS-Fuzz 项目中 123 个开源库的测试用例。该过程通过 Rocq 独立程序自动检查证明，几乎无需人工复核，成功发现了数百个传统测试难以捕捉的深层漏洞，包括一个潜伏超过十年的逻辑错误。 尽管成果显著，该方法存在严格的适用边界：证明仅在特定处理器架构、单线程程序及 64 MB 以下输入条件下成立，且单次验证的计算成本高达数亿 tokens。虽然 Opus 5.5 相比 Opus 5 在解决相同证明任务时减少了约 40% 的 token 消耗，显示出模型效率的提升，但整体算力开销依然巨大。此外，Anthropic 并未披露项目的总财务成本，仅指出若 AI 能自我验证代码，可降低开发者审查时间从而节省全流程成本。 事实层面，该项目证明了 AI 在特定约束下具备自动化形式化验证能力；推断层面，这标志着软件验证范式正从“能否编程”转向“能否保证安全”，可能推动关键基础设施如 glibc 和 OpenSSL 的自动化验证普及；猜测层面，未来 AI 生成的代码是否能在更广泛的硬件配置中实现同等程度的自动验证仍待观察，目前的结论不能直接外推至通用商业软件的全场景部署。