Anthropic: LLMs make formal verification of software feasible at larger scale

Anthropic collaborated with Theorem to use Claude to prove crash-free properties at the RISC-V assembly level for 239 fuzzing entry points across 123 OSS-Fuzz open-source libraries, and states this is the first large-scale work to use AI for formal verification of production software at the assembly code level. The proofs total approximately 180 million lines of Rocq, covering all inputs smaller than 64 MB, under the premise that the program is a single-threaded static binary on Linux. During the proof process, Claude discovered and fixed hundreds of long-undetected bugs, including an out-of-bounds write requiring an approximately 20 MB input with a specific layout and CVE-2026-56132 in libexpat; when verifying a widely used PDF reader, the security bugs found in one week were equivalent to the usual annual volume of reports. On efficiency, Opus 5.5 proved half of the tasks on 36 small verification tasks using approximately 40% fewer tokens than Opus 5.