Anthropic 前沿红队：Claude 与 Theorem 合作，在 RISC-V 汇编层为 123 个 OSS-Fuzz 开源库的 239 个入口写出形式化证明，约 1.8 亿行 Rocq

核心背景与行业痛点

AI 找漏洞、串联利用的能力越来越强，传统的测试和 fuzz 只能「多试一些输入」，无法证明没有 bug。形式化验证能给出数学上的保证，但成本极高：seL4 内核实现用了 2 人年，验证却用了 20 人年，因此过去只用于航空电子等关键代码。Anthropic 前沿红队这次想证明，LLM 已能让形式化验证覆盖大量真实生产代码。

架构亮点与底层机制

做法是把 Google OSS-Fuzz 里开发者写好的 fuzz 入口直接当规范：编译成 RISC-V 可执行文件，结合 Theorem 的 RISC-V 指令语义和 Linux 进程语义，生成「任何小于 64 MB 的输入都不会崩溃」的定理，由 Claude 写证明、Rocq 内核校验。因为 OSS-Fuzz 会用 ASan 插桩，「不崩溃」同时意味着没有被 ASan 捕获的内存错误。证明卡住时，Claude 会修补代码、重新生成规范再证明。需要信任的只剩 RISC-V/Linux 模型、定理陈述和 Rocq 检查器本身。

权威 Benchmark 与实测跑分对比

官方口径：几周内证明了 123 个库的 239 个入口，约 1.8 亿行 Rocq，典型证明约 60 万行。过程中发现数百个 bug，包括需约 20 MB 特定输入的越界写，并重新发现 libexpat 的 CVE-2026-56132。在 36 个小任务上，Opus 5.5 证完一半所需 token 比 Opus 5 少约 40%；共享工作区让 token 再降 17%。另有实验：用 Claude 写的 x86 语义证明 Linux 内核 zlib 符合 RFC 1950；Rust 写的 Python 解释器在 170 万个随机程序上与 CPython 行为一致率 99.95%。

开发者实战落地与开箱指南

局限要看清：证明只针对单线程静态 RISC-V + musl，日常部署多是 x86/ARM + glibc；ASan 也抓不到全部内存错误，单个证明可能消耗上亿 token。想尝试的话，可以从 GitHub 上的 theorem-labs/oss-verify-proofs 复核公开证明，用 Theorem 发布的 Claude skill 为自己的项目接入流程，或申请 Theorem 为开源项目代跑同一流水线。