Formal Methods Tools

SAT & SMT Tools

This page lists all of the SAT & SMT 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
Abella SMT Solver Theorem Prover SAT Solver GPLv3
Agda 2 Theorem Prover Specification Language MIT
Alt-Ergo SMT Solver OCamlPro-Non-Commercial
BEAGLE SMT Solver Theorem Prover SAT Solver MIT
Bitwuzla SMT Solver Theorem Prover SAT Solver MIT
SMT Solver Theorem Prover SAT Solver MIT
CaDiCaL SAT Solver MIT
Chyp Theorem Prover Apache-2.0
Colibri SMT Solver MIT
CryptoMiniSat SAT Solver MIT GPLv2
SMT Solver Theorem Prover BSD-3-Clause
cvc5 SMT Solver Theorem Prover BSD-3-Clause
SMT Solver Apache-2.0
E Theorem Prover GPLv2
Gappa SMT Solver Theorem Prover SAT Solver MIT
Glucose SAT Solver MIT
Theorem Prover Apache-2.0
Isabelle Theorem Prover BSD-2-Clause
LEAN Theorem Prover Modeling Language Apache-2.0
Lingeling SAT Solver MIT
MathSAT SMT Solver All Rights Reserved
Megalodon Theorem Prover MIT
SMT Solver Theorem Prover SAT Solver MIT
MetiTarski University of Cambridge MIT
SAT Solver MIT
OpenSMT SMT Solver GPLv3
Theorem Prover
ParaFROST SAT Solver GPLv3
Princess SMT Solver Theorem Prover SAT Solver MIT
SMT Solver Theorem Prover SAT Solver MIT
Prover9 Theorem Prover
PVS Theorem Prover GPL-2.0
Q3B
SMT Solver MIT
SAT Solver LGPLv2
Rocq Theorem Prover LGPL-2.1
Theorem Prover
SMT-RAT SMT Solver SAT Solver MIT
SMTInterpol SMT Solver GPLv3
SPASS SMT Solver Theorem Prover SAT Solver All Rights Reserved
STP Constraint Solver SMT Solver Theorem Prover MIT
Vampire Theorem Prover BSD-3-Clause
veriT SMT Solver BSD-2-Clause
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
Zipperposition Theorem Prover BSD-2-Clause
Red dot indicates tool has not been updated or maintained recently