Provers. What are they and why you might need one?

Before the list, one clarification, because the words “formal methods” cover three very different kinds of tools, and mixing them up is the most common confusion in this area. Let me give you my taxonomy:

1. Interactive theorem provers (also called proof assistants): Rocq, Lean, Isabelle, Agda… A human writes a proof — as a program term or as a tactic script — and the machine checks every step. You can prove an unbounded statement: “this compiler is correct for every valid C program”, “every finite group of odd order is solvable”. The price is manual effort: the landmark results below took person-years to person-decades.
2. Model checkers and specification tools: TLA+ with its TLC checker, Alloy. You do not verify a program at all — you write an abstract specification of a design (a state machine), and the tool exhaustively explores every behavior of a finite instance of it (say, 3 nodes and 2 messages in flight). Fully automatic, brutally effective at finding design bugs, but the deliverable is a debugged design, not a theorem. Lamport himself frames TLA+ as a blueprint tool: it is “useful for eliminating fundamental design errors, which are hard to find and expensive to correct in code”¹. The famous industrial user here is Amazon: their CACM paper describes pitching TLA+ to engineers as “exhaustively testable pseudo-code” while deliberately avoiding the words “formal”, “verification” and “proof” — and finding a DynamoDB bug whose shortest error trace was 35 steps long². Amazon also evaluated Alloy first and found it “not expressive enough for many of our use cases” — which tells you practitioners themselves put TLA+ and Alloy in the same category, separate from proof assistants².
3. SMT solvers: Z3 is the canonical one. Fully automatic decision procedures for restricted logical fragments (arithmetic, bit-vectors, arrays…). You do not write proofs in Z3 — you hand it a formula and get back sat/unsat. It is not an end-user proving environment but the engine that other verifiers are built on: Dafny, F*, Liquid Haskell, Why3 — and even TLAPS, the TLA+ proof system — all discharge their obligations to Z3 or its cousins³.

So TLA+ and Alloy are not in the list not because they are bad (they are wonderful), but because they answer a different question. This article is about category 1, with a guest appearance of category 3 at the end. If you want a deeper map of the interactive-prover world, the standard survey is “QED at Large”⁴.

To be fair about the labels: Z3’s own repository calls it “a theorem prover”, and TLA+ does ship a proof system (TLAPS). The honest distinction is not the name but the workflow and the deliverable: in category 1 a human constructs a machine-checked proof of an unbounded statement; in category 2 a machine exhaustively checks a bounded instance of a design; in category 3 a machine decides a formula in a restricted fragment.

Most widely used and established technology. Has a lot of great literature dedicated to it — the canonical entry point is the Software Foundations series, whose first volume, Logical Foundations, is a literate proof script you can execute chapter by chapter⁵.

Yes, about the name: Coq was renamed. The discussion started in 2021 (the English slang reading of the old name was scaring off newcomers, notably students), the decision was announced in October 2023, and the rename became official with the release of Rocq 9.0 on March 12, 2025. The new name honors Inria Rocquencourt, where the tool was born, and keeps a bird in the house via the mythical Roc⁶.

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity.  Qed.

It is based on the Curry-Howard correspondence: propositions are types, proofs are programs. It is possible to program in Coq in a fairly ordinary functional style, and a distinctive superpower the project itself advertises is extraction: you prove your program correct and extract certified OCaml, Haskell or Scheme from the proof development⁷.

What it is best at. Verified software and programming-language metatheory. If a POPL paper comes with a mechanized proof, the default vehicle is Rocq. The classical examples:

• CompCert — a formally verified optimizing C compiler by Xavier Leroy’s team, started around 2005, commercially supported today. The correctness theorem covers the whole way from C source to assembly⁸.
• The Four Color Theorem — Georges Gonthier and Benjamin Werner machine-checked the famously computer-assisted proof, completed 2004–2005⁹.
• Feit–Thompson (Odd Order) Theorem — Gonthier’s team formalized this landmark of finite group theory in 2012, building the Mathematical Components library along the way¹⁰.
• Iris — the higher-order concurrent separation logic framework, now the standard substrate for mechanized concurrency proofs¹¹, and on top of it RustBelt — the first machine-checked foundations for Rust, proving that the unsafe internals of the standard library are safely encapsulated¹².
• CertiKOS — the first functional-correctness proof of a complete concurrent OS kernel, from Yale¹³.

The authors on the competition. Funny enough, the Rocq team is the quietest of them all: the official FAQ merely lists Isabelle, HOL, Nuprl and PVS as “provers that are fairly similar to Coq by the way they interact with the user”, and the comparison page in the official wiki mostly discusses how to encode other systems’ logics into Coq¹⁴. The sharpest official comparison text involving Rocq actually lives in Lean’s FAQ — see below.

Where to start: Software Foundations, Volume 1: Logical Foundations⁵.

Popular prover developed after Haskell with laziness in mind. Also has a great tutorial and you would find this useful if you already have some Haskell knowledge.

What it is best at. Dependently-typed programming as proving. The official documentation defines Agda as “a dependently typed programming language” that “can be used as a proof assistant” — in that order¹⁵. There is no separate tactic language: you write proof terms by hand, interactively, refining typed holes in the editor. The official wiki’s own comparison page is refreshingly blunt about the trade: Coq proofs “can be much shorter, while Agda proofs are often more readable”, and Agda is deliberately more experimental — you can even switch off termination checking, “making a system possibly inconsistent, but more suitable for experimentation”¹⁶. Agda is also, via the --cubical extension, the leading practical vehicle for homotopy type theory: cubical Agda makes univalence and higher inductive types actually compute¹⁷.

Classical examples:

• Programming Language Foundations in Agda (PLFA) — Wadler, Kokke and Siek’s open-source textbook that teaches PL theory entirely in Agda, released 2018¹⁸.
• agda-unimath — a large community formalization of univalent mathematics, launched 2021¹⁹.

The authors on the competition. Ulf Norell’s 2007 PhD thesis, in which Agda 2 was designed, positions it explicitly: Cayenne made type checking undecidable by admitting general recursion; Epigram’s programming model was “a great inspiration” but its implementation “has not yet reached a level where it can be used for writing bigger programs”; Haskell GADTs and Dependent ML “only support a limited form of type dependencies”. Agda’s stated contribution was “proving that practical programming with dependent types is within our reach”²⁰.

Where to start: PLFA¹⁸.

First language which is trying to find a practical application of dependent types. Could be used as a prover, but is more a practical language with dependent types — and its author says so himself: the defining JFP paper states that Idris “is intended to be a general purpose programming language”, which is why it deliberately gives up Haskell-style full type inference — with dependent types, the types are the specification, so you want to write them²¹.

What it is best at. Type-driven development of ordinary software with dependent types: length-indexed vectors, type-safe printf, protocols and state machines encoded in types. Idris 2 adds a genuinely new trick — it is “the first implementation of quantitative type theory in a full programming language”: every variable carries a multiplicity 0, 1 or ω, so the types can guarantee that a value is erased at runtime or used exactly once (hello, linear session-typed channels)²². Idris 2 is also self-hosted — “the first language with full first-class dependent types implemented in itself”²².

The authors on the competition. Brady’s papers have honest related-work sections: against Agda, he notes Agda bakes metavariables and implicit arguments into the type theory itself, which makes implicits more flexible “at the expense of complicating the type system”, whereas Idris elaborates down to a tiny core kernel; against Rust, he positions QTT as the cleaner way to combine linear and dependent types “with no restrictions on whether variables are used in types or terms”^{21, 22}.

Where to start: Type-Driven Development with Idris, Brady’s own book²³.

Most esoteric language among all of the contenders. Contains a proof language, a language with dependent types and refinement types and many more tricks for low-level programming. You can write type-safe malloc and free with it and do type-safe pointer arithmetic. We’ll take a closer look at ATS later in other articles too.

What it is best at. Low-level systems programming where the proofs live next to C-level code. ATS (“Applied Type System”, Hongwei Xi) compiles to C and combines dependent types with linear types, which is exactly the combination you need to track memory ownership at compile time. Xi’s own papers position ATS against pure type theory: the design separates the statics from the dynamics precisely to keep dependent types practical for programming, an approach he calls “programming with theorem-proving”²⁴. Its signature demo used to be the Computer Language Benchmarks Game, where a past version of the game showed ATS running head-to-head with C and C++ — worth phrasing as history, since ATS is no longer in the current game²⁵. The largest ATS artifact is the ATS2 compiler itself, over 180,000 lines of ATS²⁶, and ATS3 development is still alive in 2026²⁷.

Where to start: Introduction to Programming in ATS, Xi’s official book²⁸.

Prover developed by JetBrains Research. Based on the HoTT approach and gives you a few interesting tricks + a perfect IntelliJ IDE to work in. No more Emacs!²⁹

What it is best at. Being a HoTT-native prover with industrial IDE polish. Arend implements a homotopy type theory with a primitive interval type (“which syntax is similar to cubical type theory”, say the docs), which per its authors gives “a simple and clean definition of higher inductive types (including recursive ones)” — the comparison with cubical Agda and Coq’s axiomatic HoTT library is implicit but real: there, univalence is a flag or an axiom; here it is the native foundation²⁹. The standard library, arend-lib, covers algebra, category theory, homotopy theory and topology in HoTT style³⁰.

A word of caution: as of mid-2026 the project looks dormant — the last release was in July 2024 and the repositories have been quiet since early 2025. A beautiful design to study, but maybe not the horse to bet a project on.

Where to start: the official documentation and tutorial³¹.

Very practical prover. Not hyped, but people just silently do the real stuff with it. Also this is the only prover in this list which is not using dependent types, and it makes it extra interesting to take a look at what alternative approach they employ.

What it is best at. Industrial-strength verification with the best automation in the business. Isabelle/HOL’s foundation is classical simple type theory — Church’s higher-order logic, no dependent types — and the payoff for that conservatism is Sledgehammer: one command that ships your goal to a fleet of automatic provers (E, Vampire, Z3, cvc5) and reconstructs whatever they find as a checked Isabelle proof. Its Isar proof language reads closer to mathematical prose than any tactic script. And its library, the Archive of Formal Proofs, is a refereed journal of proof developments — as of 2026, nearly a thousand entries and over five million lines of proof³².

Classical examples:

• seL4 — the first formal proof of functional correctness of a general-purpose OS kernel (2009): 8,700 lines of C and 600 lines of assembler, verified by roughly 200,000 lines of Isabelle proof. The verification process found 144 bugs in an early version of the C code³³.
• Flyspeck — the formal verification of Hales’s proof of the Kepler conjecture, completed 2014. The main body was done in HOL Light; Isabelle’s part was the verified enumeration of tame planar graphs³⁴.

The authors on the competition. This is the goldmine of the whole genre. Lawrence Paulson, Isabelle’s original author, writes a blog where he takes on the comparison directly: “Why not just use Lean?” (2026) grants Lean its great language, tools and enthusiastic community, then argues Isabelle offers “the best automation anywhere” and more legible proofs — and pointedly notes that dependent types are discouraged even inside Lean’s own mathlib³⁵. In “Why don’t you use dependent types?” (2025) and the paper “Formalising Mathematics in Simple Type Theory” he argues Church’s 1940 logic is enough for serious mathematics^{36, 37}. And when people claimed Grothendieck’s schemes require dependent types, his group formalized schemes in Isabelle/HOL, showing “the powerful dependent types of Coq or Lean can be traded for a minimalist apparatus called locales”³⁸.

Where to start: Concrete Semantics by Nipkow and Klein — part I is the standard “Programming and Proving in Isabelle/HOL” tutorial³⁹.

Prover started at Microsoft Research by Leonardo de Moura (Lean’s home today is the Lean FRO). Has a very nice intro tutorial and VS Code plugin. This is one of the more practical of these languages and you can easily write real programs with it, compile and run.

What it is best at. Formalizing research-level mathematics at scale — Lean is the prover working mathematicians actually adopted. The gravitational center is mathlib, the community-built library: over 1.5 million lines, on the order of 200,000 theorems, 500+ contributors⁴⁰. Because the mathematicians are there, the AI-for-math people are there too: DeepMind’s AlphaProof, which reached silver-medal standard at IMO 2024, proves its statements in Lean⁴¹. Lean 4’s second story is that it is a genuine general-purpose programming language, implemented in itself, where users can extend the parser, elaborator and tactics in the same language they prove in⁴².

Classical examples:

• Liquid Tensor Experiment — Peter Scholze challenged the community in December 2020 to formalize his hardest recent theorem (condensed mathematics); completed July 2022, widely cited as the moment formalization reached the frontier of research math⁴³. (Honesty note: this one, like the sphere eversion project, was done in the Lean 3 era.)
• PFR conjecture — Terence Tao led a crowdsourced Lean 4 formalization of the freshly-proved Polynomial Freiman–Ruzsa conjecture in roughly three weeks in late 2023 — the canonical example of formalizing a result almost as soon as it is proved⁴⁴.
• Fermat’s Last Theorem — Kevin Buzzard’s team at Imperial is formalizing Wiles/Taylor–Wiles in Lean 4; started 2024, ongoing⁴⁵.

The authors on the competition. The official FAQ has literally the sections we want: “Is Lean just like Rocq?” (similar type-theoretic foundations — both are descendants of the Calculus of Inductive Constructions — but Lean commits to definitional proof irrelevance, “scalability, automation, and a focus on classical logic”) and “Is Lean just like Isabelle?” (dependent type theory with explicit proof terms and a small kernel vs. Isabelle’s HOL-and-LCF approach; the FAQ argues — partisan claim, mind you — that dependent types suit mathematics better)⁴⁶. The system papers, CADE-25 for Lean’s debut (“bridge the gap between interactive and automated theorem proving”) and CADE-28 for Lean 4 (full extensibility as the differentiator from other ITPs), complete the picture^{47, 42}.

Where to start: the official recommendation for absolute beginners is the Natural Number Game⁴⁸; the books are Theorem Proving in Lean 4 and, for programmers, Functional Programming in Lean⁴⁹.

One more contender by Microsoft Research (together with Inria). F* has been used to verify real software that you are, right now, running: code from the HACL* verified cryptographic library ships in Firefox’s NSS, the Linux kernel (via WireGuard’s Curve25519), and — since Python 3.12 — CPython’s hashlib falls back to HACL* implementations of SHA-2/SHA-3/MD5 when OpenSSL doesn’t provide them^{50, 51}.

What it is best at. Proof-oriented programming with SMT muscle. F*’s own book states the positioning perfectly: “F*’s dependent types are similar in expressiveness to Coq, Lean, Agda, or Idris”, but “F*’s use of an SMT solver for proof automation is unique among languages with dependent types” — you write a dependently-typed program, and Z3 discharges most proof obligations silently⁵². Verified code extracts to OCaml, C (via KaRaMeL) and even assembly. The flagship is Project Everest (2016–2021), the verified-HTTPS-stack umbrella that produced HACL*, EverCrypt and miTLS⁵³. The same book is also honest about the trade: “relatively little pure mathematics has been formalized in F*”, and Isabelle and Coq are more mature tools⁵².

Where to start: Proof-Oriented Programming in F*, the official book by Swamy, Martínez and Rastogi⁵².

After the taxonomy section you already know the punchline: Z3 is not an interactive prover, it is the automatic engine under everyone else’s hood. Developed at Microsoft Research by Leonardo de Moura (yes, the same one — he built Z3, then went off to build Lean) and Nikolaj Bjørner, presented in the classic TACAS 2008 paper³. You give it a first-order formula over arithmetic, bit-vectors, arrays; it answers sat or unsat. No tactics, no proof scripts. Dafny, F*, Liquid Haskell, Why3 and even TLA+’s proof system all stand on it. If interactive provers are mathematicians, Z3 is the calculator they all keep in the drawer.