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

Why it matters

Researchers, working with Theorem, used Claude to formally prove security properties of open-source software libraries at the assembly level, describing it as the first large-scale application of AI-driven formal verification to production code at that depth. Formal verification has traditionally demanded years of specialized expert effort, confining it to mission-critical projects such as aircraft avionics. The team argues that stronger guarantees are now necessary because language models are increasingly skilled at finding bugs and chaining them into exploits, a risk illustrated by the many vulnerabilities recently disclosed in the widely deployed Linux kernel. Claude proved that programs exit normally without memory-safety errors or failed assertions under stated assumptions, and uncovered bugs that had survived years of testing. The authors are publishing a subset of proofs for public verification and reuse, and Theorem is offering the same pipeline to other open-source projects while releasing a Claude skill to help developers verify their own code. They expect formal verification to become an essential part of secure software development.