Formal verification is the practice of proving, with mathematical rigor and usually with a machine-checked proof, that a system satisfies a formal specification of its intended behavior. In software, developers translate code into a mathematical model and attempt to prove that it always obeys a defined set of rules; a failed proof indicates a possible violation and suggests where it lies (Source: anthropic.com). The guarantee is relative to the specification, the modeled environment and the trusted checking tools, and does not establish that the specification itself captures what users intended (Formalizing Fermat's Last Theorem (Anthropic, September 2026)). In AI policy and safety debates the technique appears in three roles: as a defense for software that AI systems can increasingly attack, as a proposed source of evidence that an AI system is safe, and as a check on machine-generated mathematics.
Background
Formal, machine-checked verification has historically been applied to small, high-assurance components because of its cost. The seL4 microkernel, described by its developers in 2009 as the first formal proof of functional correctness of a complete, general-purpose operating-system kernel, comprised about 8,700 lines of C and 600 lines of assembly; the proof was carried out in the Isabelle/HOL theorem prover and assumed the correctness of the compiler, assembly code and hardware (Source: sigops.org). Its developers later reported that the kernel's design, documentation, coding and testing took 2.2 person-years while the correctness proof took about 20 person-years, and extended the result to a proof that the binary implements the C semantics, removing the compiler from the trusted base (Source: sel4.systems). The seL4 authors acknowledged the standard limitation of the method: a proof "only shows that the implementation has precisely the same bugs that the specification contains" (Source: sigops.org).
Key elements
- Specification. A formal statement of what "correct" means. Some programs have a natural specification (a PNG decoder following RFC 2083); for most, such as a text editor or browser, an unambiguous specification is difficult to write, which Anthropic describes as a significant obstacle to verification at scale (Source: anthropic.com).
- Model of the environment. The semantics of the machine, operating system or world against which the property is proved. Bugs found in verified code arise where this model differs from reality (Source: anthropic.com).
- Proof and checker. The proof is checked by a small trusted program (for example the Rocq or Lean kernel, or Isabelle/HOL), so that a proof of any length need not be read by a person; what remains to be trusted is the specification, the environment model and the checker (Source: anthropic.com).
Use of language models to produce proofs
In October 2026 Anthropic, working with the company Theorem, reported that Claude proved that 239 fuzzing entry points across 123 libraries in Google's OSS-Fuzz project cannot crash on any input up to 64 MB, after patching the bugs it found during the work. The proofs operate on compiled RISC-V binaries and total about 180 million lines of Rocq; a typical proof is about 600,000 lines for a binary with a median length of 18,000 RISC-V instructions. They assume a single-threaded static binary with a fixed memory budget running on Linux, and Anthropic states that "formally verified" does not mean "bug-free." Bugs found along the way included a counter underflow in a decompressor that produced an out-of-bounds write only on inputs of about 20 MB with one specific layout, and a rediscovery of CVE-2026-56132 in libexpat. Anthropic also reported that Claude Opus 5.5 proved half of a 36-task verification set using about 40% fewer tokens than Claude Opus 5, and that agents sharing a proof workspace used 17% fewer tokens than agents working alone. It noted that letting the model patch code opened a route to reward hacking, since a program rewritten to do nothing trivially never crashes, and that it penalized patches and audited them for this (Source: anthropic.com). Anthropic framed the work against frontier models' growing ability to find and chain software vulnerabilities and predicted that verification will become as practical as fuzzing for most production software; that forecast is the company's (Source: anthropic.com).
Greg Brockman of OpenAI, in an August 2026 essay on a "defender's window," likewise names applying mathematical-proof capabilities to software verification among defensive uses of AI, although the essay does not demonstrate complete formal verification of deployed systems (The Defender's Window (Brockman, 2026)).
In mathematics, proof assistants such as Lean are used to check machine-generated proofs, a use covered in AI for Science and Machine-produced mathematics: claims, verification and credit (Prove2Me formalization platform paper; Formalizing Fermat's Last Theorem (Anthropic, September 2026)). The Leiden Declaration on AI and mathematics lists "insisting on formal verification when appropriate" among standards of rigor for the field (Leiden Declaration on Artificial Intelligence and Mathematics (2026)).
Formal verification in AI safety proposals
Several proposals give formal verification a central place in assuring the safety of AI systems themselves.
- Provably safe systems. Max Tegmark and Steve Omohundro argued in September 2023 that powerful AI systems should be built to provably satisfy human-specified requirements, that advanced AI used for formal verification and mechanistic interpretability would soon make this technically feasible, and that it is "the only path which guarantees safe controlled AGI" (Source: arxiv.org).
- Guaranteed safe AI. A May 2024 paper by David "davidad" Dalrymple, Joar Skalse, Yoshua Bengio, Stuart Russell, Tegmark, Sanjit Seshia, Omohundro and others defines "guaranteed safe (GS) AI" as a family of approaches combining a world model, a safety specification, and a verifier that provides "an auditable proof certificate that the AI satisfies the safety specification relative to the world model." The authors argue the approach is necessary and that the main alternatives are inadequate (Source: arxiv.org).
- Public research funding. The UK Advanced Research and Invention Agency (ARIA) runs a Safeguarded AI programme led by Dalrymple that funds work combining scientific world models with mathematical proofs to obtain quantitative safety guarantees (Source: aria.org.uk); the University of Oxford describes it as part of a £59 million ARIA investment (Source: cs.ox.ac.uk).
- Safety cases. A framework for frontier-AI safety cases lists formal verification, or proofs that a system satisfies certain requirements, among possible sources of evidence, while describing it, alongside mechanistic interpretability and AI control, as a nascent field needing more investment (Safety Cases for Frontier AI).
- Controls on deployed systems. Arvind Narayanan and Sayash Kapoor include formal verification of code against specifications in a list of established engineering controls, with least-privilege access and reversible actions, that can constrain AI errors (AI as Normal Technology).
Debates and limitations
The main limitation, stated by verification practitioners and by AI developers, is the gap between a specification and the real world. Anthropic lists two forms in its 2026 work: the machine may behave in ways the model does not describe (its proofs cover RISC-V binaries linked against musl libc, while most deployments use x86 or ARM with glibc), and the proven claim may not cover everything of interest (AddressSanitizer does not detect all memory-safety bugs, not all entry points were verified, and callers can still misuse a library) (Source: anthropic.com). Proofs remain costly to produce; Anthropic reports that LLM-generated proofs can take hundreds of millions of tokens (Source: anthropic.com). For AI safety proposals the specification problem is larger, since the GS AI approach requires a mathematical world model and a mathematical description of acceptable effects, whose construction its authors identify as a main technical challenge (Source: arxiv.org).
See also
- AI and Cybersecurity
- Safety Cases (Frontier AI)
- AI Control
- AI for Science
- Machine-produced mathematics: claims, verification and credit
Relationships
- related: AI and Cybersecurity — verification as a defense against AI-assisted vulnerability discovery
- related: Safety Cases (Frontier AI) — formal proof as a proposed evidence source
- related: AI Control, Mechanistic interpretability — other assurance approaches named alongside it
- related: Reward Hacking — failure mode noted in model-written proofs
- supports: Safety Cases for Frontier AI, AI as Normal Technology, The Defender's Window (Brockman, 2026)
- related: Anthropic, Claude Opus 5.5
- related: Max Tegmark, Yoshua Bengio, Stuart Russell