大多数软件都充满缺陷，人工智能（AI）如今能轻松发现并利用它们。针对网络攻击的标准防御已不再足够，我们需要证明代码无缺陷的方法。形式化软件验证原本要专家耗时数年，难以用于真实世界项目；但与定理（Theorem）合作后，大语言模型（LLM）已能大规模生成形式化证明。借助克劳德（Claude），我们在100多个真实世界开源软件库的汇编代码层（RISC-V）证明了安全属性。

大多数软件都充斥着 bug，而 AI 现在已能轻松发现并利用这些 bug。传统的网络攻击防御手段已不再充分：我们需要方法来证明代码没有 bug。形式化软件验证可以提供这种保证，但它历来需要专家付出数年努力，因此对于大多数实际项目来说并不实用。不过，在与 Theorem 的合作中，我们发现情况已不再如此：LLM 现在能够大规模生成形式化证明，从而实现包含已证明安全保证的新软件开发工作流。我们使用 Claude，在 100 多个真实开源软件库的汇编代码级（RISC-V）证明了安全属性。据我们所知，这是首个利用 AI 在生产软件的汇编代码级应用形式化验证的大规模尝试。在编写证明的过程中，Claude 还发现了多个躲过了多年检测的 bug——尽管此前已有数万亿次测试运行。随着模型能力持续提升，我们预计形式化验证将成为安全软件开发的重要组成部分。

引言

即便是成熟且经过充分测试的软件也存在 bug，而 LLM 正越来越擅长发现它们。Linux 内核是当今测试最充分的软件之一，部署在全球数十亿台设备上，但最近披露了超过 1000 个漏洞。随着前沿模型越来越有能力将看似无害的 bug 串联成关键漏洞利用，我们需要能在这些 bug 被野外利用之前检测并修复它们的技术。

理想情况下，此类技术可以找到并修补所有 bug，然后提供某种证明，表明再没有 bug 可找。形式化验证就是实现这一目标的一种方法。在形式化验证中，开发者将代码转化为数学模型，然后尝试证明它始终遵循一组定义好的安全规则。如果无法证明，就意味着代码中可能存在违反规则的 bug，而失败的性质暗示了 bug 可能是什么。在每次消除失败原因后重复这一过程，最终将证明代码不存在任何会违反这些规则的 bug。

然而，形式化验证并不容易。证明的规模可能是原始代码的许多倍，编写它们需要大量努力以及小众且高度专业化的技能。例如，实现 seL4 操作系统内核花了两人年，但对其进行形式化验证却花了 20 人年。因此，形式化验证以往只适用于真正关键任务的应用，例如空客的航空电子代码。

但 LLM 正使其变得容易得多。前沿模型现在可以完全自主地为真实软件生成正确性证明。为了证明这一点，我们让 Claude 在 123 个开源库中证明有用的安全属性，包括展示它们的某些可执行产物在特定条件下永不崩溃。具体来说，Claude 证明了对于每一个小于 64 MB 的输入，以及每一种建模的 Linux 操作系统（OS）响应和内存布局，这些程序在以下假设下（即程序在 RISC-V CPU 上使用 Linux OS，作为具有固定内存预算的单线程静态二进制文件运行）将始终正常退出，不触发内存安全错误或失败断言。这距离修复所有可能的 bug 仍很遥远，但它让我们比以往更接近目标，并提供了实现该目标的路线图。

我们发布了其中一部分证明，以及 RISC-V 和 OS 语义，以便任何人都可以验证和重用它们。本项目的合作方 Theorem 还提出为其他开源项目运行相同的流程，并发布了一个 Claude 技能，帮助开发者开始验证自己的代码。

形式化验证是一个拥有多种方法论的广泛领域。下面我们还描述了使用其他形式化验证方法加速其他安全或软件开发任务的初步探索，例如评估 zlib 压缩算法的安全性、证明用 Rust 编写的 Python 解释器的行为等价性，以及根除关键软件中长期存在的 bug。

形式化验证的未来前景广阔。随着模型变得更智能，编写证明的成本正在下降。此外，随着更多代码被形式化，以及实现安全保证的方法变得更加标准化，跨代码库重用或修改证明的能力将摊平成本。我们鼓励所有开发者用 LLM 探索形式化验证——尤其是那些以前用能力较弱的模型尝试过并发现行不通的人。

下文将更详细地介绍我们的形式化验证实验。

将测试转化为证明

要证明一个软件是正确的，我们必须首先说明“正确”的含义。正确性由规范（spec）定义。在某些程序中，有一种清晰的方式来正式指定程序的预期行为。例如，PNG 解码器接收一个字节序列，并（遵循 RFC 2083）将这些字节解码为相应的图像。但对大多数程序来说，事情没那么简单。文本编辑器或网页浏览器“正确”意味着什么？获得全面且无歧义规范的难度，是大规模验证软件的一个重大障碍。

为了在我们试图证明的开源库代码中解决这个问题，我们采取了一种方法：使用在 Linux 上执行任何 RISC-V 编译二进制文件的通用模型，通过编码“该测试套件始终通过”这一规则，将其预先存在的可编译测试套件自动转换为规范。从历史上看，证明此类规范是棘手的，因为编写一个能涵盖并对任意输入下数万条汇编指令的所有可能行为和交互进行论证的证明，本身具有内在的复杂性（而且证明往往因此变得极其庞大）。这正是当今 LLM 的用武之地：为了一个明确定义的目标而处理数百万行代码，是 LLM 极其擅长的任务。

在这个项目中，我们从模糊测试（fuzz tests）开始。在这些测试中，开发者在代码中编写一个入口点（entry point）来接收输入，任何导致崩溃的输入都是作者关心的 bug。然后，模糊测试器（fuzzer）作为一种测试引擎，在入口点生成大量半随机和变异的输入以试图发现 bug（如图 1 所示）。模糊测试器运行的时间越长，能发现的 bug 就越多。但这本质上是一个暴力过程，无论尝试多少输入，都无法保证覆盖每一条可能的代码路径。

为了找出模糊测试可能暴露的所有 bug，我们将模糊测试转换为定义在编译后 RISC-V 指令上的规范。该规范规定，对于任何小于 64 MB 的输入，模糊测试都不会崩溃。如果 Claude 能证明这个规范，那么在 RISC-V 上的模糊测试就变得多余了：对那个入口点进行模糊测试将永远找不到任何 bug。

我们在 Google 的 OSS-Fuzz 计划中对数百个项目进行了此操作，该计划为符合条件的开源项目提供持续模糊测试。OSS-Fuzz 包含数千个开发者编写的入口点，这些入口点通过崩溃（例如断言失败）来寻找被破坏的代码属性。OSS-Fuzz 会自动为 C 和 C++ 程序插桩 AddressSanitizer（ASan），使其在内存被不当访问时崩溃（这是软件漏洞的主要成因）。像内存安全这样的广泛规范几乎适用于所有软件。

在几周时间里，Claude 成功修补了它发现的 bug，然后证明了在 123 个不同 OSS-Fuzz 库的 239 个入口点上，对于任何输入（最大 64 MB）都不会发生崩溃。这些证明作用于编译后的 RISC-V 指令（即可执行二进制文件），包含约 1.8 亿行 Rocq 代码，典型的证明长达约 60 万行，用于为中位数长度为 18,000 条 RISC-V 指令的二进制文件提供安全保障。这些证明是借助 Theorem 的 RISC-V 指令和 Linux 进程语义，将 RISC-V 汇编代码转换为数学模型来构建的。这意味着这些证明目前假设程序在 RISC-V CPU 上使用 Linux OS，作为具有固定内存预算的单线程静态二进制文件运行。扩大这些证明的范围完全可行，因为这将涉及为更多汇编架构和其他操作系统进程标准化语义。

尽管证明代码量巨大，但几乎不需要人工审查。Rocq 证明检查器确保证明正确满足了规范。因此，开发者唯一需要信任的产物是：RISC-V 和 Linux 进程的形式化模型；被证明的确切定理陈述；以及 Rocq 证明检查器本身。

这并不意味着这些库没有 bug。相反，这意味着任何剩余的 bug 要么存在于上述产物中，要么超出了 Claude 证明的范围。加固那些仍可能存在 bug 的可信组件（Rocq、RISC-V 和 Linux 语义）并非易事，但这比调试大规模证明所覆盖的每一行代码要容易得多——尤其是因为这种方法可以保护任意数量的项目，而不会增加可信组件的规模。

我们欢迎对我们的证明进行独立验证，并鼓励改进我们的方法。为此，我们发布了为本项目制作的、尚未公开的可信组件；Claude 针对无需修补的模糊测试编写的完整 Rocq 证明；以及我们未能证明的其他模糊测试的规范。

发现并修复 bug

上文表明，我们可以将许多开源库开发者编写的测试（模糊测试）转化为规范，Claude 可以证明这些规范始终会通过——有时是在修补了它发现的剩余 bug 之后。因此，尝试证明这些规范的过程发现了数百个 bug。

在 Claude 尝试证明数百个入口点的过程中出现了大量 bug。为了确保 Claude 不必每次都停下来等待人类，我们让 Claude 修复它发现的 bug：它修补代码，从而用修补后的代码重新生成规范，然后 Claude 继续证明这个新规范。

我们发现的许多 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 通过直接将证明应用于机器代码，使形式化验证得到更广泛使用的一个实例。

我们还看到了以其他方式将 LLM 与形式化验证结合使用的成功案例。例如，我们让 Claude 编写 RFC 1950（定义 zlib 压缩文件格式的技术文档）的形式化规范。然后，我们让 Claude 证明 Linux 内核中的 zlib 实现正确实现了该规范。与上面的例子一样，Claude 在二进制级别证明了这一属性，只是 Claude 没有用 RISC-V，而是使用 Claude 生成（并经过大量测试）的 x86 ISA 形式化语义，直接证明了 x86 编译的二进制文件。然后我们在另外六个广泛使用的库上重复了这一过程。在此过程中，我们在一些极端情况下发现了一些轻微的（不可利用的）bug，目前正在向上游报告。我们从这一工作中得出两个结论：(1) 这些经过极其充分测试的代码库已经几乎完全正确；(2) 证明关于真实现有代码库的端到端正确性属性是可能的。

在另一项实验中，我们让 Claude 用 Rust 开发一个大型 Python 子集解释器，并（使用 Rust 验证工具 Verus）证明它遵循一篇学术论文中概述的 CPython 语义。然后我们实证测量了其对 CPython 行为的遵循程度，运行了超过 170 万个随机生成的 Python 程序，发现在 99.95% 的测试中与 CPython 行为完全一致，剩余的测试差异是意料之中的已知极端情况。

通过对简单安全属性进行形式化验证尝试，我们还在几个广泛使用且关键的应用程序中发现了问题。在其中之一，我们发现了一个此前未知的、潜伏了十多年的逻辑 bug。在验证一个广泛使用的 PDF 阅读器的过程中，我们在一周内发现的安全 bug 数量相当于通常一年的报告量。

这仅仅是个开始

LLM 辅助的形式化验证的一个关键限制是，生成证明可能需要数亿个令牌。如果我们的目标是让这些方法可用于整个软件生态系统，成本效率至关重要。幸运的是，我们有充分的理由预期效率会提高。

更新的模型需要更少的令牌

我们根据真实的 OSS-Fuzz 代码构建了 36 个小型验证任务。Opus 5.5 证明其中一半任务所用的令牌比 Opus 5 少约 40%。我们预计随着模型在长验证任务上接受训练，这一趋势将持续下去。

证明可以重用

当智能体分开工作时，它们往往最终会重复大量工作。证明和软件一样，是由更小的证明递归构建而成的——证明越小，往往越可重用。为了衡量这一点的影响，我们让智能体在证明各自目标时互相复制彼此的证明。在使用这个共享工作区时，智能体所需的令牌比单独工作时少了 17%，有些智能体甚至在之前单独尝试失败后取得了成功。

在我们的 OSS-Fuzz 证明工作中，我们观察到同样的现象在大规模上发生。证明的大部分内容涉及每个程序都包含的代码（特别是 C 运行时和 AddressSanitizer 的初始化），因此非常不同的程序最终可能会有显著重叠的证明。智能体团队利用了这一点，复制另一个团队完成的证明，然后针对自己的程序进行调整（图 6）。

证明的这种可重用性正是 Mathlib（Lean 中共享的形式化数学库）发展壮大到拥有由 700 多名贡献者提交的近 30 万个定理的原因：每一个新证明都建立在现有工作体系之上。在我们的 OSS-Fuzz 工作过程中，我们也积累了类似的证明体系，其中一些包含在本次发布中（我们不会发布可能暴露开源软件中未修补 bug 的证明）。

随着我们从这些初步实验中走出来，我们需要一种策略来验证庞大的现有软件体系，从最关键的依赖项开始。正如我们所展示的，这可以通过使用通用规范并在二进制级别工作来大规模实现，从而避免了用另一种语言重写整个代码库的需要。

这种方法还促进了包级别粒度上的证明重用，这意味着每个依赖项只需验证一次。依赖项遵循幂律：即使只证明一小部分共享库，也能使大量软件变得可证明。更多细节请参见 Theorem 验证整个 Nix 生态系统的路线图，其中包括 glibc、OpenSSL 和 cURL 等关键基础设施。

局限性

在实践中，形式化验证有时能证明的代码安全性比我们希望的要少。

“形式化验证过”并不意味着“没有 bug”。 Claude 可以编写一个证明，表明编译后程序的行为满足形式化规范的要求（该证明由外部证明检查器验证）。然而，证明检查器无法告诉你你的规范是否与现实相符。为了与现实相符，规范必须正确涵盖并建模被验证程序所运行的现实世界机器的一切，包括 CPU 和操作系统。当经过验证的代码中出现 bug 时，那是因为规范或假设的机器语义与现实不同。幸运的是，这也意味着我们知道去哪里寻找剩余的 bug，以及如何设计一个将这些仍可能存在 bug 的差距最小化的系统。以下是这一点在我们证明中的体现，以及未来缩小这些差距的工作思路。

真实机器做了模型没有描述的事情。 我们的证明针对的是链接到 musl libc 的单线程静态 RISC-V 二进制文件。然而，大多数人是在 x86 或 ARM 上运行这些库，并动态链接到 glibc。为了缩小这一差距，我们需要更接近已部署系统的系统模型。例如，朝这个方向迈出的一步是生成准确的 x86 语义。

该声明可能并未涵盖我们关心的所有内容。 我们证明了在 Google OSS-Fuzz 的许多模糊测试入口点上，对于任何小于 64 MB 的输入都不会触发崩溃（包括 ASan 崩溃）。然而，ASan 并不能检测所有内存安全 bug，而且我们并未验证每个库的所有入口点。即使我们验证了，验证所有入口点也不能覆盖整个库（尤其是如果存在死代码）。此外，真实程序可能会误用该库，导致调用者出现内存损坏。为了缩小这一差距，我们需要规定调用者对每个公共函数必须做什么，并且调用者必须严格遵守。

我们预计，随着我们更多地了解如何利用 LLM 进行形式化方法，以及随着模型持续改进，这些局限性将变得可以解决，我们将能够验证我们所依赖的代码中更大比例的部分。

结论

发展轨迹是清晰的：形式化验证历来只适用于最安全关键代码中定制的专家手工保证，但很快，它将对几乎所有生产软件变得像今天的模糊测试一样实用。就像静态类型、测试框架和其他正确性工具一样，验证将从“外挂”成熟为“内置”，这不仅由 LLM 推动，也由语言设计和开发工作流的创新推动。

在当今世界——LLM 会自动扫描并发现越来越多的代码漏洞——我们必须使用能够保证代码安全属性的流程。LLM 规模化的形式化验证是一种很有前途的方法，能以以前无法企及的范围和规模获得这些保证。我们鼓励其他人进行实验，以便我们共同构建一个健壮软件已广泛普及、而软件 bug 成为被充分理解且能快速解决的罕见现象的世界。

讨论整体偏审慎甚至怀疑，乐观声音主要来自少数已有落地经验的工程师。分歧主轴不是智能体能否写出通过检查的证明，而是这种证明到底算不算完整的形式化验证：一边强调规格、意图与现实之间的不可消除落差，以及大模型产出错配和复杂度墙；另一边则用 Lean、Rocq 等价性验证、发现真实缺陷并可安全合并优化代码的实例说明它确有工程价值。

认为形式化只能保证代码符合规格，无法保证规格符合现实与用户意图

• 形式验证要求先把代码正确建模成待证命题；但无法确保这个模型就是你要验证的程序本身，证明的可能只是被错误抽象的替身，而不是真实软件。（较多人）
• 所谓“100% 覆盖所有预期/非预期输入、所有利益相关者和用户行为”的形式规格，在当下大模型辅助的快节奏写码环境里并不存在；文章最后用传统模糊测试找崩溃、修完再证明崩溃已修复，被批评为近乎无意义。（较多人）
• 软件本质是人类期望的表示，而期望本身无法被形式化验证；证明检查器只检查代码与规格是否一致，不检查规格是否匹配人的目标。（较多人）
• 即使规格写对了，如何知道大模型证明的东西就是用户真正想要的，依然是开放问题；形式化验证只是把问题向上抬了一层。（较多人）
• 引用：> 证明检查器无法告诉你规格是否符合现实；想象一下，要给“现实”写一份形式化规格吧！（@adyavanapalli）

认为它不是完整/端到端的形式化验证，最多是高级确认或缺陷发现

• 这条流程只证明程序行为符合某个规格，考虑到软件供应链和真实攻击面，并未覆盖端到端语义；因此更接近确认，而不是验证。（少数人）
• 已有先例：大模型生成的 Lean 证明虽通过校验，配套论文却与证明内容不一致；Anthropic 把程序翻译成 Rocq 证明时也可能出现同类“看起来被证明”的错配，所以它能抓缺陷，却远非严格证明。（少数人）
• 引用：> 这当然能抓一些缺陷，但离真正的证明还差得远。（@j16sdiz）

认为冗长证明会撞复杂度墙，规模化必须依赖更好的抽象

• Anthropic 自己在附录承认：智能体采用的冗长证明风格可能在更复杂程序上撞墙，规模化需要围绕更好的模块化抽象与推理原则重构证明；有数学家因此推测大模型会在人类数学“凸包”之外遇到能力墙。（较多人）
• 形式验证涉及的系统通常不在预训练分布内，预训练大模型的广博领域知识优势被削弱，因此它比数学更能测试推理能力；这一观察反而增加了“凸包假说”的可信度。（较多人）
• 引用：> 当系统不在训练分布内时，预训练模型广博知识的优势买不到多少收益；形式验证正是检验推理的有趣试金石。（@jaykru）

已有工程实践显示可行，且能发现真实差异、支撑安全合并

• 有开发者把 Rust 与 C 翻译进 Lean，用大模型写等价性证明，已验证 Postgres 重写中约 12%、约 7 万行 C 代码的单线程行为一致，并发现跨平台浮点结果差异等细微问题。（少数人）
• 同一位开发者认为没有看到会阻止其进一步扩展的根本限制，直接反驳“复杂度墙”结论。（少数人）
• 工作中也出现这样的用法：智能体提交用 SIMD、CUDA 加速某函数的拉取请求，并附带 Rocq 行为等价证明，团队因此可以放心合并；这对优化与重构的安全落地很有价值。（少数人）
• 另有开发者用 Claude 从同一份规格分别实现 JavaCard VM 和证明生成器，要求两边出现完全相同的缺陷才能漏过；结果与字节码验证器一起用 ESBMC 静态验证并发现了一些缺陷，但后续让 Claude 写优化器字节码变换验证器时，它已在同一重构上卡了一周多。（少数人）
• 引用：> 我不认为存在会阻止它进一步扩展的根本限制。（@malisper）

认为真正的出路是转向确定性声明式语言，让验证默认发生

• 有人推测大模型不会去形式化验证大模型生成的命令式代码；开发会跳过函数式，直接进入类似 SQL 的确定性声明式语言，并配有效应系统与定理式语法，从而在编译或执行前默认完成验证，产物更短、幻觉更少、人也更易审阅。（少数人）
• 引用：> 到那时每个程序默认就是被形式验证过的；可以把它想成 AdaErlangSQL+++。（@yazaddaruvala）

怀疑这是市场宣传，或指出当前 Agent 并不主动验证

• 有人讽刺 Anthropic 的“市场宣传稿”队列很深，怀疑连篇内容更偏市场材料而非研究。（少数人）
• 更悲观地看，大模型进入软件开发至今多是抛弃最佳实践，因此不相信它会自然带来验证扩展；日常用 Claude 开发与处理工单时，它也不会主动做形式验证，往往直接假设系统状态，除非被要求才写校验脚本。（少数人）
• 引用：> 日常用 Claude 时，它不会主动做形式验证，往往直接假设系统状态，而不是快速写脚本去验证。（@lenerdenator）

有价值的补充

• 房屋类比：建房子分“愿景 / 蓝图 / 验收”三层。研究让验收近乎完美，但验收只查蓝图，不查愿景；若蓝图错了，房子仍能通过完美验收。要补的另一半，是确保蓝图符合并持续符合人的意图。（@Olscore）
• 延伸阅读：评论串里有人贴出此前两篇关于 TLA+ 的讨论，分别涉及“TLA+ 能检查什么、不能检查什么”和“互联网发现了 TLA+，然后呢？”。（@braiamp）
• 待观察问题：形式验证若被更多采用，是否会加速遗留 COBOL 系统向现代技术栈迁移？（@PandaRider）