北京时间 2026 年 10 月 23 日约 06:01，Anthropic 官方账号在 X 指向一篇日期为 2026 年 10 月 22 日的 Frontier Red Team 研究文。Anthropic 称，与 Theorem 合作，用 Claude 在 RISC-V 汇编层对来自 Google OSS-Fuzz 的真实开源库形式化证明了安全属性。DigIntoAI 没有实测这些证明或流水线。

按 Anthropic 说法，Claude 先修补发现的缺陷，再证明：在 123 个 OSS-Fuzz 库的 239 个 fuzz 入口点上，对任意小于 64MB 的输入、以及所建模的 Linux 操作系统响应与内存布局，程序不会因内存安全错误或断言失败而崩溃。Anthropic 称据其所知，这是首次大规模用 AI 对生产软件做汇编级形式化验证。Anthropic 称将公开部分 Rocq 证明与可信组件；Theorem 另称可为其他开源项目跑同一流水线，并发布可复用的 Claude skill 帮助开发者起步。

Anthropic 同时写明边界：证明假定单线程静态二进制、固定内存预算、RISC-V CPU 与 Linux。需信任的工件包括 RISC-V 与 Linux 进程形式模型、所证定理陈述，以及 Rocq 证明检查器。Anthropic 写明这并不等于库中无 bug；剩余问题可能落在上述可信组件内，或超出证明范围。简言之，LLM 放大的形式化验证可在这些假设下证明既定的不崩溃规约，但不能单独保证一切部署场景零缺陷。站内相关说明见 Anthropic 用 Claude 收窄代码攻击面、Anthropic 将 Agent Skills 捐赠给 AAIF 和 METR 与 Redwood 对 OpenAI 内部 agent 监控做了红队评估。

我们没有复现 Rocq 证明，没有重跑这些 OSS-Fuzz 入口点，也没有核实 Theorem 的 Claude skill。