Anthropic 用 Claude 数周内形式化验证百余个真实开源库

tianyin_xu · x · 2026-10-25

Anthropic 在 Frontier Red Team 博客发布新研究：与 TheoremLabs 合作，用 Claude 在几周内对超过 100 个真实开源库证明了安全属性。形式化验证传统上只适用于小型代码库或需大量专家时间，AI 模型正在改变这一点。

形式化方法研究者 Ilya Sergey 评价这是「历史性时刻」——形式化方法首次在大规模真实二进制上落地验证。但他指出局限：当前 spec 是单入口（非 API）、证明体量巨大、复用主要靠复制改造；FM 社区需要发展组合推理与模块化抽象才能进一步扩展规模。