Formal verification leaves the expert's desk: Claude proves RISC-V assembly safe across 123 open-source libraries
Synopsis
Formal verification once took years of expert effort and was reserved for code such as avionics. In a collaboration with Theorem, Claude turned existing fuzz tests in open-source libraries into specifications and then produced proofs over compiled RISC-V assembly for 239 entry points across 123 OSS-Fuzz libraries, patching the bugs it found along the way. The proofs assume a single-threaded, statically linked RISC-V binary on Linux with a fixed memory budget and inputs up to 64 MB.
Interpretation
Formal security proofs can now be produced at scale by a large language model at the machine-code level of real open-source software, rather than written by hand by a few experts project by project. Formal verification previously required years of expert effort, for example two person-years to implement the seL4 kernel but 20 person-years to verify it, so it was practical only for mission-critical code such as Airbus avionics. In a collaboration with Theorem, Claude patched the bugs it found and then proved no crash on any input up to 64 MB for 239 entry points across 123 OSS-Fuzz libraries over a few weeks, totaling about 180 million lines of Rocq.
The approach treats a developer's existing fuzz test as the specification: the rule that the test never crashes is encoded as a statement about the compiled RISC-V instructions, and the model proves it. Fuzzing brute-forces semirandom inputs and never guarantees coverage of every code path, whereas a completed proof makes fuzzing that entry point superfluous. The proofs translate assembly into a mathematical model using Theorem's RISC-V instruction and Linux process semantics, with a typical proof about 600,000 lines for binaries whose median length is 18,000 RISC-V instructions.
The proof attempt itself surfaces bugs that fuzzing is unlikely to reach, and the model is allowed to patch them, regenerate the specification and continue proving. Fuzzers typically mutate small inputs capped at 1 MB and rely on code coverage, so they miss paths that need large inputs or particular call sequences. In one library's copy of a decompressor, Claude found a counter underflow leading to an out-of-bounds write only on inputs of around 20 MB with one rare layout; an image decoder out-of-bounds read needed a 64 MB input and over 2 GB of memory.
Perspective
The demonstrated setting is single-threaded, statically linked RISC-V binaries on Linux with a fixed memory budget and inputs up to 64 MB, covering the verified fuzz-test entry points rather than whole libraries.
A proof does not mean bug-free code: the proof checker cannot tell whether the specification matches the real machine, ASan does not detect all memory-safety bugs, and callers misusing a library can still cause memory corruption; a single proof can also take hundreds of millions of tokens, so cost remains a barrier to wider use.