LLMs make formal software verification feasible
Archived — this story has rotated out of today’s deck. It is kept here in full.
The gist
Anthropic and Theorem used Claude to formally prove security properties in 123 open-source libraries.
The work suggests formal verification could become routine for production software.
Background
Anthropic is the AI company behind the Claude model, and Theorem is a research organization that offers a formal verification method using LLMs free of charge to open-source projects. Formal verification — mathematically proving software behaves as specified — has historically required years of expert effort: verifying the seL4 operating system kernel took 20 person-years, so it was practical only in mission-critical code such as Airbus's avionics. The research arrives as LLMs grow more adept at finding and exploiting bugs, with the Linux kernel recently seeing over 1,000 vulnerabilities disclosed.
How it unfolded
- Oct 22, 2026Anthropic publishes research with Theorem showing LLMs can produce formal proofs at large scale, proving security properties at the RISC-V assembly level in over 100 real-world open-source libraries.
- Oct 23, 2026GIGAZINE reports the work covered 123 open-source libraries, proving no bug-induced crashes for single-threaded static binaries with fixed memory on a RISC-V CPU running Linux.
- Oct 23, 2026LavX News reports 239 entry points proven across 123 libraries, with roughly 180 million lines of proof code written in the Rocq proof assistant.
- Oct 23, 2026Claude is reported to have found hundreds of bugs that evaded trillions of fuzzing runs, including a counter underflow in a decompressor and an out-of-bounds read in an image decoder, and to have rediscovered CVE-2026-56132 in libexpat.
- Oct 23, 2026Claude writes a formal specification of RFC 1950 (the zlib format) and proves the Linux kernel's zlib implementation matches it at the x86 binary level; in another experiment it proves a Rust-built Python interpreter adheres to CPython semantics with a 99.95 percent behavioral match across 1.7 million random programs.
Who’s saying what
- Anthropic
- The research team says this is, to its knowledge, the first large-scale effort to apply AI to formal verification of production software at the assembly level, and that formal verification will soon be as practical as fuzzing for almost all production software.
- Caution
- Anthropic notes the proofs do not mean the libraries contain no bugs — remaining bugs lie within the listed artifacts or outside the proof's scope — and that proving no bugs on RISC-V does not rule out bugs on Arm or x86.
- Expert
- Runtime Verification CEO Everett Hildenbrandt says the edge in his team's kernel experiment came from a hypothesis about where to look — drivers handling untrusted input with less scrutiny — not from simply asking an LLM for bugs.
Still unverified
Anthropic's claim that this is the first large-scale effort to use AI to apply formal verification to production software at the assembly code level is stated as "to our knowledge."