Formal Methods Tools

All Tools

This page lists all of the tools on this site in alphabetical order. Click a tool name in the first column to view tool details. Click a colorful item in the second column to view all the tools for which that term applies. Item colors mean nothing and are intended to make it easy to skim the page. Colors are generated by hashing each term’s name and converting it to RGB color values.

Tool Applications Licenses
Model Checker CRAPL
ABC Theorem Prover Model Checker MIT
Abella SMT Solver Theorem Prover SAT Solver GPLv3
Aeneas Program Prover Rust Verifier Apache-2.0
Agda 2 Theorem Prover Specification Language MIT
Alt-Ergo SMT Solver OCamlPro-Non-Commercial
Andromeda Theorem Prover BSD-3-Clause
Arend Theorem Prover Apache-2.0
Theorem Prover
AVR Model Checker GPL-3.0
Aya Prover Theorem Prover MIT
BEAGLE SMT Solver Theorem Prover SAT Solver MIT
Bitwuzla SMT Solver Theorem Prover SAT Solver MIT
Model Checker Apache-2.0
Theorem Prover Yolo
SMT Solver Theorem Prover SAT Solver MIT
CaDiCaL SAT Solver MIT
CADP Model Checker All Rights Reserved
Caesar Probabilistic Program Prover MIT
CGAAL Model Checker AGPL-v3
Chyp Theorem Prover Apache-2.0
Cobra Static Analyzer MIT
CodeGen2 Program Synthesizer Apache-2.0
Colibri SMT Solver MIT
COMICS Counterexample Generator
Concuerror Model Checker BSD-2-Clause
contractLarva Runtime Verifier Apache-2.0
Copilot Runtime Verifier
CPAchecker Model Checker Apache-2.0
Creusot Program Prover Rust Verifier LGPLv2.1
CryptoMiniSat SAT Solver MIT GPLv2
cur Theorem Prover Specification Language BSD-2-Clause
SMT Solver Theorem Prover BSD-3-Clause
cvc5 SMT Solver Theorem Prover BSD-3-Clause
Dafny Program Prover MIT
detectEr Runtime Verifier GPL-3.0
Visualizer
DNNF Neural Net Verifier MIT
DNNV Neural Net Verifier MIT
SMT Solver Apache-2.0
DSCheck Model Checker ISC
E Theorem Prover GPLv2
easy-rte Runtime Verifier MIT
Eldarica Model Checker BSL
ESBMC Model Checker Apache-2.0 BSD 4-clause MIT BSD 3-clause GPLv3
Fast Downward PDR Model Checker GPL-3.0
fbPDR Model Checker MIT
Fiat Program Synthesizer MIT
FMDNN Neural Net Verifier
Model Checker GPL-3.0
Gappa SMT Solver Theorem Prover SAT Solver MIT
Geyser Model Checker MIT
Gillian Program Prover BSD-3-Clause
Glucose SAT Solver MIT
Theorem Prover Apache-2.0
hlola Runtime Verifier MIT
Holbert Theorem Prover BSD-3-Clause
IMITATOR Parameter Synthesizer GPLv3
ImSpin Model Checker MIT
Incremental Neural Network Verifiers Neural Net Verifier MIT
Model Checker BSD-3-Clause
Isabelle Theorem Prover BSD-2-Clause
IVAN Neural Net Verifier
Runtime Verifier BSD-3-Clause
IVy
Protocol Verifier MIT
JANI Modeling Language Apache-2.0 MIT
Runtime Verifier
Kani Model Checker Rust Verifier Apache-2.0 MIT
Kind 2 Model Checker Apache-2.0
knuckledragger Theorem Prover MIT
Lakeroad Program Synthesizer MIT
Lambdapi Theorem Prover
LEAN Theorem Prover Modeling Language Apache-2.0
Lingeling SAT Solver MIT
LISA Theorem Prover Apache-2.0
Loom Rust Verifier MIT
Loom Rust Verifier MIT
Model Checker
LTSmin Model Checker BSD-3-Clause
MathSAT SMT Solver All Rights Reserved
Model Checker
mCRL2 Model Checker BSL
Megalodon Theorem Prover MIT
Model Checker MIT
MESA Runtime Verifier NASA Open Source
SMT Solver Theorem Prover SAT Solver MIT
MetiTarski University of Cambridge MIT
SAT Solver MIT
Program Synthesizer MIT
Miri Rust Verifier Apache-2.0 MIT
Momba Modeling Framework Apache-2.0 MIT
Model Checker MIT
Narya Theorem Prover GPL-3.0
Program Synthesizer MIT
NuSMV Model Checker LGPL
NuXMV Model Checker All Rights Reserved
OpenSMT SMT Solver GPLv3
Theorem Prover
ParaFROST SAT Solver GPLv3
Paranoid Scientist Runtime Verifier MIT
PDRC Model Checker
Pnmc Model Checker BSD-2-Clause
Princess SMT Solver Theorem Prover SAT Solver MIT
Probabilistic Invariant Synthesizer
PRISM Probabilistic Model Checker GPLv2
SMT Solver Theorem Prover SAT Solver MIT
Parameter Synthesizer GPLv3
PROSE Program Synthesizer MIT
Prover9 Theorem Prover
Rust Verifier Mozilla-2.0
PVS Theorem Prover GPL-2.0
pyPL Model Checker Model Generator Theorem Prover Unilicense
Q3B
SMT Solver MIT
QEA
Runtime Verifier Specification Language MIT
Qrhl-tool Theorem Prover MIT
R2U2 Runtime Verifier MIT Apache-2.0
RbSyn Program Synthesizer BSD-3-Clause
Reach Model Checker MIT
rIC3 Model Checker GPL-3.0
SAT Solver LGPLv2
Rocq Theorem Prover LGPL-2.1
Roméo Model Checker GPL
ROSMonitoring Runtime Verifier MIT
Runtime Verifier
Rumur Model Checker Unilicense
Runtime Verifier GPL-3.0
Sally Model Checker GPLv2
SASyLF Theorem Prover
Theorem Prover
Model Checker GPL-3.0
SM(P/)T Model Checker GPLv3
SMT-RAT SMT Solver SAT Solver MIT
SMTInterpol SMT Solver GPLv3
SpaceEx Hybrid Systems GPLv3
SPASS SMT Solver Theorem Prover SAT Solver All Rights Reserved
Spin Model Checker All Rights Reserved
STAMINA Probabilistic Model Checker MIT GPLv3
stateright Model Checker MIT
Storm Probabilistic Model Checker GPLv3
STP Constraint Solver SMT Solver Theorem Prover MIT
TAPAAL Model Checker GPL-2.0
Model Checker
TLA+ Modeling Language
Tree Diffusion Program Synthesizer MIT
Uppaal Model Checker All Rights Reserved
Vampire Theorem Prover BSD-3-Clause
VeRAPAk Neural Net Verifier MIT
verifyDNN Neural Net Verifier
Verifying-DNN Neural Net Verifier
VeriGauge Neural Net Verifier MIT
VeriStable Neural Net Verifier
veriT SMT Solver BSD-2-Clause
Verus Rust Verifier MIT
Whiley Theorem Prover Theorem Prover Apache-2.0
Why3 SMT Solver Theorem Prover SAT Solver MIT
Yices 2 SMT Solver SAT Solver GPLv3
Z3 SMT Solver Theorem Prover SAT Solver MIT
Model Checker
Zipperposition Theorem Prover BSD-2-Clause
Red dot indicates tool has not been updated or maintained recently