原标题：New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Anthropic 发布 Frontier Red Team 博客新研究，与 TheoremLabs 合作，用 Claude 在数周内为一百多个真实开源库证明了安全属性。形式化验证能证明代码不存在特定 bug，但此前只适用于小型代码库或需要大量专家时间，AI 模型正开始改变这一局面。原文链接：https://t.co/zUyx8CjBEk
原文给出了用 Claude 大规模形式化验证开源库的具体做法和规模数字，可帮助读者了解 AI 在代码安全证明上的进展。
本页的摘要、推荐理由与解读出自 AIsa Studio 的 AI 风向智能体，原文版权归原作者所有。
2026 年 10 月 22 日，Anthropic 发布 Frontier Red Team 博客新研究，与 TheoremLabs 合作，用 Claude 在数周内为一百多个真实开源库证明安全属性。形式化验证可证明代码不存在特定 bug，但此前仅适用于小型代码库或需大量专家时间，AI 模型正改变这一局面。10 月 23 日的官方博客跟进披露更多细节：团队对 123 个开源库在 RISC-V 汇编代码层面证明安全性质，包括程序在特定条件下不会触发内存安全错误或断言失败，作者称这是首次大规模用 AI 对生产软件做汇编级形式化验证；过程中 Claude 还发现了多年未被检测到的 bug，团队为防 reward hacking 对任何补丁施加惩罚，并奖励证明补丁未改变程序行为。同日 The Decoder 报道称，Claude 将崩溃测试转化为数学问题、分析机器码并生成约 1.8 亿行证明，由 Rocq 独立自动校验，几乎无需人工复核；验证某广泛使用的 PDF 阅读器时，一周发现的安全漏洞相当于其一年报告量，还抓到一个潜伏十余年的逻辑错误。报道同时指出限制：证明仅在特定处理器架构、单线程和 64 MB 以内输入下成立，单个证明耗资最高数亿 token；Opus 5.5 比 Opus 5 用约少 40% 的 token 解决一半证明；Theorem 计划将方法推广到 glibc、OpenSSL 和 cURL。
Studio