PRISM Probabilistic Model Checker
PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that …
The Ultimate Formal Methods Toolbox
Discover, Explore, and Contribute to the World’s Largest Collection of Formal Methods ToolsWelcome to this collection of Formal Methods Tools, which aims to be the world’s most comprehensive source for information on tools for formal methods. From decades-old classics to cutting-edge tools, this site aims to put as much information as possible into one convenient place. Explore a wide selection of tools, contribute tools you make or love, and help grow the formal methods community.
Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site).
Try Something New
This list shows a selection of 20 random tools, refreshed every time this site is updated.
STAMINA Probabilistic Model Checker
A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces …
E Theorem Prover
E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with …
CaDiCaL SAT Solver
CaDiCaL is a simplified satisfiability solver.
dReal SMT Solver
[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems …
SMTInterpol Interpolating SMT Solver
SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and …
Alt-Ergo SMT Solver
Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools …
cvc5 Theorem Prover
cvc5 is an automatic theorem prover for SMT problems.
Q3B SMT Solver
[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which …
OpenSMT SMT Solver
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making …
COMICS DTMC Counterexample Generator
COMICS is a stand-alone tool which performs model checking and the generation of counterexamples for …
veriT SMT Solver
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
ParaFROST SMT Solver
ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA …
MathSAT SMT Solver
[ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help …
Vampire Theorem Prover
Vampire is a theorem prover.
Storm Probabilistic Model Checker
Storm is a tool for the analysis of systems involving random or probabilistic phenomena.
MiniSat SAT Solver
[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help …
Colibri SMT Solver
Colibri is an SMT solver.
Riss SAT Tool Collection
[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection.
Z3 Theorem Prover
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This …