A Reference of Formal Verification Tools
Last updated
Adding "verified" to a piece of software is a powerful adjective, and there are several meanings it can take, with different levels of guarantees and scopes: From a proven Rocq definition of the algorithm used to generate Haskell code, to a loop invariant in your Rust source code.
This page lists different approaches and tools that can be used for verification.
Help us keep this reference accurate
This reference is a work in progress. If you spot something wrong or out of date, or think a tool should be on the list, let us know and we will update it. Email us at contact@quint.sh.
With AI writing more of the software we all rely on, many teams are working on improving the guardrails that keep software behaving correctly. Software testing techniques are responsible for most of the work, but formal methods are known for covering cases that tests might miss, in unusual interleavings, edge-case inputs, and against implicit assumptions.
No single tool fits every job, so the sections below group tools by approach, from writing a model to proving properties of the code you already have. The right choice depends on the problem in front of you, and your strategy to protect your software, from design to production.
Write a model and check properties
with model checkers
A model is a high-level description of a system, usually as a state machine. Because it abstracts away implementation details, a model stays small enough to check powerful properties, such as whether a bad scenario can happen in any possible ordering of events. Model checkers do this automatically, with no proofs to write, and show a step-by-step counterexample when a property fails. A model does not tell you whether the code matches it, so that gap has to be closed separately, with conformance testing techniques. Models are great design documents and serve as a reference for how the software should behave (during testing and production too).
Specifies systems in set theory and temporal logic, checked with the TLC or Apalache model checkers and the TLAPS prover. Widely used in industry, including at AWS, Microsoft, and Intel.
An official MCP server in the VS Code extension, plus official agent skills. Specula derives TLA+ models from existing code.
TLA+'s semantics in a typed, programming-style syntax, with tests. Can be transpiled to TLA+, and uses the same model checkers. Offers model-based testing via Quint Connect.
Official skills teach coding agents to write and check Quint specs. Quint Studio keeps AI-written code tied to the spec.
TLA+'s semantics in imperative style. Labels mark atomic steps, which suits concurrent algorithms. Transpiles to TLA+ and uses the same model checkers.
The MCP server in the TLA+ VS Code extension also handles PlusCal.
Specs in Starlark, a Python subset, with crashes and interleavings modeled for you. It can also estimate performance and reliability probabilistically.
Official Claude Code skills for writing, checking, and debugging specs, and for model-based tests.
Models systems as state machines exchanging asynchronous events and explores their orderings. Used most for distributed cloud services, notably at AWS.
PeasyAI, an official MCP server, turns design documents into checked P code.
Checks processes that communicate over channels against temporal properties, scaling to very large state spaces. Used most for protocols and embedded software.
Keeps proof obligations in a decidable logic, so checking an inductive invariant is automatic and predictable. Used most for protocol proofs.
Models are TLA+-style transition systems embedded in Lean 4, so one model can be model checked, proved with SMT automation, and finished with interactive proofs where needed.
Models structures as sets and relations and finds bounded counterexamples, shown as diagrams. Used most for data models, access policies, and configurations.
Computes probabilities and expected values over Markov models, such as the chance of reaching a bad state. Used for randomized algorithms, protocols, and reliability analysis.
Write theorems and prove them
with proof assistants
Proof assistants let you state more general theorems, such as a property that holds for any number of processes or any input size, and prove them with full mathematical rigor. The cost is effort: each proof has to be written down step by step, although AI has recently become very helpful at writing them. The gap between what you proved and the code that runs remains, but some tools can generate executable code from verified definitions, so that code is correct by construction.
Dependent type theory with a tactic language and extraction to OCaml, Haskell, or Scheme. Used most for verified compilers, cryptographic code, and language research.
Classical higher-order logic, with Sledgehammer calling external provers to find proof steps. Used most for OS and algorithm verification, and mathematics.
Early community MCP servers expose proof state and Sledgehammer to agents.
A proof assistant that is also an efficient programming language. Home of Mathlib, one of the largest formalized math libraries, and the main target of AI provers.
The main target of AI provers such as Aristotle and Leanstral, with official skills, a popular MCP server, and LeanCopilot for tactic suggestions.
Proofs are written directly as programs by filling typed holes, mostly without tactics. Used most in type theory and programming language research.
A community MCP server lets agents fill holes, split cases, and search for proofs.
Write code in
verification-aware languages
These languages keep the code, its specification, and its proofs in one place, so what you verify is the program you run once it is compiled or extracted to a mainstream language. Most of them use SMT solvers to discharge proof obligations automatically, which means much less proof writing than in a proof assistant. The trade-off is that the verified parts have to be written in the new language and connected to the rest of your system, and interactions between concurrent processes are usually hard to express with these tools.
Write contracts and loop invariants next to the code, and an SMT solver proves them as you type. Compiles to C#, Java, JavaScript, Go, and Python.
dafny-annotator, a research tool, uses LLMs to add the annotations Dafny proofs need.
Dependent types plus SMT automation and an effect system, extracting to OCaml, F#, or C. Used most for verified cryptography and parsers.
An official Claude Code plugin with an F* agent and proof-debugging skills, plus an MCP server.
Sends each proof obligation in its WhyML language to whichever prover suits it, from SMT solvers to Rocq. Also the proof engine behind SPARK and Creusot.
General-purpose programming with first-class dependent types. Idris 2 tracks whether each value is used never, once, or freely, so types can enforce resource protocols.
Prove properties directly
on the code you already have
These tools check properties in code that is written in a mainstream language, through contracts, annotations, or test-like harnesses added to the existing code, with no separate model to keep in sync and little to rewrite.
Limitations to keep in mind
- Real code has every implementation detail, so verification tasks are much heavier, and automatic checks often stop at a bound, such as a number of loop iterations.
- Each tool covers a subset of its language and libraries, and the rest has to be modeled by hand or trusted.
- Most check one program at a time, so bugs from interactions between services, often the costliest ones, are usually out of reach.
Rust
Checks unit-test-like harnesses over all inputs up to a bound, including unsafe code, for panics, overflows, and many kinds of undefined behavior.
AProver, a research agent, writes specs and harnesses for Rust functions and checks them with Kani.
Specs and proofs written as Rust ghost code and checked quickly by SMT. Handles raw pointers and concurrency; used most for systems software.
Microsoft Research agents, co-authored by Verus developers, that generate Verus proofs.
Uses Rust's ownership types to generate much of each proof, so safe code needs few annotations. Proves code cannot panic, plus custom contracts.
Handles mutable borrows with prophecies, keeping proofs about mutation well automated. Specs are written in Pearlite, a Rust-like logic.
Model checks Rust actors across all message orderings. Actors are plain Rust and can run on a real network, but the system must be built as Stateright actors.
C and C++
Analyses for C with ACSL contracts: Eva proves the absence of runtime errors, WP proves functional contracts. Used most in aerospace and energy.
A community MCP server for running Eva and WP from agents.
Checks every execution up to a loop bound for memory errors, overflows, and failed assertions, with no annotations needed. Used most for embedded C.
AProver, a research agent co-authored by CBMC's creator, writes specs and triages CBMC counterexamples.
Go
Verifies annotated Go, including goroutines and channels, using separation logic. Proves memory safety, absence of crashes, and functional properties.
Python
Verifies type-annotated Python against contracts, including runtime errors, termination, and deadlock freedom.
An official MCP server and Claude Code plugin for verifying and debugging from agents.
Ada
A subset of Ada whose contracts are proved automatically, adoptable one module at a time. Used most in avionics, rail, and defense.
Official AdaCore skills for GNATprove that work with most coding agents, plus an MCP server.
Smart contracts
Proves rules for all inputs or returns a counterexample. Supports EVM chains, Solana, Stellar, and Sui; used most for DeFi invariants.
AutoProver writes and proves CVL specs for Solidity, and AI Composer generates code checked against them.
Define a language's semantics once and get an interpreter and verifier from it. Used most to verify EVM smart contracts.
New and worth watching
These tools launched recently, so we list them separately so you can evaluate maturity on your own.
A dependently typed language that runs in parallel on CPUs and GPUs, where the compiler re-checks proofs of stated laws after every change.
Status: Released in September 2026; no tactics or proof search yet.
Verifies //@ contract comments in ordinary TypeScript by translating it to Dafny or Lean, leaving production code unchanged.
Status: Tech preview since April 2026.
A Dafny-style verifier embedded in Lean 4, where programs can be run, tested, and verified, mixing SMT automation with interactive proofs.
Status: Research prototype, published at CAV 2026.
One-line claims above Rust functions, checked at the rigor you choose, with alerts when code drifts from its claim.
Status: Alpha; checks by tests and formal proof are only for design partners so far.
Comparison table
A quick reference: what you express with each tool, how it checks it, and whether it has AI tooling.
| Tool | You express | How it checks | AI tooling |
|---|---|---|---|
| TLA+ | State machines via actions, invariants, and LTL properties, in math notation | Explicit-state (TLC), symbolic (Apalache), proofs (TLAPS) | Official |
| Quint | State machines via actions, invariants, and LTL properties, in typed code | Simulator; Apalache (symbolic) and TLC backends | Official |
| PlusCal | State machines via imperative TLA+, and properties in TLA+ | TLA+ tools after translation | Official |
| FizzBee | State machines via actions, and assertions, in a Python-like language | Explicit-state model checker; probabilistic analysis | Official |
| P | Communicating state machines and specification monitors | Systematic exploration of event orderings | Official |
| Spin / Promela | Communicating processes and LTL properties | Explicit-state model checking of LTL properties | None found |
| Ivy | State machines and invariants, in a decidable logic | SMT, with decidable queries | None found |
| Veil | State machines via actions, and invariants, in Lean | Model checking, SMT, and Lean proofs | None found |
| Alloy | Relations, constraints, and assertions | SAT solving within a bounded scope | None found |
| PRISM | Probabilistic state machines and probabilistic properties | Probabilistic model checking | None found |
| Rocq (formerly Coq) | Theorems and proofs via tactics | Proof kernel checks every step | Community |
| Isabelle/HOL | Theorems and structured proofs | Proof kernel; Sledgehammer calls external provers | Community |
| Lean 4 | Theorems and proofs via tactics | Proof kernel checks every step | Official |
| Agda | Theorems and proofs as programs | Type checking | Community |
| Dafny | Programs with contracts | SMT (Boogie, Z3) | Research |
| F* | Programs with specifications in their types | Type checking and SMT (Z3) | Official |
| Why3 | Programs with contracts | SMT solvers, or Rocq and Isabelle for hard goals | None found |
| Idris | Programs with properties in their types | Type checking | None found |
| Kani | Test-like harnesses with assertions, for Rust | Bounded model checking (CBMC) | Research |
| Verus | Rust with specifications and proofs | SMT (Z3) | Research |
| Prusti | Rust with contracts | Viper (SMT) | None found |
| Creusot | Rust with contracts | Why3 (SMT) | None found |
| Stateright | Rust actors and their properties | Explicit-state model checking | None found |
| Frama-C | C with contracts | Abstract interpretation (Eva), deductive proof (WP) | Community |
| CBMC | C with assertions | Bounded model checking (SAT/SMT) | Research |
| Gobra | Go with contracts | Viper (SMT) | None found |
| Nagini | Python with contracts | Viper (SMT) | Official |
| SPARK | Ada with contracts | GNATprove (SMT, via Why3) | Official |
| Certora Prover | Rules about smart contracts | SMT | Official |
| K Framework | Language semantics and claims | Symbolic execution and SMT | None found |
AI tooling: Official means from the tool's maintainers, Community means third-party projects, and Research means research prototypes. Each card links to them.
How to choose
The first factor to consider is whether the tool/language can express the properties you care about and enough of the system/environment and adversarial surface that threaten it.
Then, consider the balance of cost and level of guarantee: if your software changes fast, it might not justify expensive proofs, while if it's a stable algorithm you don't intend to change, a full mathematical proof might be worth it.
Finally, consider the strategy to bridge any confidence you get out of formal verification to your code: every pull request has potential to break the things you verified, and guardrails need to enforce correctness continuously. Conformance testing and code generation can help, or using verifiers for the code itself when their expressivity and power match your correctness requirements.
Frequently asked questions
TLA+, Quint, FizzBee, P, and PlusCal are the common options. TLA+ is the most established option. Quint and PlusCal can transpile to TLA+, with Quint having a modern syntax but keeping the declarative structure, while PlusCal keeps a lot of the syntax but has an imperative structure. FizzBee and P have actor-model definitions.
Quint and FizzBee are the two aimed squarely at approachability. Quint keeps TLA's semantics and can leverage the same verifiers, while FizzBee has new paradigms and uses its own model checker.
Combine many techniques from testing to formal verification. Formally verify the most important components using the tools that can better express your properties and environment. For example, concurrent and distributed systems have properties that span multiple processes and an environment that allows interleavings, so TLA+ and similar tools are a good fit. Use conformance testing techniques to bridge the gap between specification and code.
Increasingly, yes. Quint's agent skills and Specula help coding agents draft specifications, Certora's AutoProver proposes smart contract properties, and AI provers such as Harmonic's Aristotle write Lean proofs. The output is still checked by a model checker or proof kernel, so what you need to review is whether the specification says what you meant.
Start with a lightweight specification language rather than a proof assistant. Quint and FizzBee let you model a small critical component and check its properties in hours. Leverage AI, but spend time understanding what is being checked and what is not covered.
Help us keep this reference accurate
This reference is a work in progress. If you spot something wrong or out of date, or think a tool should be on the list, let us know and we will update it. Email us at contact@quint.sh.
Try Quint on your next spec
Executable specifications, model checking, simulation, and model-based testing, in a language that any software developer can read.
