跳转至

大语言模型助力形式化软件验证实现规模化突破

LLMs Are Making Formal Software Verification Feasible at a Much Larger Scale

作者： 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

Authors: 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 轻易挖掘和利用的漏洞，而通过严密数学推导证明代码绝对没有缺陷的“形式化软件验证”，过去往往需要顶级专家耗时数年，因而仅能局限于航空航天等极少数容错率为零的关键系统。Anthropic 与 Theorem 开展前沿合作，首次证实以 Claude 为代表的大语言模型 (Large Language Model, LLM) 能够在大规模真实生产环境中自主构建严密的形式化数学证明。研究团队在 RISC-V 汇编代码级别，针对超过 100 个现实开源软件库成功完成了无崩溃安全证明，并顺带挖掘出经历过数万亿次模糊测试仍未暴露的深层长周期漏洞。这项突破标志着形式化软件验证正在走出象牙塔，未来将成为构建本质安全软件基石的核心支柱。

摘要

Summary

大部分现代软件都潜藏着安全缺陷，而现今的 AI 工具能轻而易举地找出并利用这些漏洞，使传统的网络安全防御手段逐渐捉襟见肘。虽然“形式化软件验证” (formal software verification) —— 即用严密的数学推导来证明代码绝对不存在任何漏洞 —— 是最理想的防御方案，但在过去，这项工作往往需要顶级专家耗费数年心血逐行推导，导致它只能被应用在航空航天飞控等极少数容错率为零的关键系统中。

Most software contains bugs that modern AI can easily find and exploit, rendering traditional cyber defenses insufficient. While formal software verification—mathematically proving code is bug-free—is the ideal defense, it has historically demanded years of expert human effort, restricting its use to ultra-high-stakes systems like aerospace avionics.

在与 Theorem 的合作研究中，团队证实了以 Claude 为代表的大语言模型 (LLM) 能够以史无前例的规模自主生成形式化证明。借助 Claude 的推理能力，团队成功在汇编代码层级 (RISC-V) 证明了超过 100 个真实开源软件库的安全属性 (这也是业界首次在汇编级别将 AI 驱动的形式化验证大规模应用于生产级软件)。在这个过程中，Claude 还顺藤摸瓜揪出了多个顽固的历史遗留漏洞，而这些漏洞此前即使经历过数万亿次自动化模糊测试 (fuzz-test) 也从未被察觉。随着模型的持续进化，形式化验证有望真正成为构建可信安全软件的基石。

In a collaboration with Theorem, researchers demonstrated that Large Language Models (LLMs) like Claude can autonomously produce formal proofs at an unprecedented scale. By leveraging Claude, the team proved security properties at the assembly-code level (RISC-V) across over 100 real-world open-source software libraries (marking the first large-scale application of AI-driven formal verification to production software at the assembly level). Along the way, Claude uncovered long-standing bugs that had eluded trillions of automated fuzz-test runs. As models advance, formal verification is poised to become an essential pillar of secure software development.

引言

Introduction

现代软件的脆弱性早已人尽皆知；即便是像 Linux 内核这样经过无数严苛测试的核心系统，近期公开披露的安全漏洞也超过了 1,000 个。随着前沿 AI 模型越来越擅长将看似无关紧要的小瑕疵串联成破坏力惊人的漏洞利用链，开发者比以往任何时候都更需要一种前置防御手段 —— 从根本上直接验证软件绝对不存在缺陷。

Modern software is notoriously fragile; even heavily tested systems like the Linux kernel recently had over 1,000 vulnerabilities disclosed. Because frontier AI models are increasingly adept at chaining seemingly benign bugs into catastrophic exploits, developers need proactive techniques that verify the absence of bugs altogether.

什么是形式化验证？

What is Formal Verification?

形式化验证将计算机代码转化为严格的数学模型，以此来推导证明该代码完全遵循预先定义好的安全规则。在推导过程中，一旦证明步骤受阻走不通，就意味着发现了一个潜在的代码缺陷。通过不断排查修复并重复这一过程，最终就能在数学层面上得到无可争议的安全保障，确保代码中不存在任何违背既定规则的漏洞。

Formal verification translates code into a mathematical model to prove it strictly adheres to a defined set of security rules. If a proof fails, the failure reveals a potential bug. Iterating on this process eventually yields a mathematical guarantee that the code is free of rule-violating bugs.

然而，撰写数学证明是一项门槛极高的小众技能，证明代码本身的体量往往是原始源代码的数倍之多 (例如著名的 seL4 微内核操作系统，编写内核源码只用了 2 人年，但对其进行完整的形式化验证却耗费了足足 20 人年)。

However, writing proofs requires a niche skill set and is often many times larger than the source code itself (e.g., the seL4 operating system kernel took 2 person-years to write, but 20 person-years to formally verify).

借助大语言模型实现规模化

Scaling with LLMs

如今，前沿大语言模型已经能够为现实生活中的软件自主编写正确性证明。研究人员让 Claude 为 123 个开源软件库推导证明其安全属性 —— 特别是要确立其可执行二进制程序在特定约束条件下永远不会发生崩溃 (例如：输入数据在 64 MB 以内、作为单线程静态二进制文件运行在配备 Linux 操作系统的 RISC-V CPU 上)。

Frontier LLMs can now autonomously generate correctness proofs for real-world software. Researchers asked Claude to prove security properties across 123 open-source libraries—specifically establishing that their executable artifacts will never crash under certain constraints (e.g., inputs under 64 MB, running as single-threaded static binaries on a RISC-V CPU with a Linux OS).

研究团队目前正在公开部分证明代码，以及配套的 RISC-V 架构与操作系统语义模型；同时 Theorem 也提供了相应的工作流管线与 Claude 技能 (skills)，帮助开发者验证各自的代码库。

The researchers are publishing a subset of these proofs, along with RISC-V and OS semantics, while Theorem offers pipelines and Claude skills to help developers verify their own codebases.

将测试套件转化为数学证明

Turning Tests into Proofs

要用数学方法证明一段软件是完全正确的，前提是必须先用一份“规范” (specification, 简称 spec) 明确定义出究竟什么是“正确”。然而对于大多数复杂的通用软件 (例如文本编辑器) 而言，编写一份详尽完备的形式化规范本身就难如登天。为了跨越这道阻碍，研究人员巧妙地将现有的测试套件自动转化为形式化规范，所立下的证明规则极其朴素直接：要求“该测试套件必须在所有可能的 RISC-V 二进制执行路径中永远顺利通过”。

To prove software is correct, one must define "correctness" via a specification (spec). For most arbitrary software (like text editors), a comprehensive spec is difficult to write. To bypass this, the researchers automatically converted preexisting test suites into specs by asserting the rule: "this test suite always passes" across all possible RISC-V binary executions.

巧妙利用模糊测试

Leveraging Fuzz Tests

该项目充分利用了来自 Google OSS-Fuzz 项目的模糊测试 (fuzz tests)。在这些测试中，自动化测试引擎会用海量随机变异的输入狂轰滥炸程序入口，试图触发程序崩溃 (例如配合能够揪出内存安全错误的 AddressSanitizer (ASan) 来监测异常)。

The project utilized fuzz tests from Google's OSS-Fuzz initiative, where automated testing engines bombard entry points with mutated inputs to force crashes (e.g., via AddressSanitizer, which catches memory safety errors).

[ Fuzz Test / Entry Point ] + [ RISC-V & OS Semantics ] 
       ↓
[ Generated Spec (No crashes for inputs < 64 MB) ]
       ↓
[ Claude writes Proof ] → [ Rocq Proof Checker validates ]

验证成果

Results

Claude 成功对代码漏洞进行了修复补全，并为 123 个 OSS-Fuzz 软件库中的 239 个程序入口完整证明了“永不崩溃”属性。

Claude successfully patched bugs and proved the "no-crash" property for 239 entry points across 123 OSS-Fuzz libraries.

  • 庞大规模：整个项目累计包含约 1.8 亿行 Rocq 证明代码；对于平均包含 18,000 条 RISC-V 指令的二进制程序，一份典型的数学证明代码量高达约 60 万行。
  • 极小可信计算基：由于所有的数学逻辑都经过 Rocq 证明检查器进行机械化的自动化判定，开发者只需要信任极小的一部分“可信计算基” (Trusted Computing Base, TCB)：形式化语义模型 (RISC-V 架构与 Linux 系统行为)、定理陈述本身，以及 Rocq 检查器工具本体即可。
  • Scale: Comprises ~180 million lines of Rocq proof code, with typical proofs hitting ~600,000 lines for binaries averaging 18,000 RISC-V instructions.
  • Trust Base: Because the Rocq proof checker mechanically validates the logic, developers only need to trust a minimal trusted computing base: the formal models (RISC-V and Linux), the theorem statements, and the Rocq checker itself.

揪出并修复隐藏缺陷

Finding and Fixing Bugs

尝试在数学上证明代码正确的过程，本身就是一面照出深层隐藏 Bug 的“照妖镜”。在此次研究中，Claude 被赋予了完全自主的权力：它可以自己修改修复 Bug、重新生成规范并继续推导后续证明。

The process of attempting to prove code correct naturally surfaces hidden bugs. Claude was given the autonomy to patch bugs, regenerate specs, and resume proof generation.

  • 捕获极难复现的隐蔽缺陷：常规模糊测试器通常只能对微小的输入变异 (通常小于 1 MB) 进行试探，严重依赖代码覆盖率。而 Claude 的形式化验证直接揪出了多处深层漏洞 —— 例如某解压工具中的一处越界写 (out-of-bounds write) 缺陷，该漏洞需要构造极为罕见的特定内存布局并在输入接近 20 MB 时才会触发；此外还自主重新发现了 libexpat 库中的已知高危漏洞 CVE-2026-56132。
  • 突破内存安全的边界：证明测试套件全部通过不仅能保障内存安全，还能形式化验证更高维度的系统不变量 (invariants)，比如往返一致性 (roundtripping)、幂等性 (idempotence) 以及代数恒等律 (例如证明 LZO 算法压缩后再解压能够百分之百无损复原)。
  • Hard-to-find Bugs: Fuzzers typically mutate small inputs (<1 MB) and rely on code coverage. Claude's formal verification uncovered deep vulnerabilities, such as an out-of-bounds write in a decompressor requiring a rare layout with a ~20 MB input, and rediscovery of vulnerabilities like CVE-2026-56132 in libexpat.
  • Beyond Memory Safety: Proving test suites pass also verifies high-level invariants like roundtripping, idempotence, and algebraic laws (e.g., LZO compression/decompression equivalence).

更多形式化验证实战案例

Other Formal Verification Case Studies

  • zlib 与 x86 二进制：Claude 为经典压缩库 zlib (RFC 1950) 撰写了完整的形式化规范，并在其自身生成的 x86 指令集架构 (ISA) 语义基础上，直接在 x86 二进制层面证明了 Linux 内核内置 zlib 实现的正确性。
  • Rust 编写的 Python 解释器：Claude 采用 Rust 语言构建了一个 Python 子集解释器，并利用形式化验证工具 Verus 证明其严格契合 CPython 语义规范；该成果通过了多达 170 万个测试程序的检验 (运行行为契合度高达 99.95%)。
  • 关键高危应用实战：当将形式化验证应用到一款被广泛使用的 PDF 阅读器上时，仅仅在一周之内挖掘出的安全漏洞数量，就相当于该软件以往整整一年内被报告的漏洞总和。
  • zlib & x86: Claude wrote a formal spec for zlib (RFC 1950) and proved the Linux kernel's zlib implementation correct at the x86 binary level using self-generated x86 ISA semantics.
  • Python Interpreter in Rust: Claude built a subset Python interpreter in Rust and used Verus to prove adherence to CPython semantics, confirmed via 1.7 million test programs (99.95% behavioral match).
  • Critical Applications: Applying formal verification to a widely used PDF reader surfaced as many security bugs in one week as are typically reported in an entire year.

模型在各类验证任务中的效率数据可视化图表：

Data visualization for model efficiency across verification tasks:

Opus 5.5、Fable 5.1 与 Opus 5 在 36 项验证任务中随智能体 Token 预算变化的完成率折线图。Opus 5.5 消耗最少的 Token 即可完成证明。 / Line chart of the share of 36 verification tasks completed by token budget per agent for Opus 5.5, Fable 5.1, and Opus 5. Opus 5.5 finishes proofs with the fewest tokens.

这才刚刚拉开序幕

This Is Just the Beginning

尽管借助大语言模型进行形式化验证目前依然需要消耗庞大的 Token 预算，但整个流程的运行效率正在以惊人的速度提升：

While LLM-assisted verification requires significant token budgets, efficiency is rapidly improving:

  1. 新一代模型消耗的 Token 大幅减少：更先进的模型版本 (如 Opus 5.5) 在解决同等复杂度的验证任务时，所需的 Token 数量相较于上一代有了显著下降。
  2. 数学证明可高效复用：形式化证明具备高度的模块化特征，能够像搭积木一样递归构建。当多个 AI 智能体 (AI Agent) 共享同一个工作空间、互相借鉴并改造已有的证明片段时，整体 Token 消耗量骤降了 17%，许多原本失败的验证任务也因此迎刃而解。
  1. Newer Models Need Fewer Tokens: Newer iterations (like Opus 5.5) solve complex verification tasks using significantly fewer tokens than predecessors.
  2. Proofs Can Be Reused: Proofs are modular and build recursively. When AI agents shared a common workspace to copy and adapt existing proofs, token usage dropped by 17%, and failed tasks frequently succeeded.

由于各类程序普遍共享着大量底层标准函数库 (比如 C 语言的运行时初始化流程)，因此跨软件库复用证明代码具备极佳的可扩展性。这一特性为将来验证整个开源生态 (包括 Nix、glibc、OpenSSL 以及 cURL 等核心基础软件) 铺平了康庄大道。

Because standard routines (like C runtime initialization) are shared across programs, proofs scale efficiently across packages, paving the way toward verifying entire ecosystems like Nix, glibc, OpenSSL, and cURL.

跨程序证明代码复用与迁移适应的可视化展示：

Visualization of proof reusability and adaptation across programs:

libcups、freerdp 和 libzmq 证明代码的模块化图表，展示了各组成部分中完全相同、略微调整、较多修改以及全新编写的比例分布。 / Block chart of the proofs for libcups, freerdp, and libzmq, showing how much of each part was identical, lightly edited, edited more or new.

局限性与挑战

Limitations

  • “形式化验证”并不等同于“绝对无 Bug”：证明只能保证代码完全符合给定的规范；如果编写的形式化规范本身出现疏漏，或者底层的机器模型 (CPU 架构或操作系统行为) 脱离了真实的物理运行环境，程序依然可能残留严重缺陷。
  • 当前系统模型的局限：目前的证明体系建立在单线程、与 musl libc 静态链接的 RISC-V 二进制假设之上；而在真实的工业生产环境中，绝大多数系统运行的是高度复杂的动态链接 x86 或 ARM 架构环境。
  • 验证范围的边界：针对单个函数入口点或仅依赖 AddressSanitizer (ASan) 证明内存安全性，并不能等同于证明了整个软件库在所有业务逻辑上的绝对正确，也无法防范上层调用者由于使用不当而引入的安全隐患。
  • "Formally verified" ≠ "Bug-free": A proof guarantees that code matches a specification, but if the specification or underlying machine model (CPU/OS) diverges from physical reality, bugs can persist.
  • Model Gaps: Current proofs assume single-threaded, static RISC-V binaries linked with musl libc, whereas production systems typically run dynamically linked x86/ARM environments.
  • Scope Limits: Proving individual entry points or memory safety (via ASan) does not guarantee total library correctness or guard against misuse by calling applications.

结语

Conclusion

形式化验证正在迎来历史性拐点 —— 它不再是仅属于航空航天等极端昂贵、严苛场景的高冷特权，而是正逐步蜕变为主流生产级软件触手可及的高效实用工具。随着大语言模型智力水平的飞跃，以及底层基础证明库的日益丰富，形式化软件安全验证终将从以往“亡羊补牢”式的后置补丁，演进为现代软件工程中不可或缺的“出厂即自带”标配规范。

Formal verification is transitioning from an elite, ultra-expensive practice reserved for mission-critical aerospace code into a scalable, practical tool for mainstream production software. As LLMs become more intelligent and foundational proof libraries expand, verifying software security will evolve from a bolt-on afterthought to a built-in standard.