LLMs Make Formal Software Verification Practical

Formal verification—mathematically proving that code meets security specifications—can eliminate entire classes of bugs. But the approach has been impractical for production software because generating proofs demands extensive specialist effort and significant time investment. A single operating system kernel required 20 person-years to verify. AI models are now changing this equation by handling the proof generation work at scale.

Anthropicand Theorem demonstrated this shift by using Claude to generate formal proofs for 123 open-source libraries, working at the assembly-code level. They converted existing test suites into mathematical specifications, then had Claude produce proofs showing the code couldn’t crash on valid inputs. In the process, Claude discovered bugs that had evaded detection for years despite running trillions of traditional fuzz test iterations. This marks the first large-scale application of AI-assisted formal verification to production-grade software at the assembly level.

The researchers published the proofs for reuse and released tools to help developers verify their own code. As models continue improving, formal verification could transition from a luxury for mission-critical systems like avionics into a standard practice across software development, fundamentally changing how organizations approach security guarantees.