Anthropic用Claude自动生成1.8亿行证明根除软件崩溃
AI技术投降派
随着AI将形式化验证的编写成本推向历史拐点，原本仅用于航天等极少数场景的“无Bug数学证明”正成为软件开发的内置基础设施。
AI-assisted summary of AI给123个代码库写不崩溃证明，数学级别 — original source. Check the original for full context.
Source published:
Key ideas
- Anthropic 联合初创公司 Theorem 利用 Claude 针对 123 个开源库的 239 个测试入口生成数学证明，确保在小于 64MB 输入下程序绝不崩溃，通过改名后的 Rocq 校验约 1.8 亿行证明代码。 (0:00)
- 形式化验证流水线直接在 RISC-V 底层机器码上展开，平均每条机器指令配有 30 余行证明，成功找出数百个模糊测试因输入阈值（如超 20MB）或复杂资源竞争无法触发的深层漏洞并完成修复。 (2:34)
- 当前验证存在显著边界：仅覆盖单线程、静态链接的 RISC-V + Linux 环境且仅证明“不崩溃”而非“功能正确”；公开 GitHub 仓库目前仅涵盖 25 个库的 60 个入口。 (4:49)
- Claude 3.5 Opus 在证明生成效率上提升了约 40%，多 Agent 经验复用降低了 17% 算力开销，验证成本曲线拐头或将推动形式化验证从航天专用转变为内置的开发基础设施。 (5:55)
Detailed notes
## Background 该视频由 Bilibili 频道“AI技术投降派”于2026年10月25日发布。视频简介引用了迪杰斯特拉关于“程序测试无法证明 bug 不存在”的名言，重点介绍了 Anthropic 使用 Claude 在几周内为123个开源库的239个测试入口写出数学证明，论证了只要输入小于 64MB 程序便不会崩溃，并拆解了其流水线、实战战果与边界条件。
## TL;DR 视频深入探讨了 Anthropic 联手 Theorem 利用大模型推动形式化验证工业化落地的技术突破。不同于传统模糊测试的随机抽查，Claude 通过将 RISC-V 底层机器码转译为数学定理，并借助 Rocq 严格检查器生成了约 1.8 亿行数学证明，排查并修复了大量万亿次模糊测试都无法触及的刁钻深层漏洞。视频同时保持严谨清醒，算清了单线程 Linux 环境限制、“不崩溃非功能正确”以及开源子集等现实局限，指出形式化验证的成本曲线已迎来历史性拐点。
## Atmosphere & style 整体基调严谨扎实、理性客观且不失极客式的震撼感。主讲人以计算机科学史上的著名论断切入，叙事条理清晰、抽丝剥茧，既展现出技术范式被颠覆时的兴奋，又极其克制地用“诚实账本”泼冷水。整场解说充满技术硬核感与现实穿透力，让观众在见证 AI 解决工业级工程难题的同时，清醒意识到技术理想与物理现实之间的距离。
## Bulletin - [00:00](https://www.bilibili.com/video/BV1DSn46jELa?t=0s) Anthropic 联合初创公司 Theorem 利用 Claude 针对 123 个开源库的 239 个测试入口生成数学证明，确保在小于 64MB 输入下程序绝不崩溃，通过改名后的 Rocq 校验约 1.8 亿行证明代码。 - [02:34](https://www.bilibili.com/video/BV1DSn46jELa?t=154s) 形式化验证流水线直接在 RISC-V 底层机器码上展开，平均每条机器指令配有 30 余行证明，成功找出数百个模糊测试因输入阈值（如超 20MB）或复杂资源竞争无法触发的深层漏洞并完成修复。 - [04:49](https://www.bilibili.com/video/BV1DSn46jELa?t=289s) 当前验证存在显著边界：仅覆盖单线程、静态链接的 RISC-V + Linux 环境且仅证明“不崩溃”而非“功能正确”；公开 GitHub 仓库目前仅涵盖 25 个库的 60 个入口。 - [05:55](https://www.bilibili.com/video/BV1DSn46jELa?t=355s) Claude 3.5 Opus 在证明生成效率上提升了约 40%，多 Agent 经验复用降低了 17% 算力开销，验证成本曲线拐头或将推动形式化验证从航天专用转变为内置的开发基础设施。
## Key takeaways - [00:00](https://www.bilibili.com/video/BV1DSn46jELa?t=0s) 传统模糊测试（Fuzzing）本质属于概率抽查，即使如 OSS-Fuzz 累计进行万亿次测试，也无法突破迪杰斯特拉“测试无法证明 bug 不存在”的理论死穴。 - [00:47](https://www.bilibili.com/video/BV1DSn46jELa?t=47s) 形式化验证将程序与安全属性转化为纯数学定理，通过穷尽所有边界情况获得绝对全覆盖，但此前受制于极度高昂的人力与时间成本。 - [01:45](https://www.bilibili.com/video/BV1DSn46jELa?t=105s) 以 2009 年验证 seL4 微内核为例，仅 8700 行 C 代码消耗了 20 人年，高成本导致通用软件长期无法采用形式化验证来根治占漏洞七成的内存安全问题。 - [02:34](https://www.bilibili.com/video/BV1DSn46jELa?t=154s) Anthropic 验证流水线避开容易引发歧义的高层 C/C++ 源码，直接编译为 RISC-V 机器码作为验证对象，从底层指令级别构建数学定理。 - [03:05](https://www.bilibili.com/video/BV1DSn46jELa?t=185s) 交互式定理证明器 Rocq 的检查内核独立校验证明逻辑，Claude 生成的约 10 亿行证明中有 1.8 亿行通过，过程完全无需人类介入审查。 - [03:35](https://www.bilibili.com/video/BV1DSn46jELa?t=215s) 验证体量达到平均一条二进制指令对应 30 多行证明，证明难度并未降低，本质变革在于由 AI 替代了极其稀缺的形式化验证专家。 - [03:52](https://www.bilibili.com/video/BV1DSn46jELa?t=232s) 证明过程挖掘出模糊测试无法覆盖的漏洞，包括需要 20MB 罕见布局下溢的越界写入、高内存（2GB）占用读取及双句柄调用顺序缺陷。 - [04:25](https://www.bilibili.com/video/BV1DSn46jELa?t=265s) 流水线还复现了 libexpat 的已知 CVE，并抓出未崩溃但违背敏感文件加载限制策略的深层逻辑缺陷，所有问题均由 Claude 自动修补后再重新证明。 - [04:49](https://www.bilibili.com/video/BV1DSn46jELa?t=289s) 现阶段证明存在严格前提边界：仅适用于单线程、静态链接的 RISC-V Linux 环境，普通用户普遍使用的 x86/ARM 架构及动态 glibc 不在证明范围内。 - [05:15](https://www.bilibili.com/video/BV1DSn46jELa?t=315s) 验证范围被严格限定在“程序不崩溃”，绝不代表“功能业务正确”，如哈希计算错误或伪随机数偏差等逻辑缺陷均不在防线之内。 - [05:32](https://www.bilibili.com/video/BV1DSn46jELa?t=332s) 官方博客声称的 123 个库 239 个入口在 GitHub 上仅开源了 25 个库 60 个入口，社区对定理陈述与物理现实环境的映射边界仍存质疑。 - [06:20](https://www.bilibili.com/video/BV1DSn46jELa?t=380s) 多 Agent 协作展现出经验复用优势，不仅能攻克单一 Agent 无法解决的复杂证明，还直接降低了 17% 的 Token 算力消耗。 - [06:45](https://www.bilibili.com/video/BV1DSn46jELa?t=405s) Theorem 与 Anthropic 展现出将 Nix 生态乃至 glibc、curl 底层软件全面形式化验证的野心，预示着形式化验证正由奢侈的“事后修补”转变为研发的“内置基础设施”。
## Detailed walkthrough ### [00:00](https://www.bilibili.com/video/BV1DSn46jELa?t=0s) 引言与原理：迪杰斯特拉的预言与形式化验证
1970年，计算机科学家艾兹格·迪杰斯特拉（Edsger W. Dijkstra）留下一句振聋发聩的名言：“程序测试可以证明 bug 的存在，但永远不能证明 bug 的不存在。”半个多世纪以来，整个软件工程界几乎都活在这句话的阴影下。2026年10月22日，Anthropic 发布了一篇标题很长但核心极其震撼的博客：大模型正在把形式化验证推向规模化应用。Claude 在短短几周之内，给 123 个开源库的 239 个测试入口写出了严格的数学证明——任何小于 64MB 的输入，都不会让程序发生崩溃。
这件事之所以极其反常识，在于它颠覆了常规的找 bug 逻辑。平时业界抓 bug 主要靠测试，尤其是模糊测试（Fuzzing）：依靠机器疯狂生成海量的随机输入往程序里硬塞，一旦塞崩了就逮到一个漏洞。比如谷歌旗下的 OSS-Fuzz 项目，从 2016 年一直跑到今天，累计运行了上万亿次测试。然而迪杰斯特拉早就点破了死穴：模糊测试本质上是“抽查”。即便测试了一亿个输入没有崩溃，第一亿零一个输入照样可能让系统宕机；由于可能的输入组合有无穷多个，抽样排查永远存在漏网之鱼。形式化验证则走向了一条完全不同的道路：把程序翻译成数学对象，把“程序不崩溃”转化为一个数学定理，然后像解数学几何题一样穷尽所有边界情况，证明定理绝对成立。证明一旦跑通，覆盖的就是该范围内的全部输入，而非概率抽样。
```mermaid flowchart TD accTitle: 模糊测试与形式化验证对比 accDescr: 对比传统模糊测试的随机抽查与形式化验证的数学定理全覆盖路径
subgraph Fuzzing["传统路径：模糊测试 (Fuzzing)"] A["生成随机输入"] --> B["海量抽查 (万亿次测试)"] B --> C["抓取崩溃 Bug"] C -.->|"局限"| D["抽样永远有漏网之鱼"] end
subgraph Formal["颠覆路径：形式化验证 (Claude + Rocq)"] E["程序二进制"] --> F["转译为数学对象与定理"] F --> G["穷尽逻辑证明 (约1.8亿行证明)"] G --> H["绝对覆盖全部有效输入"] end ```
[01:45](https://www.bilibili.com/video/BV1DSn46jELa?t=105s) 旧账：seL4 的二十人年与高昂的验证代价
形式化验证这条路在计算机科学史上一直存在，但过去几十年它有一个致命弱点：成本高昂到了极致。业内最著名的教科书级案例是 seL4 操作系统微内核——澳大利亚团队在 2009 年做出了世界上第一个经过完整形式化验证的操作系统内核。这个内核本身只有区区 8700 行 C 代码，写代码本身花费了两年人力；但为了完成它的形式化验证，团队足足耗费了“20人年”的时间，写出的证明代码高达约 20 万行。换算下来，“写代码花两份时间，证明花十份时间”。
正因为这种夸张的成本，半个世纪以来形式化验证几乎只属于不惜一切代价的极少数场景，比如航天飞行器、飞机航电系统以及顶级密码学库，通用软件根本无力承担。微软和谷歌两家巨头都曾统计过，自家产品大约七成的安全漏洞归根结底都是内存安全问题。各大软件厂商明知道形式化验证能彻底根治内存漏洞，可现实就是“验证不起”。
[02:34](https://www.bilibili.com/video/BV1DSn46jELa?t=154s) 方法：从 RISC-V 二进制到 Rocq 的 Q.E.D.
面对高耸的成本高墙，Anthropic 联合形式化验证初创公司 Theorem 跑通了一条工业化验证流水线。整套方法分为严谨的三步： 1. **编译机器码**：将开源库及其模糊测试用例统一编译成 RISC-V 处理器的机器码。这里的关键细节在于，验证针对的并非容易产生歧义的 C/C++ 源代码，而是经过编译器处理后的真实底层二进制指令； 2. **构建数学定理**：将“该测试入口对于任何小于 64MB 的输入都不会引发崩溃”准确地形式化为一个数学定理； 3. **由 AI 编写证明**：交由 Claude 撰写证明。证明使用改名后的 Rocq（即数学界著名的交互式定理证明助手 Coq）进行逐行检查。
Rocq 内部包含一个铁面无私的检查内核（Kernel），无论证明过程写得多么花哨，逻辑上只要出现半步漏洞就会直接拒收。因此，系统完全不需要人类工程师去人工审查 Claude 写出的每一行证明代码。在整轮验证实验中，Claude 累计写下了约 10 亿行证明代码，最终成功通过 Rocq 严格检查器的约有 1.8 亿行，单个入口的证明平均长达 60 万行。与之相对，被验证的二进制指令中位数其实只有 1.8 万条——平均一条机器指令需要配 30 多行证明，与当年验证 seL4 的证明体量处于同一数量级。形式化验证本身的数学难度并没有降低，唯一的质变在于：“证明没有变简单，变得是写证明的人，以前是稀缺的形式化验证专家，现在是 Claude。”
[03:52](https://www.bilibili.com/video/BV1DSn46jELa?t=232s) 战果：翻出模糊测试错过的深层漏洞
在大规模推导证明的过程中，Claude 顺带把大量模糊测试几十年来都没能发现的漏洞给一锅端了。这些漏洞极其刁钻： - **罕见布局与超大输入**：某个开源库自带的解压器中存在计数器下溢缺陷，会导致严重的越界写入。但该 bug 必须在输入数据达到约 20MB 且内部数据布局极其罕见时才会触发；而传统的模糊测试输入上限通常只有 1MB，在物理维度上就根本够不着触发条件。 - **高内存与特定资源竞争**：一个图像解码器的越界读取 bug，需要塞入 64MB 输入并占用 2GB 内存才会发生；另一个 bug 则要求针对同一个文件的两个句柄按照严苛的先后顺序交替调用。 - **复现已知 CVE 与深层逻辑 Bug**：验证流水线成功复现了 libexpat 的已知 CVE 安全漏洞，甚至找出了许多“不引发崩溃但破坏安全策略”的逻辑 bug。例如，某个库宣称具有“限制加载特定敏感文件”的防御功能，但在实际代码实现中该限制逻辑根本没有被真正执行。
在这套流水线下，类似问题被抓出了数百个，并且全部由 Claude 先自动修复漏洞代码，再重新针对修复版本进行完整证明。以某个知名 PDF 阅读器为例，Claude 仅用一周时间找出的安全漏洞数量，就抵得上过去一整年社区报告的总和。
[04:49](https://www.bilibili.com/video/BV1DSn46jELa?t=289s) 边界：必须算清的“诚实账本”
尽管成果惊人，主讲人强调必须冷静客观地拉开这份“诚实账本”，形式化验证通过绝不等于完全没有 bug，背后存在多项极其严格的先决条件与现实鸿沟： - **运行环境前提极其严苛**：证明仅仅覆盖所声明的前提——单线程、静态链接在 RISC-V + Linux 环境下，并且假定内存预算固定。而绝大多数普通用户的电脑跑的是 x86 或 ARM 架构，动态链接 glibc 的系统并不在验证的证明范围之内。 - **“不崩溃”不等于“功能正确”**：数学定理所锁定的只是“程序不崩溃”，完全不涉及更高维度的业务逻辑正确性。假如程序把哈希值算错，或者密码学随机数发生器“不够随机”，这些逻辑缺陷在不崩溃的证明体系下一概不管。 - **入口不代表全库**：239 个验证入口只是特定的调用路径，入口之外依然存在大量未经验证的代码，至于死代码更是永远不会被测试覆盖。 - **开源代码与声称口径存疑**：博客宣传中写的是 123 个库、239 个测试入口，但公开推送到 GitHub 仓库的证明其实只是一个子集，仅包含 25 个库的 60 个入口，其余内容暂未开源。这引发了 Hacker News 社区工程师的尖锐质疑：万一定理陈述本身的边界条件就写错了呢？模型设定与物理真实世界之间的断层，正受到开源社区的严密审视。
[05:55](https://www.bilibili.com/video/BV1DSn46jELa?t=355s) 趋势：成本曲线拐头与内置化未来
在技术演进速度方面，Anthropic 选取了 36 个验证任务专门评估模型的迭代效率。数据显示，新一代 Claude 3.5 Opus 比上一代模型完成形式化证明的速度提升了约 40% 的 Token 效率。与此同时，证明经验还展现出了强大的复用潜力：让多个 AI Agent 之间“互相抄作业”，直接省去了 17% 的算力开销；更有两项极其复杂的验证任务单打独斗完全解不出来，唯有多个 Agent 协作验证才最终破局。
初创公司 Theorem 的路线图甚至更加激进，计划形式化验证整个 Nix 生态系统，从 glibc、OpenSSL 再到 curl 等现代互联网的“地基级软件”统统囊括在内。Anthropic 官方给出的终局判断是：形式化验证未来绝不会再是系统上线后亡羊补补牢的“事后补丁”，而是会像静态类型检查、单元测试框架一样，成为软件开发流程中内置默认的基础设施。
正如主讲人总结道：“质变还没有到，前提仍然苛刻，覆盖仍然有限，但成本曲线已经拐头。”半个多世纪前，迪杰斯特拉宣告测试只能证明有 bug；过去五十年，后半句“证明没有 bug”贵到全人类几乎没人能大规模用得起；而今天，随着证明生成任务被规模化外包给 AI，软件验证的经济账终于迎来了历史性的拐点。
## Notable quotes > [02:34](https://www.bilibili.com/video/BV1DSn46jELa?t=154s) 证明没有变简单，变得是写证明的人，以前是稀缺的形式化验证专家，现在是 Claude。
> [05:55](https://www.bilibili.com/video/BV1DSn46jELa?t=355s) 质变还没有到，前提仍然苛刻，覆盖仍然有限，但成本曲线已经拐头。
## Mentioned Edsger W. Dijkstra, Anthropic, Claude, Claude 3.5 Opus, Theorem, Rocq, Coq, seL4, OSS-Fuzz, Google, Microsoft, RISC-V, x86, ARM, Linux, glibc, libexpat, OpenSSL, curl, Nix, Hacker News
## Video description 一九七零年，迪杰斯特拉留下一句话：程序测试可以证明 bug 的存在，但永远不能证明 bug 的不存在。昨天，Anthropic 把后半句往前推了一大步：Claude 在几周之内，给一百二十三个开源库的二百三十九个测试入口写出了数学证明——任何小于六十四MB的输入，程序都不会崩溃。证明直接写在编译后的 RISC-V 机器码上，由 Rocq（改名后的 Coq）的内核逐行检查，约一亿八千万行证明通过验证，几乎不需要人工审查。
作为对比：二零零九年验证 seL4 操作系统内核，八千七百行 C 代码花了二十人年。写证明这个"只有航天和航电才用得起"的奢侈活，正在变成 AI 的日常任务。顺带的战果也很实在：万亿次模糊测试都没发现的漏洞（二十MB罕见布局才触发的越界写入、需要双句柄配合的越界读取），被证明过程一个个翻了出来，共数百个，Claude 自己修掉再重新证明。
当然，账要算诚实：证明只覆盖单线程 RISC-V 加 Linux 的前提，你的 x86 电脑不在范围内；证的是"不崩溃"，不是"功能对"；博客宣称的一百二十三库，公开发布的证明只有二十五库六十个入口。这期视频从 Dijkstra 的名言讲起，拆解证明流水线、战果与全部边界条件。
00:05 引言：迪杰斯特拉与昨天的新闻 00:47 原理：抽查与穷尽的区别 01:45 旧账：seL4 的二十人年 02:34 方法：从二进制到 QED 03:52 战果：漏网之鱼一锅端 04:49 边界：诚实账本 05:55 趋势：成本曲线拐头
[Source](https://www.bilibili.com/video/BV1DSn46jELa)