Bitwuzla SMT Solver
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point …
BitwuzlaThe 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.
Colibri SMT Solver
Colibri is an SMT solver.
Colibricvc5 Theorem Prover
cvc5 is an automatic theorem prover for SMT problems.
cvc5Yices 2 SMT Solver
Yices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas …
Yices 2Q3B SMT Solver
[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which uses BDDs.
Q3BMiniSat SAT Solver
[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and …
MiniSatBoolector SMT Solver
[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …
BoolectorMathSAT SMT Solver
[ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and developers …
MathSATSMTInterpol Interpolating SMT Solver
SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and Bindings This tool is …
SMTInterpolParaFROST SMT Solver
ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in …
ParaFROSTveriT SMT Solver
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal …
veriTZ3 Theorem Prover
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This tool is available …
Z3cvc4 Theorem Prover
[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5
cvc4Lingeling SMT Solver
Lingeling is a SAT solver.
LingelingSTP Simple Theorem Prover
STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available through the following …
STPGlucose SAT Solver
Glucose is a SAT solver.
GlucoseRiss SAT Tool Collection
[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection.
RissCryptoMiniSat SAT Solver
CryptoMiniSat is a SAT solver. APIs and Bindings This tool is available through the following interfaces: C++ Namespace: …
CryptoMiniSatdReal SMT Solver
[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems that can be encoded as …
dRealSMT-RAT SMT Toolbox
SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the following interfaces: C++ API: …
SMT-RAT