Anthropic research shows how LLMs can scale software formal verification

LLMs are making formal software verification feasible at a much larger scale

Anthropic and Theorem used Claude to verify security properties at the RISC-V binary level for 239 test entry points across 123 open-source libraries. The work turned existing fuzzing into formal specs, had Claude fix the bugs it found, and generated about 180 million lines of Rocq checked by the Rocq checker.

Why it matters: Anthropic and Theorem convert existing fuzzing into formal specs, then let Claude produce machine-code-level proofs, so verification does not require rewriting the whole codebase.