LLMs are making formal software verification feasible at a much larger scale

Large language models are now being used to generate formal correctness proofs for real-world software at the assembly level, making formal verification far more scalable. By translating existing fuzz tests into formal specifications - principally a “no crash” property for all inputs under 64 MB - and modeling RISC-V and Linux process semantics, Claude produced machine-checkable Rocq proofs for 239 entry points across 123 OSS-Fuzz libraries. The effort produced about 180 million lines of Rocq proof code (typical proof ~600,000 lines) operating on compiled RISC-V binaries (median binary ~18,000 instructions). While proving specs, the model also found and patched hundreds of bugs that had eluded fuzzing. A subset of proofs and the formal semantics were published so others can independently check and reuse them; Theorem offers to run the pipeline for other projects and provides tooling to help developers adopt the workflow.

This approach reduces the expert labor historically required for formal verification and creates a concrete trust model: the guarantees hold conditional on the correctness of the RISC-V and Linux formal semantics, the stated theorem goals, and the Rocq proof checker. Limitations include the current scope assumptions (single-threaded static binaries with fixed memory on RISC-V/Linux) and that proofs only rule out bugs within those assumptions and reachable from the verified entry points. Expanding architectures, OS models, and standardized specs will amortize costs and broaden applicability, moving formal verification toward routine integration into secure software development.