Anthropic and Theorem prove security properties for 123 open-source libraries using LLM-driven formal verification

• Anthropic and Theorem demonstrated that LLMs (Claude) can perform large-scale formal verification, proving security properties for 123 open-source libraries (239 entry points) at the RISC-V assembly level.
• The verification covered all inputs under 64MB, proving that programs terminate normally without memory safety errors or assertion failures under modeled Linux OS responses.
• The process generated approximately 180 million lines of Rocq proof code, with an average of 600,000 lines per proof and a median of 18,000 RISC-V instructions per binary.
• Claude identified and patched bugs that fuzzers missed, including a compressor counter underflow, an out-of-bounds read in an image decoder, and a logic bug in file loading limits.

Methodology and Efficiency

• Existing fuzz tests were converted into rules stating that the test suite always passes, serving as specifications for RISC-V compiled binaries.
• Opus 5.5 completed half of 36 verification tasks using approximately 40% fewer tokens than Opus 5.
• Allowing agents to share a workspace and copy proofs reduced token usage by 17% compared to independent work, with 30 of 34 completed proofs using fewer tokens than the average standalone cost.

Case Studies and Results

• A Rust-based Python interpreter was proven to follow CPython semantics using Verus, matching CPython behavior in 99.95% of 1.7 million random test programs.
• Verification of a widely used PDF reader found security bugs equivalent to a year's worth of reports in just one week, including a logic bug latent for over 10 years.
• The Linux kernel's zlib implementation was proven accurate against RFC 1950 using x86 ISA formal semantics, revealing minor bugs.

Limitations and Scope

• Current proofs are limited to single-threaded, static RISC-V binaries linked with musl libc, whereas production environments often use x86/ARM with dynamic glibc linking.
• "Formally verified" does not guarantee bug-free software, as the proof checker cannot verify if the specification matches real-world hardware or OS behavior.
• The approach does not cover all entry points or dead code, and memory corruption from incorrect caller usage remains a potential risk.