Anthropic demonstrates LLM-assisted formal verification at scale

Anthropic published research on 22 October on using Claude to apply formal verification to open-source software at greater scale. The company and partner Theorem worked on fuzz-test entry points in projects from Google’s OSS-Fuzz program. Fuzzing tries many sample inputs to find bugs, while formal verification attempts to prove that a specified property holds for all relevant inputs under stated assumptions. The research links the approaches by turning existing fuzz tests into properties to prove at the machine-code level.

Claude produced proofs for 239 entry points across 123 open-source libraries, using binaries compiled for the RISC-V processor architecture. The work does not provide a general guarantee that the full source code is bug-free. The property was narrower: that a single-threaded, statically linked program would not crash under specified fuzz-test behavior while running on RISC-V in a modeled Linux environment with a fixed memory budget. Inputs were limited to under 64 MB, and the tested crash conditions included memory errors caught by AddressSanitizer (ASan).

The method converted existing tests into a specification: a test entry point should not crash on any input smaller than 64 MB. Theorem’s formal semantics for RISC-V instructions and Linux processes, together with the binary, established the proof obligation. Claude wrote Rocq proofs, which the Rocq kernel checked mechanically. Anthropic says Claude found and patched bugs in some entry points before proving the patched binary. When a patch was applied, the specification was regenerated against the updated binary.

Anthropic reports that the proofs comprised about 180 million lines of Rocq code, with a typical proof about 600,000 lines and a median binary of 18,000 RISC-V instructions. It also says the process found hundreds of bugs, some requiring large inputs or unusual call sequences that fuzzing might rarely encounter. Examples in the post include an integer underflow and out-of-bounds write in compression code, out-of-bounds reads in image decoders, and a logic flaw in a file-restriction feature. These are findings reported by Anthropic from its experiments; the company does not say that every bug has been independently confirmed by third parties.

The proof-checking approach is a strength: even when the model writes a large amount of code, the Rocq kernel checks whether the theorem follows from the formal model. But a formal proof does not itself establish that the specification captures every behavior of a real deployed system. The work assumes single-threaded static RISC-V binaries and specified Linux semantics; Anthropic says it does not directly cover common x86 or ARM deployments and dynamic linking. ASan also does not detect every memory-safety flaw, and the work did not prove every entry point or all dead code in the libraries.

The result should therefore not be read as “123 libraries are bug-free.” The narrower finding is that selected fuzz entry points were proved against a crash property under a particular machine model and input bound, and that the proof effort also found bugs. Trust still depends on components such as the processor and operating-system models, theorem statements and Rocq checker. Anthropic says it is releasing some proofs and trusted components and inviting independent verification.

The company also reports a smaller experiment in which a shared proof workspace used 17% fewer tokens than agents working alone, and a separate 36-task evaluation where Opus 5.5 proved half the tasks with about 40% fewer tokens than Opus 5. These results are limited to the stated tasks and research setup; they are not general cost or speed guarantees. The broader contribution is a research path for proving tested properties at the binary level, not evidence that all defects in production software have been eliminated.