大语言模型助力形式化软件验证大规模应用成为现实

Claude大语言模型与Theorem合作展开的验证项目表明，LLM已能将形式化软件验证从传统的小规模、高成本工作扩展至产业级应用。1该项目首次在汇编代码层面对Google OSS-Fuzz计划下的123个开源库进行了大规模形式化验证，覆盖239个模糊测试入口点。1Claude为这些入口点生成了无崩溃保证的证明（假设输入不超过64 MB），生成的证明代码总计约1.8亿行Rocq代码，单个典型证明可达60万行，涵盖中位数为18,000条RISC-V指令的二进制文件。1

在验证过程中，Claude发现并识别出数百个漏洞，包括多项长期隐伏的缺陷。1这些发现包括由20 MB输入触发的计数器下溢导致的越界写入、需要64 MB输入和2GB内存才能触发的图像解码器越界读取，以及在PDF读取器中潜伏超过十年的逻辑缺陷。1相比先前的Claude Opus 5版本，新的Opus 5.5在处理简单验证任务时消耗的tokens减少了约40%。1此外，当多个代理共享证明工作区时，所需tokens进一步下降17%，部分代理即使在单独尝试失败的情况下，也能通过共享证明最终成功完成验证。1该项目基于单线程静态二进制文件、固定内存预算、RISC-V处理器和Linux操作系统等验证假设开展工作。1

Large language models are making formal software verification practical at unprecedented scale. Claude, in collaboration with Theorem, has successfully generated formal proofs for 239 entry points across 123 distinct libraries from Google's OSS-Fuzz program, marking the first time formal verification has been conducted at the assembly code level for over one hundred real-world open-source software repositories.1

The verification work produced approximately 180 million lines of Rocq code, with typical individual proofs containing around 600,000 lines and covering binary files with a median of 18,000 RISC-V instructions.1 Through this process, Claude identified and enabled fixes for hundreds of vulnerabilities, including several long-hidden defects such as a counter underflow triggered by 20 MB inputs causing out-of-bounds writes, an image decoder out-of-bounds read requiring 64 MB of input and 2 GB of memory, and a PDF reader logic flaw that had remained undetected for over a decade.1 The verification assumed programs running as single-threaded static binaries with fixed memory budgets on RISC-V CPUs under Linux.1

Efficiency improvements were also demonstrated in the approach. Claude Opus 5.5 reduced token usage by approximately 40 percent compared to Opus 5 on simpler verification tasks, and when agents shared proof workspaces, token requirements decreased by 17 percent, with some agents achieving successful proofs through shared work after failing independently.1 This advancement represents a significant shift for formal verification from a practice historically requiring years of expert investment to a feasible methodology now implementable at scale through language models.1