Overview
- Researchers used Claude to convert existing fuzz tests into formal specifications and then generate proofs that 239 program entry points across 123 libraries would not crash under the stated conditions.
- The team worked at the RISC-V assembly level, produced about 180 million lines of proof code with typical proofs around 600,000 lines, and used the Rocq tool to independently check the generated proofs.
- The verification uncovered hundreds of defects that previous testing missed, including counter underflows and out-of-bounds reads that required rare, large inputs or specific operation sequences to trigger.
- Anthropic allowed Claude to patch some of the found bugs and re-run proofs, but the guarantees apply only to the properties, inputs, and a single-threaded, statically linked RISC-V model of Linux used in the work.
- If reproducible and integrated into development pipelines, this AI-driven workflow could make formal verification cheaper and more common, though independent checks, broader models, and real-world testing will determine how widely it helps developers and users.