Anthropic×Theorem：Claude 在 RISC-V 汇编级形式化验证 123 个开源库（约 1.8 亿行 Rocq），自称首次大规模 AI 汇编级验证

这件事意味着什么

【要点】

Anthropic Frontier Red Team 于 10 月 22 日（@AnthropicAI UTC 22:01，北京时间 06:01）发文：与 Theorem 合作，用 Claude 在汇编级（RISC-V）对 123 个真实开源库做形式化验证，据称为首次大规模将 AI 用于生产软件的汇编级形式化验证。

一、做法：把 Google OSS-Fuzz 的 fuzz 测试改写成「任意 <64MB 输入下永不崩溃」规格，对编译出的 RISC-V 二进制与 Theorem 的 RISC-V/Linux 语义一起交给 Claude 写 Rocq 证明；共覆盖约 239 个入口点，证明约 1.8 亿行 Rocq（典型单证约 60 万行，对应中位约 1.8 万条 RISC-V 指令）。证明过程中 Claude 还修了它自己发现的 bug（含需约 20MB 特定布局才触发的下溢、需 64MB 输入的越界读、libexpat CVE-2026-56132 再发现等）。

二、其他案例：用 Claude 写 RFC 1950 规格并证明 Linux 内核 zlib 实现（x86 二进制）；用 Verus 证明 Rust 子集 Python 解释器相对学术 CPython 语义；验证 PDF 阅读器时一周内发现的安全问题量级接近该项目一年公开报告量。

三、发布物：公开部分信任基（RISC-V/OS 语义、定理陈述）、无需打补丁即可证明的完整 Rocq、以及未能证完的规格；Theorem 另推 OSS Verify，并发布 Claude skill 帮开发者自验开源项目（免费面向开源）。

【可核验】

Anthropic 研究页：https://www.anthropic.com/research/formal-verification

@AnthropicAI：https://x.com/AnthropicAI/status/2113390212911083894

@theoremlabs OSS Verify：https://x.com/theoremlabs/status/2113396868814360821

文中数字与局限均来自官方正文（单线程静态 musl 二进制、RISC-V、固定内存预算等假设）。

【我们的判断】

一、背景：形式化验证长期卡在「证明比代码贵一个数量级」（文中 seL4：实现 2 人年、验证 20 人年）。与此同时 frontier 模型找洞能力上升，传统 fuzz/补丁循环不够；Anthropic 把「AI 进攻」对冲成「AI 写证明」，是红队线自然延伸，也呼应本站近期 METR/Redwood 对 OpenAI 监控缺口（e/1039）——攻防两侧都在加速。

二、横向：DeepMind 用 Lean 做数论/OEIS 形式证明（e/796 等）偏数学陈述；doubleAI Maxwell（e/974）偏运行时改代码并证明改动；本工作直接对着 OSS-Fuzz 入口与汇编语义，规模（123 库 / 1.8 亿行 Rocq）是软件安全方向目前最硬的公开演示。代价是信任基仍含 Rocq、ISA/OS 模型与定理陈述本身——「已形式化验证 ≠ 无 bug」。

三、影响：若成本随模型下降且证明可复用（文中共享工作区约少 17% token），关键依赖（glibc/OpenSSL/cURL 等）「验一次、处处受益」的路线图变得可信；安全预算可能从「更多 fuzz 机时」部分转向「证明流水线」。Theorem 的 OSS Verify 若落地，会改变开源维护者与保险/合规对「可证明安全」的预期。

四、局限：目前假设单线程、静态链接、RISC-V、输入 <64MB；多数生产二进制是 x86/ARM + 动态 glibc；规格不等于现实（ASan 也非全覆盖）。文中承认证明可耗数亿 token，短期待业界复现与独立审计。