发帖
雷达卡
资料名称： Anthropic 2026 年 10 月 22 日发布的研究报告《LLMs are making formal software verification feasible at a much larger scale》，与 Theorem 合作完成。
帖内资料： 研究正文全文（含四章正文与局限说明）、6 页技术附录 PDF（三个定理的精确表述、crash 的定义、Rust 版 Python 解释器实验、形式化验证专家评述），以及三个公开代码与证明仓库的入口。
时间覆盖： 正文发布于 2026 年 10 月 22 日；配套仓库最近一次推送在 2026 年 10 月 27 日至 28 日之间。
许可与引用： 研究报告网页与附录 PDF 未标注转载许可；代码仓库里 oss-verify-proofs 与 rocq-linux-process-semantics 为 MIT 许可，oss-verify 为 Apache-2.0。
适用任务： 软件供应链安全评估、形式化验证入门、AI 编程能力边界判断、开源依赖库的安全审计。
先说要解决什么问题。形式化验证一直被认为「贵得只有飞机和操作系统用得起」：seL4 微内核写代码用了两个人年，验证它用了二十个人年；空客的飞控代码也是同类投入才做下来。这份报告的主张是，这个成本结构正在变——让模型去写证明，几周时间就能把上百个真实开源库的汇编层安全性证完。
具体做了多少活，报告给了很实的数字：123 个来自 Google OSS-Fuzz 的开源库，239 个入口点（entry point，即作者为测试留的入口，任何让程序崩溃的输入都算 bug）。证明直接作用在编译后的 RISC-V 指令上，不是源码，总量约 1.8 亿行 Rocq 证明代码；单个证明典型规模约 60 万行，而它要保证的二进制中位数只有 1.8 万条 RISC-V 指令——证明比被证明的东西大了三十多倍，这也解释了为什么过去没人这么干。
看懂这份材料的关键，是把「证明了什么」和「在什么前提下证明」分开。附录把结论拆成三个定理，并且先用一句话定义了什么叫崩溃：访问未映射内存这类故障、断言失败这类中止、以及任何模型没描述的行为（比如用到了 Linux 语义里没定义的系统调用），三者任一即算崩溃。三个定理是：带 AddressSanitizer 的二进制对任何输入都不崩；带插桩和不带插桩的两个二进制行为等价；不带插桩的普通二进制同样不崩。
少任何一个都不够——只有第一个，普通用户跑的版本没被覆盖；只有第二和第三个，等价关系本身挡不住「两个都在崩但崩法不同」。
「行为等价」只比四样东西：标准输入读到的字节、标准输出与标准错误的字节、退出码或被什么信号终止、文件系统的最终状态。性能不在其中，报告承认这一点，但认为够用。还有个细节：程序崩溃时轨迹直接结束、不含崩溃本身，所以「一个崩、一个死循环」在定义上仍算等价——正因如此才需要第三个定理。
所以适用假设必须一条条摆清楚，这也是这份材料最容易被误读的地方：
- 输入：小于 64 MiB 的任意输入，覆盖所有内存布局；加大这个上限只是改参数重新生成规格，但报告只证到 64 MiB。
- 线程：单线程。多线程与并发不在范围内。
- 二进制形态：静态链接、链接的是 musl libc，不是多数人实际用的动态链接 glibc。
- 执行环境：RISC-V 处理器上的 Linux 进程模型，用的是一套公开的 Linux 进程形式语义。
- 覆盖范围：只覆盖被证的那些入口点，不是整个库；库里的死代码、以及调用方自己误用库导致的越界，都不在证明里。
发现的问题比「证明了什么」更有说服力，因为都是具体到能复现的：某库自带解压器里有一个计数器下溢，进而越界写，但只在约 20 MB、且内存布局极其特定的一种输入下触发——这类输入模糊测试基本碰不到，因为 fuzz 的变异输入通常卡在 1 MB 量级；一个图像解码器的越界读需要 64 MB 输入和 2 GB 以上内存才出现；另一个库的越界读要求对同一个文件的两个句柄按特定顺序调用；还有一个是 libexpat 里 CVE-2026-56132 的重新发现，需要极深的嵌套输入。
除了会崩的 bug，还找到一类根本不崩的逻辑问题：有个库用来限制「应用能加载哪些文件」的功能，并不是在所有路径上都生效。
正文另外三个实验值得单独看，因为它们展示了同一套方法的不同用法。一是给 zlib 写形式化规格：拿 RFC 1950 这个定义压缩格式的文档当规格，证明 Linux 内核里的实现符合它，而这次证的是 x86 二进制，用的是模型自己生成并反复测试过的 x86 指令语义。二是让模型用 Rust 写一个覆盖 Python 大子集的解释器，再用 Verus 证明它符合论文里描述的 CPython 语义，然后跑 170 万个随机生成的 Python 程序做实测，99.95% 行为一致，其余差异属于已知边角情形。
三是对一个广泛使用的 PDF 阅读器做简单安全性质的验证，一周内发现的安全问题数量，相当于平常一年被报告的量。
成本这块报告没有回避：单条证明可能消耗上亿 token。但两个降本因素都给了数字——同一批 36 个小任务上，Opus 5.5 比 Opus 5 少用约 40% 的 token 就证完一半；让多个智能体共享工作区、互相抄已完成的证明，比各自单干少用 17% 的 token，有的智能体本来单干失败、共享后成功了。共享之所以有效，是因为一份证明的大部分内容其实是每个程序都有的东西（C 运行时初始化、AddressSanitizer 相关部分），所以差异很大的程序，证明也有大量重合。
报告拿 Mathlib 作类比：那个 Lean 数学库靠每人往上叠，攒到了近 30 万条定理、七百多位贡献者。
局限部分是官方自己写的，比多数读者预期的更坦率。「形式验证通过」不等于「没有 bug」：证明检查器只能保证证明符合规格，没法保证规格符合现实；当被验证的代码仍然出问题时，原因通常是规格或者假设的机器语义与真实机器不一致——好在这也意味着知道该往哪里找。第二个缺口是「我们关心的性质未必被覆盖」：AddressSanitizer 本身检测不到全部内存安全 bug，每个库也没把入口点证全，就算证全了，整个库仍未必被覆盖，何况调用方误用还能在调用方那一侧造成内存破坏。
要补上，得为每个公开函数写清调用方必须遵守什么。
最后是公开范围，这点对做复现的人很重要：公开了本次新建、此前不公开的可信组件（RISC-V 与 Linux 进程的形式模型）、无需打补丁就证完的完整 Rocq 证明、以及证不下来的那些规格；但没有公开可能暴露未修补漏洞的证明。也就是说，仓库里的证明集合不等于「全部 239 个入口点」，缺的那部分恰恰是最有信息量的部分。
还有一处自我披露容易被跳过：模型在证明时能自己改代码，这留出了「作弊」口子——把程序改成永不崩溃，任何定理都成立。报告的应对是补丁一律扣分、对「能证明改动影响哪些输入、影响多小」额外加分，并把补丁记录下来做审计。做复现的人不看这一段，容易把「证明通过」当成纯粹的模型能力。
────────────────
研究原文、六页附录、三个仓库（含证明集合与 RISC-V／Linux 语义）的地址都列在下面，回帖就能看到。
京公网安备 11010802022788号
