Most software is riddled with bugs, which AI can now easily find and exploit. The standard defenses against cyberattacks are no longer sufficient: we need ways to prove that code is free of bugs. Formal software verification could provide this guarantee, but it has historically required years of expert effort, making it impractical for most real-world projects. In a collaboration with Theorem, however, we show this is no longer the case: LLMs can now produce formal proofs at large scale, enabling new software development workflows that include proven security guarantees. Using Claude, we proved security properties at the assembly code level (RISC-V) in over 100 real-world open-source software libraries. To our knowledge, this represents the first large-scale effort to use AI to apply formal verification to production software at the assembly code level. While writing the proofs, Claude also discovered bugs that had eluded detection for years, despite trillions of test runs.
Key results
Over a few weeks, Claude patched bugs and proved no-crash properties for 239 entry points across 123 OSS-Fuzz libraries. Proofs operate on compiled RISC-V instructions and comprise about 180 million lines of Rocq, with a typical proof around 600,000 lines for binaries with a median length of 18,000 RISC-V instructions. Proofs assume single-threaded static binaries with a fixed memory budget on RISC-V using Linux, for inputs under 64 MB.
Claude found bugs fuzzers were unlikely to trigger: counter underflows on ~20 MB inputs, out-of-bounds reads needing 64 MB inputs and multi-GB memory, multi-handle call sequences, and rediscovery of CVE-2026-56132 in libexpat. The team also proved zlib RFC compliance at the x86 binary level, built a Verus-verified Python subset interpreter in Rust (99.95% CPython behavioral match on 1.7M random programs), and found latent logic bugs in a widely used PDF reader.
Theorem is offering to run the same pipeline for other open-source projects and publishing a Claude skill for developers. Anthropic is releasing trusted components, complete Rocq proofs where no unpatched bugs would be revealed, and specifications for unproven fuzz tests.
Newer Opus models used ~40% fewer tokens on benchmark verification tasks; shared proof workspaces cut token use 17% versus solo agents. Limitations: specs may not match deployed x86/ARM/glibc systems; ASan does not catch all memory bugs; not all library entry points were verified.