Anthropic 形式化验证研究配图。图源：Anthropic 官网
一句话：以前要专家耗几年的「用数学证明这段代码不会炸」，现在 Claude 能按周量产了。
10 月 22 日，Anthropic Frontier Red Team 和形式化验证公司 Theorem 发文：用 Claude 在 RISC-V 汇编/二进制层，给 Google OSS-Fuzz 里 123 个开源库、239 个入口写出机器可检查的证明——在约定假设下，任意小于 64MB 的输入都不会触发崩溃（含 AddressSanitizer 抓到的内存错误）。他们称，这是首次把 AI 形式化验证铺到生产级开源库的汇编规模。
• Anthropic 研究原文
https://www.anthropic.com/research/formal-verification
• Anthropic 研究原文（再贴一次）
https://www.anthropic.com/research/formal-verification
• 公开证明仓库 oss-verify-proofs
https://github.com/theorem-labs/oss-verify-proofs
• 公开证明仓库（再贴一次）
https://github.com/theorem-labs/oss-verify-proofs
他们到底证明了什么
• 不是「代码完美无 bug」，而是：把现有 fuzz 测试翻译成规格，证明该入口在模型化的 RISC-V + Linux 环境下「测例永远过」。
• 证明写在 Rocq（原 Coq）里，约 1.8 亿行通过检查；单个入口常见约 60 万行证明，对应中位数约 1.8 万条 RISC-V 指令的二进制。
• 假设很硬：单线程、静态链接、固定内存预算、RISC-V + Linux。换到你电脑上的 x86/ARM + 动态链接 glibc，结论不能直接照搬。
• 写证明的过程中，Claude 还挖出并修补了多年 fuzz 都难碰到的 bug：超大输入、罕见布局、跨句柄调用顺序、甚至不崩溃的逻辑洞。
开发者能直接用什么
• Theorem 开源了一部分集合：约 60 个入口 / 25 个库的可复查证明（含 openssl、zstd、simdjson、mbedtls 等）。
• 另有 RISC-V / Linux 过程语义仓库，以及给维护者报名接入的 Claude Skill（贴进 Claude Code / Cursor 一类 Agent 就能走报名流程）。
• 报名 Skill（add-project）
https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md
• 报名 Skill（再贴一次）
https://github.com/theorem-labs/oss-verify/blob/main/.claude/skills/add-project/SKILL.md
• Linux 过程语义仓库
https://github.com/theorem-labs/rocq-linux-process-semantics
• Anthropic 官方 X 帖
https://x.com/AnthropicAI/status/2113390212911083894
Anthropic 相关配图。图源：既有媒体/官网素材
别过度解读
• 「形式化验证通过」≠「线上永远安全」：规格、CPU/OS 模型、证明检查器本身仍在信任边界里。
• 没覆盖的架构、多线程、动态链接、超过 64MB 的输入、库被调用方误用，都不在这批定理里。
• 真正的变化是成本曲线：把「只有航电/内核才玩得起」的证明，压到能对一堆日常开源库批量开跑；证明还能互相抄作业复用。
对安全圈读者：AI 已经很会找洞了；下一步是「在明确边界内证明这扇门关死」。Anthropic 这篇是把这句话第一次按工业库规模摊开。
机智流只做草稿预览，未群发。细节与局限以 Anthropic / Theorem 原文为准。
