Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明
LLMs are making formal software verification feasible at a much larger scale
Anthropic 与 Theorem 合作，用 Claude 将 OSS-Fuzz 模糊测试转化为规格，对 123 个开源库的 239 个入口点证明了任意 64 MB 以下输入不崩溃，生成约 1.8 亿行 Rocq 证明。
Anthropic 用 Claude 对 123 个 OSS-Fuzz 开源库在 RISC-V 汇编层面写 Rocq 证明，读者可以据此了解 LLM 规模化形式化验证的实际流程与局限。
Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross
大多数软件都充斥着缺陷，而如今 AI 能轻易地找出并利用这些缺陷。面对网络攻击，标准防御手段已经不够用了：我们需要能证明代码没有缺陷的办法。形式化软件验证本可以提供这种保证，但过去它需要专家投入数年精力，对大多数现实项目来说并不现实。不过，在与 Theorem 的合作中，我们证明情况已经改变：LLM 现在能大规模生成形式化证明，从而催生出带有可证明安全保障的全新软件开发流程。借助 Claude，我们在 100 多个真实开源软件库中，于汇编代码层面（RISC-V）证明了安全属性。据我们所知，这是首次大规模尝试用 AI 将形式化验证应用于生产软件的汇编代码层面。在编写证明的过程中，Claude 还发现了多年来一直未被察觉的缺陷，尽管这些代码已经过数万亿次测试运行。随着模型能力持续提升，我们预计形式化验证将成为安全软件开发中不可或缺的一环。
引言
即便是成熟且经过大量测试的软件也含有缺陷，而 LLM 越来越擅长找出它们。Linux 内核是当今测试最充分的软件之一，部署在全球数十亿台设备上，最近却披露了超过 1,000 个漏洞。随着前沿模型越来越能把看似无害的缺陷串联成严重漏洞利用，我们需要能在这些缺陷被野外利用之前发现并修复它们的技术。
理想情况下，这类技术能找出并修补所有缺陷，然后给出某种证明，说明再无缺陷可寻。形式化验证就是实现这一目标的一种方法。在形式化验证中，开发者把代码转换成数学模型，然后尝试证明它始终遵循某组既定的安全规则。如果证明失败，就意味着代码中可能存在违反规则的缺陷，而失败的性质也暗示了缺陷可能是什么。反复进行这一过程（每次消除失败原因之后），最终就能得到证明：代码中不存在任何会违反这些规则的缺陷。
然而，形式化验证并不容易。证明的规模可能比原始代码大许多倍，编写证明需要大量投入，而且属于小众、高度专业化的技能。例如，实现 seL4 操作系统内核用了两人年，而对其进行形式化验证用了20 人年。因此，形式化验证一直只在真正关键的任务中才具有可行性，比如空客的航空电子代码。
但大语言模型让这件事容易多了。前沿模型现在能够完全自主地为真实世界的软件生成正确性证明。为了演示这一点，我们让 Claude 为 123 个开源库证明有用的安全属性，包括证明其中一些可执行产物在某些条件下绝不会崩溃。具体来说，Claude 证明了：在特定假设下（即程序以单线程静态二进制形式运行、内存预算固定，运行在采用 Linux 操作系统的 RISC-V1 CPU 上），对于所有小于 64 MB 的输入，以及所有建模的 Linux 操作系统（OS）响应和内存布局，这些程序总能正常退出，不会触发内存安全错误，也不会出现断言失败。这距离修复所有可能的 bug 还很远，但确实比以往任何时候都更接近目标，也为实现这一目标提供了一份路线图。
我们公开了这些证明的一个子集，任何人都可以验证和复用，同时一并公开了RISC-V 与操作系统语义。本项目的合作方 Theorem 也愿意为其他开源项目运行同一套流程，并发布了一个 Claude 技能，帮助开发者上手验证自己的代码。
形式化验证是一个涵盖多种方法论的广阔领域。下面我们还会介绍一些初步探索：用其他形式化验证方法加速其他安全或软件开发任务，例如评估 zlib 压缩算法的安全性、证明用 Rust 编写的 Python 解释器行为等价，以及根除关键软件中长期存在的 bug。
形式化验证的前景值得期待。随着模型越来越智能，编写证明的成本正在下降。此外，随着更多代码被形式化、实现安全保障的方法日趋标准化，跨代码库复用或修改证明的能力将摊薄成本。我们鼓励所有开发者用大语言模型探索形式化验证——尤其是那些此前用能力较弱的模型尝试过、觉得行不通的人。
在本文余下部分，我们会更详细地介绍这些形式化验证实验。
把测试变成证明
要证明一段软件是正确的，首先得说清楚“正确”到底指什么。正确性由规约（spec）来定义。有些程序可以很清晰地形式化描述其预期行为。例如，PNG 解码器接收一串字节，并（按照 RFC 2083）把这些字节解码成对应的图像。但对大多数程序来说，事情没那么简单。一个文本编辑器或网页浏览器“正确”意味着什么？难以获得全面且无歧义的规约，是大规模验证软件的一大障碍。
为了对开源库中我们想要验证的代码做到这一点，我们采取的办法是：把开源库已有的可编译测试套件自动转换成一个规约，具体做法是把“这套测试永远通过”这条规则编码进去，并借助一个通用模型来描述在 Linux 上执行任意 RISC-V 编译二进制文件意味着什么。过去，证明这类规约是极其困难的，因为要写出一份证明，把数万条汇编指令在任意输入下的所有可能行为和交互都涵盖进去并加以论证，本身就极为复杂（而且由此产生的证明往往体量巨大）。这正是当今大语言模型（LLM）的用武之地：围绕一个定义明确的目标处理数百万行代码，恰恰是 LLM 极为擅长的事情。
在这个项目中，我们从模糊测试入手。在这类测试中，开发者会在代码里写一个入口点2来接收输入，只要某个输入导致崩溃，就是作者关心的 bug。随后，模糊测试器这个测试引擎会在入口点生成海量的半随机和变异输入，试图找出 bug（见图 1）。模糊测试器运行得越久，能发现的 bug 就越多。但这本质上是一种暴力搜索过程，无论尝试多少输入，都无法保证覆盖每一条可能的代码路径。
模糊测试的原理是：把大量生成的输入送进同一个入口点，找出会导致崩溃的输入。输入是无穷的，所以这种搜索永远不可能穷尽。
为了找出模糊测试本会暴露的所有 bug，我们把模糊测试转换成一个针对编译后 RISC-V 指令定义的规约。该规约规定：对于任何小于 64 MB 的输入，模糊测试都不会崩溃。3如果 Claude 能证明这个规约，那么针对 RISC-V 的模糊测试就变得多余了：对这个入口点做模糊测试永远不会发现任何 bug。
我们在 Google OSS-Fuzz 计划中的数百个项目上做了这件事。OSS-Fuzz 为符合条件的开源项目提供持续的模糊测试，其中包含数千个由开发者编写的入口点，它们通过让程序崩溃（例如断言失败）来发现代码属性被破坏的情况。OSS-Fuzz 会自动为 C 和 C++ 程序插桩 AddressSanitizer4（ASan），一旦内存被不当访问就让程序崩溃（这是软件漏洞的主要成因）。像内存安全这样的广谱规约几乎适用于所有软件。
开源库及其现有的模糊测试会被编译成 RISC-V 可执行文件。这个可执行文件，连同 Theorem 的 RISC-V 与操作系统形式化语义以及期望的“不崩溃”属性，会机械地生成一份证明必须满足的规约。Claude 负责写证明，Rocq 内核负责对照规约检查证明。绿色表示已获证明，前提是受信任的组件正确无误。
在几周时间里，Claude 成功修复了它发现的漏洞，随后证明：在 123 个不同的 OSS-Fuzz 库中，239 个入口点在任意输入（最大 64 MB）下都不会崩溃。这些证明针对的是编译后的 RISC-V 指令（即可执行二进制文件），总计约 1.8 亿行 Rocq 代码；对于中位长度为 18,000 条 RISC-V 指令的二进制文件，一份典型证明约有 60 万行，用以提供安全保障。这些证明的构建方式，是利用 Theorem 的 RISC-V 指令语义和 Linux 进程语义，把 RISC-V 汇编代码转换为数学模型。这意味着这些证明目前假设：程序以单线程静态二进制形式运行，内存预算固定，运行在采用 Linux 操作系统的 RISC-V CPU 上。扩大这些证明的适用范围完全触手可及，只需为更多汇编架构和其他操作系统进程制定标准化语义。关于 Claude 所写证明的专家点评，见此处。
覆盖所有输入的形式化无崩溃证明，排除了从入口点可达的任意路径上的所有崩溃。在反复迭代证明的过程中，Claude 还能发现并修复任何仍然可达、会导致崩溃的漏洞。
尽管证明代码体量巨大，但几乎不需要人工审查。Rocq 证明检查器会确保证明正确满足了规约。因此，开发者只需要信任以下几项产物：
- RISC-V 与 Linux 进程的形式化模型；
- 实际被证明的定理陈述；
- Rocq 证明检查器本身。5
这并不意味着这些库中没有漏洞。它的含义是：任何仍然存在的漏洞，要么位于上述产物之中，要么超出了 Claude 证明的覆盖范围。加固这些仍可能含有漏洞的可信组件（Rocq、RISC-V 和 Linux 语义）并非小事，但相比逐一调试大规模证明所覆盖的每一行代码，这项任务要可控得多——尤其是这种方法可以在不增大可信组件规模的前提下，保障任意数量项目的安全。
我们欢迎对本项目证明的独立验证，也鼓励改进我们的方法。为此，我们公开发布了本项目构建、此前尚未公开的可信组件（即上述各项）；Claude 为无需修复的模糊测试编写的完整 Rocq 证明；以及我们未能完成证明的其他模糊测试的规约。
发现并修复漏洞
上文已经说明，可以把许多开源库中由开发者编写的测试（模糊测试）转化为规约，让 Claude 证明这些规约始终成立——有时需要先修复它发现的剩余漏洞。正因如此，在尝试证明这些规约的过程中，一共发现了数百个漏洞。
在 Claude 尝试证明数百个入口点的过程中，大量漏洞浮出水面。为了确保 Claude 不必每次遇到这种情况都停下来等人，我们让 Claude 自行修复它发现的漏洞：它修补代码，规约随之基于修补后的代码重新生成，然后 Claude 继续证明新的规约。6
我们发现的许多 bug，模糊测试器几乎不可能找到。模糊测试器会变异小输入，通常上限为 1 MB，并且通常依赖代码覆盖率来引导它们找到 bug。在证明某个库的一个入口点时，Claude 在其解压器副本中发现了一个计数器下溢，导致越界写入，但只会在约 20 MB、具有一种罕见特定布局的输入上触发。其他 bug 包括：一个图像解码器中的越界读取，需要 64 MB 输入和超过 2 GB 内存；另一个库中的越界读取，需要对同一文件的两个句柄进行特定调用序列；以及 libexpat 中 CVE-2026-56132 的重新发现，需要深度嵌套的输入。Claude 还发现了根本不会导致崩溃的逻辑 bug。例如，在证明某个库内存安全时，它注意到一个用于限制应用程序可加载哪些文件的功能并不总是被执行。
这个项目的最终目标是证明 RISC-V 编译的模糊测试已没有剩余的崩溃可找。然而，上述这类 bug 表明，无论该目标是否达成，这个过程还有另一个好处：即使只是尝试这个过程，也会产生需要修复的真实 bug。
证明内存安全之外的东西
证明一个模糊测试没有更多崩溃可找，比听起来更有意义。现实世界代码中的模糊测试通常会测试是否违反有意义的高层属性，例如编码-解码往返、幂等性、代数定律、差分测试、自一致性，或与参考实现等价。例如，LZO 压缩算法的模糊测试断言：如果你压缩一个输入，然后解压它，结果与原始输入相同。如果该属性不成立，程序就会崩溃——因此证明测试永不崩溃，就等同于证明该属性本身。
即使属性不是由开发者直接指定的，也可能出现这种情况。例如，为了让 Claude 完成 cpp-httplib 的 OSS-Fuzz 证明，必须排除因 std::set 析构函数中递归过多而导致栈溢出的可能性。这个递归深度受树的最大深度限制，因此 Claude 必须（在机器码上！）证明 libc++ 的红黑树再平衡算法被正确优化，使树的深度保持对数级有界。
其他形式化验证案例研究
形式化验证是一个广阔的领域。上面的模糊测试到证明的例子，是 LLM 通过直接将证明应用于机器码，使形式化验证更广泛可用的一个实例。
我们还发现，把大语言模型和形式化验证结合起来，在其他场景下同样能取得不错的效果。比如，我们让 Claude 为 RFC 1950 写一份形式化规范——这份技术文档定义了 zlib 压缩文件格式。接着，我们让 Claude 证明 Linux 内核里的 zlib 实现确实正确地实现了这份规范。和上面几个例子一样，Claude 是在二进制层面完成证明的，只不过这次不是 RISC-V，而是直接用 Claude 生成的（并经过大量测试的）x86 指令集形式化语义，对 x86 编译出的二进制做了证明。7 之后我们又对另外六个广泛使用的库重复了这一流程。过程中，我们在一些边角情况里发现了几个轻微（无法被利用）的 bug，目前正在向上游提交。这次尝试让我们得出两个结论：（1）这些经过极其充分测试的代码库其实已经几乎完全正确；（2）针对真实存在的代码库，端到端地证明其正确性属性是可行的。
在另一项实验中，我们让 Claude 用 Rust 写一个覆盖 Python 大部分子集的解释器，并证明（借助 Verus 这个 Rust 验证工具）它符合一篇学术论文中描述的 CPython 语义。随后我们又用实测的方式衡量它对 CPython 行为的符合程度：跑了超过 170 万个随机生成的 Python 程序，其中 99.95% 的测试与 CPython 行为完全一致，剩下的差异都是意料之中的已知边角情况。
我们还尝试对几个广泛使用且至关重要的应用做简单安全属性的形式化验证，结果发现了不少问题。其中一个应用里，我们找到一个此前未知的逻辑 bug，它已经潜伏了十多年。在验证一款广泛使用的 PDF 阅读器时，我们一周内发现的安全 bug 数量，抵得上通常一整年的报告量。
部分工作的更多细节见附录。
这只是开始
大语言模型辅助形式化验证的一个关键局限在于，生成证明可能要消耗数亿个 token。如果我们的目标是让整个软件生态都能用上这些方法，成本效率就至关重要。好在有充分理由相信效率会不断提升。
新模型需要的 token 更少
我们基于真实的 OSS-Fuzz 代码构建了 36 个小型验证任务。Opus 5.5 能证明其中一半，而消耗的 token 比 Opus 5 少约 40%。随着模型在长验证任务上接受训练，我们预计这一趋势会延续下去。
Opus 5.5 完成证明的速度快于早期模型。图中展示在给定 token 预算下，单个智能体证明的 36 个形式化验证任务所占比例。每个任务在 500 万 token 预算下获得三次独立的单智能体尝试，首次尝试完成即计为已证明。
证明可以复用
智能体各自独立工作时，往往会重复大量劳动。证明和软件一样，是由更小的证明递归构建而成的——而证明越小，通常越容易复用。为了衡量这一点的影响，我们让智能体在证明各自目标的过程中可以互相复制对方的证明。有了这个共享工作区之后，智能体所需的 token 比单独工作时少了 17%，有些智能体甚至在单独尝试失败后，借助共享工作区取得了成功。
来自同一个共享工作区的 36 个证明，按完成顺序排列。若两个证明共享一个未改动的文件，就用一条弧线把它们连起来；柱形表示编写每个证明所消耗的 token 数，黑线表示同一任务由单个智能体独立完成时的平均成本——在 34 个已完成的证明中，有 30 个的成本高于团队协作（独立工作的智能体有两个证明未能完成）。
在 OSS-Fuzz 证明工作中，我们在大规模场景下观察到了同样的现象。一个证明的大部分内容都涉及每个程序都有的代码（尤其是 C 运行时和 AddressSanitizer 的初始化），因此差异很大的程序，其证明也可能出现大量重叠。智能体团队正是利用了这一点：复制另一个团队已完成的证明，再改写适配自己的程序（图 6）。
智能体复制已有证明，再改写适配每个新程序。每一列代表一个程序的完整证明，按字节占比划分。色块是证明的各个部分，每块显示其中有多少保持完全相同、轻度修改（同一文件，大小差异在 2% 以内）、修改较多或全新编写。共享部分几乎没有新增代码。
证明的这种可复用性，正是 Lean 形式化数学共享库 Mathlib 发展到近 30 万条定理、由 700 多名贡献者提交的原因：每个新证明都建立在已有成果之上。在 OSS-Fuzz 工作中，我们也积累了类似的证明库，其中一部分会随本次发布一并公开（可能暴露开源软件中未修复漏洞的证明不予发布）。
在走出这些初期实验之后，我们需要一套策略来验证海量的现有软件，从最关键的依赖开始。正如我们所展示的，借助通用规格说明、在二进制层面开展工作，就能大规模实现这一目标，无需用另一种语言重写整个代码库。
这种方法还便于以软件包为粒度复用证明，也就是说每个依赖只需验证一次。依赖关系遵循幂律：只要证明少量共享库，就能让一大片软件变得可证明。更多细节见 Theorem 的路线图，其中规划了如何验证整个 Nix 生态，包括 glibc、OpenSSL 和 cURL 等关键基础设施。
局限
在实践中，形式化验证有时能揭示的代码安全性问题比我们期望的要少。
“形式化验证”不等于“没有缺陷”。Claude 可以写出一个证明，表明编译后程序的行为满足形式化规格说明的要求（该证明由外部证明检查器验证）。但证明检查器无法告诉你规格说明是否符合现实。要与现实相符，规格说明必须正确涵盖并建模被验证程序所运行的真实机器的方方面面，包括 CPU 和操作系统。当已验证的代码中出现缺陷时，原因在于规格说明或假定的机器语义与现实不符。幸运的是，这也意味着我们知道该去哪里寻找残留缺陷，以及如何设计系统来尽量缩小这些仍可能藏有缺陷的缺口。下面说明这一点如何适用于我们的证明，以及未来工作中有望弥合这些缺口的思路。
真实机器做的事，模型并没有描述。我们的证明针对的是单线程、静态链接 musl libc 的 RISC-V 二进制文件。但大多数人是在 x86 或 ARM 上运行这些库，并动态链接 glibc。要弥合这一差距，我们需要更贴近实际部署系统的系统模型。比如，为 x86 生成精确的语义，就是朝这个方向迈出的一步。
这一结论可能没有覆盖我们关心的全部内容。我们证明了，在 Google OSS-Fuzz 的许多模糊测试入口点上，对于任何小于 64 MB 的输入，崩溃都不会触发，包括 ASan 崩溃。但 ASan 并不能检测出所有内存安全缺陷，而且我们也没有逐一验证每个库的所有入口点。即便验证了，验证所有入口点也无法覆盖整个库（尤其是有死代码时）。此外，真实程序可能误用库，导致调用方出现内存损坏。要弥合这一差距，我们需要明确每个公开函数对调用方的要求，而调用方必须严格遵守。
我们预计，随着我们对如何利用大语言模型服务形式化方法的了解不断深入，以及模型持续改进，这些局限将变得可控，我们也将能够验证我们所依赖代码中更大比例的部分。
结论
趋势已经很清楚：形式化验证过去只适用于在最关键安全代码中由专家手工打造的特制保证，而很快，它就会像今天的模糊测试一样，适用于几乎所有生产软件。就像静态类型、测试框架和其他正确性工具一样，验证将从“外挂式”走向“内置式”，推动这一转变的不仅有大语言模型，还有语言设计和开发工作流的创新。
在当今世界，大语言模型会自动扫描并发现越来越多的代码漏洞，我们必须采用能够保证代码安全属性的流程。LLM 规模化的形式化验证是一种很有前景的方法，有望在以往无法企及的范围和规模上确保这些保证。我们鼓励其他人也来尝试，这样我们就能共同构建一个世界：健壮的软件广泛普及，软件缺陷成为人们充分理解、能够快速处理的罕见现象。
来源：Anthropic：Research · anthropic.com