What it is
Most software is checked by testing: running it on a sample of inputs and seeing whether it behaves as expected. Testing can never cover every possible input, so bugs can and do survive years of testing undetected. Formal verification takes a different approach. It translates a program, or a piece of hardware, into a precise mathematical model, states the property the system is supposed to have (for example, “this function never crashes on any input under 64 megabytes”), and then constructs a mathematical proof — checked step by step by a computer program called a proof assistant — that the model satisfies the property. If the proof succeeds, the guarantee holds for every possible input, not just the ones tested, within the assumptions baked into the model. If it fails, the tool can often produce a concrete counterexample showing where the property breaks.
The main techniques are model checking (exhaustively exploring a system’s possible states), theorem proving (constructing a logical proof interactively or automatically, typically in a proof assistant such as Coq — recently renamed Rocq by its maintaining consortium — or Isabelle/HOL), and abstract interpretation. A landmark example is seL4, an operating-system microkernel of roughly 8,700 lines of C that researchers at Australia’s NICTA (later CSIRO’s Data61) formally proved, using Isabelle/HOL, to match its specification with no implementation bugs — the first general-purpose OS kernel verified to that standard. That project took a specialist team years.
This is the labor-intensity that has historically confined formal verification to a narrow slice of software: safety-critical kernels, cryptographic protocols, aviation and rail control systems — code where the cost of writing proofs by hand is justified by the cost of failure.
Why it matters for AI governance and narratives
Formal verification has been a byword for “the thing AI might finally make affordable.” The bottleneck was never the mathematics; it was the person-hours required to write proofs for code that keeps changing. A credible claim that large language models can generate such proofs at scale — turning a decades-old capacity constraint into a solved problem — would be a genuine inflection point in software assurance, and it slots neatly into the builder and capital ecosystems’ preferred framing of AI as a force multiplier for rigor rather than a source of unverifiable output. It is also, pointedly, a counter-narrative to the dominant safety-ecosystem concern that AI-generated code is unauditable: here the claim is that AI-generated proof is more auditable than AI-generated code, because a proof checker either accepts it or doesn’t.
That is exactly why the self-reported, unreproduced nature of any such claim matters editorially. The entity asserting the capability (Anthropic) is also the entity that would benefit most from the claim being believed — not proof of error, but a standard conflict of interest that symmetric skepticism requires flagging regardless of source.
Key facts and dates
On October 22, 2026, Anthropic published a research account, in partnership with the startup Theorem, describing the use of Claude to generate roughly 180 million lines of proof in the Rocq proof assistant. The proofs establish that 239 entry points across 123 open-source libraries — drawn from Google’s OSS-Fuzz corpus of continuously fuzz-tested software — never crash on inputs under 64 megabytes, verified at the level of compiled RISC-V assembly instructions for single-threaded, static binaries linked against the musl C library. Theorem, a San Francisco startup founded in 2025 by Jason Gross and Rajashree Agrawal (Y Combinator, Summer 2025), supplied the formal models of RISC-V instructions and Linux process semantics that let the proofs reach down to the assembly level; it also runs a free verification service for qualifying open-source projects called OSS Verify. In the process, Claude surfaced previously undetected bugs, including a rediscovery of CVE-2026-56132 in libexpat, a parsing library fuzzed for years without the flaw turning up. Anthropic’s own account is explicit about the limits: “formally verified does not mean bug-free” — the proofs do not cover the x86 or ARM architectures most software actually runs on, multithreaded execution, or the glibc library most Linux distributions link against.
Where to learn more
- Anthropic: “LLMs are making formal software verification feasible at a much larger scale” — the primary source for the claim discussed above, including its stated caveats.
- seL4: Formal Verification of an OS Kernel (Communications of the ACM) — the pre-AI benchmark for what full formal verification has historically required.
- NIST SP 800-192, Verification and Test Methods for Access Control Policies/Models — a government reference point for formal verification’s role in software assurance standards.
- Quanta Magazine: “Hacker-Proof Code Confirmed” — accessible background on formal verification’s track record prior to AI involvement.