Formal methods tools
What tools exist, what problem each one checks, and how much traction each has: how many job postings name it, its Google search trend and its GitHub stars.
Landscape by problem type
Section titled “Landscape by problem type”Each group below is “what problem you’re checking” → the tools that do it.
Design-level models (find bugs in the protocol before code exists) TLA+, Alloy, PlusCal, Quint, P, SPIN/Promela. You write an abstract model, the checker explores states. Best fit for distributed systems, consensus, cache coherence, API state machines.
Proof assistants (prove theorems and programs by hand, with tactics) Lean, Coq/Rocq, Isabelle/HOL, Agda, Idris. Deep guarantees, high effort. Used for compilers, crypto proofs, math, language semantics.
Contract-based verification of real code (annotate functions, a solver proves them) SPARK (Ada), Frama-C (C), Dafny, Why3, Verus and Creusot (Rust), JML/OpenJML (Java). You write pre/postconditions and invariants alongside normal code. This is the closest thing to “verified engineering” as a day job.
Model checkers for actual source code CBMC (C/C++), Java Pathfinder, Kani (Rust). Bounded checking of real programs rather than an abstract model.
Static analysis / abstract interpretation (prove absence of crash classes, no annotations) Astrée, Polyspace, Infer, CodeQL, Coverity. Lower ceiling, much lower cost, so this is what large companies actually deploy.
SMT and SAT solvers (the engines under most of the above) Z3, CVC5, Yices, MiniSat. Also used directly for scheduling, config validation, program synthesis.
Cryptographic protocol verification Tamarin, ProVerif, EasyCrypt, CryptoVerif. TLS 1.3 and Signal were analyzed with these.
Hardware verification SystemVerilog Assertions, JasperGold, SymbiYosys, ACL2. Oldest and most commercially mature branch of the whole field.
Type systems as lightweight verification Liquid Haskell, refinement types, Rust’s borrow checker, dependent types in Idris. Weaker guarantees, but they ride along with normal development.
Runtime verification and property testing Jepsen, TLA+ trace checking, QuickCheck/Hypothesis, Antithesis, deterministic simulation testing. Doesn’t prove anything, catches a lot. Highest practical payoff per hour.
The field looks huge because it grew from three separate communities — math, hardware, and safety-critical software — that never merged. Lots of overlapping tools, small user bases each.
Which tools people actually get hired for
Section titled “Which tools people actually get hired for”Demand is counted by how many postings on Job postings name each tool directly. It skews hard toward proof assistants, not model checkers — Lean and Coq/Rocq beat TLA+ by a wide margin, even though neither is a model checker.
The Trend column is Google Trends search interest over the last 12 months (worldwide), included only where the term maps to a single, unambiguous Trends topic — most tool names here are too generic or collide with unrelated words (“Coq” is French for rooster, “Agda” without disambiguation returns a food brand) to trust a plain keyword search, so most rows don’t get one rather than showing misleading data. GitHub ★ is each project’s current star count, checked directly via the GitHub API; closed-source or non-GitHub-hosted tools (Antithesis, Certora, UPPAAL, CryptoVerif, MathSAT) don’t get one.
| Tool | Job mentions | What it is | Trend (12mo) | GitHub ★ |
|---|---|---|---|---|
| Lean / Lean 4 | 9 | Interactive theorem prover — the single most-named tool found, concentrated at AI labs (Harmonic, DeepMind, Oath Technologies). |  | 9,234 |
| Coq / Rocq | 8 | Interactive theorem prover, same AI-lab cluster as Lean. |  | 5,581 |
| SMT solvers (Z3, CVC5, MathSAT) | 8 | Underlying decision engine for most higher-level tools; rarely hired for by name alone. |  | Z3: 12,702 · CVC5: 1,361 |
| TLA+ / TLC / Apalache | 6 | Exhaustive model checker — Huawei, Oracle, Architect Labs, Sigil Logic, Johns Hopkins APL, Google Cloud. |  | TLA+: 3,058 · Apalache: 599 |
| Isabelle/HOL | 4 | Interactive theorem prover; used for the seL4 verified microkernel. |  | — |
| Agda | 2 | Interactive theorem prover, both mentions at Harmonic. |  | 2,928 |
| Verus | 1 | Verification-aware Rust, used for Google Cloud’s C++→Rust migration. | — | 3,192 |
| Alloy | 1 | Spec language + model finder (Kodkod engine); 1 posting (Sigil Logic). |  | 868 |
| SPIN | 1 | Model checker for protocols, its own language (Promela); 1 posting (Johns Hopkins APL). |  | 476 |
| Quint | 0 | Modern executable-spec successor to TLA+, built by Informal Systems. | — | 1,685 |
| P (AWS) | 0 | State-machine modeling language, used internally across S3/DynamoDB/EC2. | — | 3,687 |
| Antithesis | 0 | Closed deterministic-simulation SaaS — can’t have a job posting since it’s proprietary tooling companies buy, not a skill anyone lists. | — | — |
| QuickCheck/Hypothesis | 0 | Property-based testing (Haskell/Python); widely adopted, never hired for by name. | — | Hypothesis: 8,997 · QuickCheck: 790 |
| Coyote | 0 | Microsoft’s systematic concurrency tester for C#, internal Azure tool. | — | 1,598 |
| FizzBee | 0 | Open-source, more approachable alternative to TLA+. | — | 350 |
| Stateright | 0 | Embedded model checker as a Rust library. | — | 1,882 |
| stateproof | 0 | TypeScript DSL compiling to TLA+; the closest TS-to-TLA+ tool found. | — | 2 |
| loom | 0 | Rust concurrency-permutation tester, under the Tokio project. | — | 2,823 |
| XState graph | 0 | Exhaustive state-graph traversal for XState machines, from Stately.ai. | — | 30,138 |
| fast-check | 0 | TypeScript/JS property-based testing, 139M downloads/month. | — | 5,149 |
| Certora Prover/CVL | 0 | SMT-based prover for smart contracts (Solidity/Solana/Move). | — | — |
| K Framework/KEVM | 0 | Semantics framework; KEVM targets EVM bytecode. | — | 591 |
| Cryptol/SAW | 0 | Haskell-hosted crypto spec DSL + Software Analysis Workbench (Galois). |  | Cryptol: 1,221 · SAW: 518 |
| Dafny | 0 | Verification-aware language, compiles to C#/Java/JS/Go/Python. |  | 3,548 |
| UPPAAL | 0 | Timed-automata model checker (academic, Uppsala/Aalborg). | — | — |
| EasyCrypt | 1 | Cryptography-specific interactive theorem prover; 1 posting (Riverside Research). | — | 416 |
| F* | 1 | Dependently-typed proof assistant, used in Project Everest (verified TLS); 1 posting (Riverside Research). | — | 3,109 |
| CryptoVerif | 1 | Automated cryptographic protocol verifier, game-hopping proofs; 1 posting (Riverside Research). | — | — |