Imagine you're a building inspector who checks houses by throwing rocks at the walls. Throw enough rocks, and you'll find the weak spots — but you can never throw every possible rock. That's fuzzing: brute-force testing that finds bugs but can never prove their absence. What this project does is replace the rock-throwing with a mathematical proof that no rock, of any shape, thrown at any angle, could ever break the wall. The inspector becomes a geometer. The committed claim: Claude autonomously wrote formal correctness proofs for 239 fuzz-test entry points across 123 real-world open-source C/C++ libraries, operating at the RISC-V assembly level, producing approximately 180 million lines of Rocq proof code. This is the first large-scale demonstration of AI-driven formal verification applied to production software at the binary level. Each proof guarantees no crash on any input up to 64 MB, for every modeled Linux OS response and memory layout, under stated assumptions (single-threaded, static binary, fixed memory budget, RISC-V on Linux). The architecture is straightforward but the execution is not. Existing fuzz tests from Google's OSS-Fuzz are compiled to RISC-V binaries. Theorem's formal semantics for RISC-V instructions and Linux process behavior mechanically translate these binaries into mathematical models in the Rocq proof assistant (formerly Coq). Claude then writes the proof that the program never crashes — a typical proof runs to ~600,000 lines covering a median binary of ~18,000 RISC-V instructions. The Rocq kernel machine-checks every proof, so the LLM's output is verified by an independent formal system. This is a critical architectural property: the LLM is the proof writer, not the proof checker. The ladder question is harder to answer than it looks. There is no real prior-art baseline for AI-driven formal verification at this scale. The closest reference point is seL4, the formally verified microkernel that took 20 person-years of expert effort to verify 10,000 lines of C. Here, Claude covered 123 libraries in weeks. But the comparison is imperfect — seL4's verification covered full functional correctness of an operating system kernel, while this project proves a narrower property (no crash on any input) for fuzz-test entry points. The scope assumptions are significant: single-threaded, static binaries, RISC-V only, fixed memory budget. Still, the sheer volume — 180 million lines of proof — represents an orders-of-magnitude jump in formal verification throughput. Integrity is genuinely strong on one axis and has real gaps on another. The proofs are machine-checked by Rocq, which is about as strong as validation gets in formal methods — the proof checker is the gold standard, not the authors' judgment. A subset of proofs and the RISC-V/OS semantics are published for independent review. However, the trusted computing base includes Theorem's RISC-V semantics and OS model, which are not independently verified community standards. If those semantics have bugs, the proofs prove the wrong thing. The project also doesn't compare against alternative approaches (e.g., bounded model checking, symbolic execution, or other LLM-assisted verification methods), so we can't assess relative efficiency. The milestone trajectory is clear: today's proofs cover single-threaded static RISC-V binaries with narrow crash-freedom properties. The next concrete targets are multi-threaded programs, x86/ARM architectures, and richer properties beyond crash-freedom (functional correctness, information-flow security). The paper also mentions initial explorations in proving behavioral equivalence of a Python interpreter written in Rust and assessing zlib's security — these hint at the broader ambition. The real unlock is when formal verification becomes a default CI/CD step rather than a research project, which requires both expanding the scope of provable properties and reducing the cost per proof. The obvious experiment not run: applying this pipeline to x86 or ARM binaries, which represent the vast majority of deployed software. The honest read is (a) and (c) combined — Theorem's formal semantics currently cover RISC-V, and building equivalent semantics for x86's notoriously complex instruction set is a major engineering effort they're likely working on for the next paper. The other missing experiment is adversarial evaluation: can the pipeline handle intentionally obfuscated code, or code with subtle concurrency bugs that the single-threaded assumption conveniently excludes?
