Fuzzing 一直是软件安全的苦力活。开发者写一个入口点，让 fuzzer 拿海量半随机输入去撞，撞出崩溃就算赢。问题在于输入是无限的，再怎么撞也撞不完——它能告诉你"这里有 bug"，却没法告诉你"这里没有 bug"。形式化验证能给后一句，代价却是过去要专家投入数年：seL4 内核实现花了 2 人年，正式验证又花了 20 人年，长期只用在空客飞控这类极端关键的场景。
Anthropic 与 Theorem 的合作把这条曲线掰弯了。用 Claude，他们在 RISC-V 汇编级为真实开源库生成可机器检查的形式化证明。按 Anthropic 的说法，这是他们所知范围内首次在汇编代码层把形式化验证用到生产软件的尝试（原文）。
从"跑测试"到"证命题"
关键手法不是让模型重写代码，而是把库已有的 fuzz 测试自动转成一条规格：这个测试在任意输入下都不会崩溃。规格定义在编译后的 RISC-V 指令上，底层依赖 Theorem 提供的 RISC-V 指令集与 Linux 进程语义；Claude 负责写证明，Rocq 内核负责校验这份证明是否真的满足规格。
这样一来，开发者真正需要信任的东西只剩三样：RISC-V 与 Linux 进程的语义模型、被证明的定理陈述本身，以及 Rocq 证明检查器。
239 个入口点，1.8 亿行证明
规模上，Claude 在数周内先修掉它发现的 bug，随后为 Google OSS-Fuzz 中 123 个库的 239 个入口点证明了"任意输入不崩溃"（输入上限 64 MB）。这些证明合计约 1.8 亿行 Rocq，单个证明通常在 60 万行左右，覆盖的二进制中位数是 1.8 万条 RISC-V 指令。Unite.AI 援引技术附录给出的数据更狠：Claude 期间总共写了约 10 亿行 Rocq，只有约 1.8 亿行通过了证明检查；cJSON 一个 391 行的解析器入口点拿到了 63 万行证明。
顺带挖出来的 bug
比证明数量更有意思的，是证明过程顺手捞出的缺陷。Claude 在一个解压器的拷贝里找到计数器下溢，进而导致越界写，但只在约 20 MB 输入配一种罕见布局时才触发；一个图像解码器里的越界读需要 64 MB 输入加上超过 2 GB 内存；libexpat 里它重新发现了 CVE-2026-56132。它还找到根本不会崩溃的逻辑 bug，比如某项限制应用可加载哪些文件的特性并非总被强制执行。在验证某个常用 PDF 阅读器时，团队称一周内发现的安全 bug 数量，相当于平时一年上报的量。
成本能不能撑住
形式化验证最大的短板是贵，证明可能要烧掉数亿 token。Anthropic 的应对有两条。一是新模型更省：他们从真实 OSS-Fuzz 代码里缩出 36 个小型验证任务，Opus 5.5 用比 Opus 5 少约 40% 的 token 就完成了一半。二是证明可复用：允许智能体在共享工作区里互相拷贝证明后，token 消耗下降 17%，还有智能体在单独作战失败后靠拷贝别人的证明成功。这跟 Lean 社区靠 Mathlib 堆到近 30 万条定理、700 多位贡献者参与的路径是同一个逻辑。
边界在哪
Anthropic 自己把话说得很清楚："形式化验证"不等于"没有 bug"。证明检查器没法判断规格是否符合现实。这些证明覆盖的是单线程、静态链接 musl libc 的 RISC-V 二进制，而多数人跑的是 x86 或 ARM、动态链接 glibc；AddressSanitizer 本身也检测不出全部内存安全问题；每个库也不是所有入口点都验证过。另一个隐患是 reward hacking——理论上 Claude 可以把程序改写成"永远不会崩溃"的样子来让命题成立，团队的应对是对打补丁扣分、对"证明补丁只影响哪些输入"加分，并对补丁做日志与审计。
所以呢
最值得留意的不是数字，而是分工变了：模型不再只负责"找 bug"，而是负责把"找 bug"升级成"证明没有 bug"，人类只需要守住三个信任锚点。如果这条路径走通，软件安全的默认形态会从"我们测了很多"变成"这一部分被证明过"。