形式化验证，是不是只有那几家安全团队才玩得起？
简单说，它就是让机器证明一段程序在所有输入下都不会出某类错。模糊测试是抽样跑一遍。形式化验证是对输入空间里每一点都给理由。
上周四 Anthropic 发了一篇。这期收的几条都围着它。
123 个开源库，239 个入口点，1.8 亿行 Rocq 证明
代码来自 OSS-Fuzz。单个证明通常 60 万行上下，覆盖的 RISC-V 二进制指令数中位数 1.8 万条。
流程不复杂。把现成的模糊测试套件转成规范，再把 RISC-V 可执行文件、Theorem 那边的 RISC-V 和操作系统语义、无崩溃属性一起丢给 Claude 写证明，最后由 Rocq 内核检查。
点评：值得看的不是模型能写多长，是“内核检查”这四个字。Claude 写错，内核过不去。模型在这条链上只干粗活。
一个解压器副本，计数器下溢，只在约 20 MB 的罕见布局上触发
同类的还有。图像解码器要 64 MB 输入加 2 GB 以上内存才越界读。有一个库要跨同一文件的两个句柄走特定调用序列。libexpat 里那个 CVE-2026-56132 也被重新找出来，要靠深度嵌套输入。
这些缺陷模糊测试碰不到。它靠随机撞。撞不上的角落，它永远不知道。
形式化验证走另一条路，直接对输入空间下断言，边界条件正好是它擅长的。我认为这次最值钱的就是这几段。
某库里“限制应用可加载哪些文件”的功能，不是在所有路径上都生效
这种缺陷不会崩，ASan 那套根本不看。
一句话讲清楚：安全检查写了，漏了个口子。靠跑测试跑不出来，靠证明才可能问出来。
证明的前提：单线程、静态二进制、RISC-V、输入小于 64 MB
模型用的是 Linux 上的 RISC-V CPU、固定内存预算、静态 musl 二进制。多数人手里是 x86 或 ARM，动态链 glibc。
这条不交代，后面的话都没意义。它证明的是那个被建模的二进制，在那个被建模的环境里，不会因为内存安全错误或断言失败异常退出。模型之外的一概不在证明里。
Anthropic 自己也标了：RISC-V 模型、Linux 进程模型、定理陈述、Rocq 检查器，这几样仍然得信。剩下的缺陷可能就在这些可信组件里，也可能在证明范围之外。
zlib 的内核实现，被证明符合 RFC 1950
这条我本来想跳过，觉得跟主线重复。后来还是收了，因为它回答了一个问题：是不是只能玩 RISC-V。看起来不是。
这次直接拿 x86 编译二进制，x86 的形式语义也是 Claude 生成、再大量测过的。
在 zlib 这种到处都在用的库上，他们找到几处角落场景下的轻微缺陷，说不可利用，正在往上游提。
共享工作区里复用证明，token 少 17%
36 个真实 OSS-Fuzz 的小任务里，Opus 5.5 比 Opus 5 少用约 40% 的 token 证完其中一半。放进共享工作区，智能体能复用彼此的证明。有几个单独跑不过的任务，共享之后过了。
文章拿 Mathlib 举例。Lean 那个形式数学库，700 多人提交了将近 30 万条定理，新证明直接建在旧证明上面。
这是形式化验证和模糊测试最不一样的地方。测试跑完就散了。证明留下来，别人能接着用。攒得越多，下一个越便宜。
Theorem 说这套流程能给别的开源项目跑，还放了个 Claude 技能出来
留给普通人的，短期内还是“用不上”三个字。
但门槛的方向在往下走。以前形式化验证是几个安全关键系统的特权，现在至少有一家愿意把流程和技能放出来。这就是够得着，虽然今天还够得有点远。
有一段我没太吃透。他们让 Claude 用 Rust 写了个大 Python 子集解释器，再用 Verus 证明它符合论文描述的 CPython 语义，170 多万个随机程序跑出 99.95% 行为一致。
这个 99.95% 和“证明”之间到底是什么关系，我还没想明白。先放在这里，想清楚了再补。
Anthropic 的结论是，形式化验证会像今天的模糊测试一样，慢慢变成多数生产软件可用的常规工具。
这个判断我信一半。工具确实在变便宜，但“证明范围之外还剩什么”，不会因为模型变强就自己消失。
本周就这些。上面哪条你试过，或者觉得我讲错了，欢迎告诉我。
下周见。