Formal Methods Tools

Actively Maintained

Tool Description
Bitwuzla Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …
Colibri Colibri is an SMT solver.
CryptoMiniSat CryptoMiniSat is a SAT solver. APIs and Bindings This tool is available through the following …
cvc5 cvc5 is an automatic theorem prover for SMT problems.
Glucose Glucose is a SAT solver.
Lingeling Lingeling is a SAT solver.
MathSAT [ Closed-Source Tool ]  MiniSat is a minimalistic, open-source SAT solver, developed to help …
OpenSMT OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making …
ParaFROST ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA …
SMT-RAT SMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the …
SMTInterpol SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and …
STP STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available …
veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
Yices 2 Yices is an SMT solver developed by SRI International. It is widely used for checking the …
Z3 Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This …