Claude Generates Formal Proofs for 123 RISC-V Libraries

Anthropic and Theorem applied Claude to generate Isabelle/HOL proofs over RISC-V semantics for 123 libraries. The proofs establish that each binary exits without memory violations or assertion failures for all inputs below 64 MB and all modeled Linux responses. The pipeline also surfaced latent bugs that had survived trillions of prior test executions.

Prior formal efforts required 20 person-years for the seL4 microkernel on 8 700 lines. The current work scales verification across production codebases without equivalent expert labor. It remains bounded to fixed memory layouts and single-threaded execution, yet covers far more lines than previous automated attempts documented in the seL4 and CertiKOS lineages.

Linux kernel vulnerability disclosures exceeded 1 000 in recent years. Assembly-level proofs close entire classes of memory-safety exploits that fuzzing and static analysis miss. Operational integration requires embedding the proof step inside continuous integration so that each commit either extends an existing proof or fails the build.

Next steps include lifting the single-thread and memory-budget restrictions and publishing the full proof corpus for independent re-verification. Model iteration is expected to reduce proof generation time further.