Claude writes formal proofs for 123 open-source libraries

Anthropic and formal-verification company Theorem used Claude to write machine-checked proofs of security properties for 123 open-source libraries, working down to the compiled RISC-V assembly rather than stopping at the source. The libraries came from Google’s OSS-Fuzz corpus, and the pair proved properties across 239 entry points.

Claude generated roughly 180 million lines of proof code in the Rocq proof assistant, with a typical proof for a single binary running to about 600,000 lines. Writing those proofs turned up hundreds of bugs the project says were unlikely to surface through fuzzing alone, including a rediscovery of CVE-2026-56132 in libexpat. Anthropic has published a subset of the proofs, the RISC-V and Linux process semantics behind them, and a Claude skill that lets you point the same process at your own code, all on GitHub.

Why it matters: formal verification has stayed a specialist, slow exercise for most of its history, out of reach for all but the most critical code. If an LLM can turn an existing fuzz harness into a machine-checked proof at this scale, it starts to look like something a team could actually run on code they ship rather than a one-off academic demonstration, and the published skill is the part worth trying first.

The caveat: the scope was single-threaded static binaries with a 64 MB input limit, so this does not yet reach concurrency bugs or the hardest classes of real-world failure.