SMT

Bitwuzla
SMT Solver

Bitwuzla is an award-winning Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations.

View on GitHub

Boolector
SMT Solver

Boolector is an award-winning Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations.

View on GitHub

cvc5
SMT Solver

cvc5 is an award-winning automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. cvc5 is the successor of CVC4.

View on GitHub

ddsmt
Delta Debugger for SMT-LIB

ddSMT is a delta debugger for input in the SMT-LIB language and its dialects and extensions. It serves as an input minimizer for SMT-LIB(-like) input that triggers interesting behavior for a given command.

View on GitHub

Murxla
An API Fuzzer for SMT Solvers

Murxla is a solver-agnostic fuzzer for SMT Solvers that randomly generates valid sequences of solver API calls based on a customizable API model, with full support for semantics and features of SMT-LIB.

View on GitHub

Smt-Switch
A Solver-Agnostic C++ API for SMT Solving

Smt-Switch provides abstract C++ classes which can be implemented by different SMT solvers. Our model checker Pono is built using Smt-Switch.

View on GitHub

Model Checking

Pono
SMT-Based Model Checker

Pono is a flexible and extensible SMT-based model checker that leverages word-level reasoning. 'Pono' is the Hawaiian word for proper, correct, or goodness.

Pono is the successor of our model checkers CoSA and CoSA2.

View on GitHub

Neural Network Verification

Marabou
SMT-Based Framework for Verifying Deep Neural Networks

Marabou is an SMT-based tool that can answer queries about the properties of a neural network by transforming these queries into constraint satisfaction problems.

View on GitHub

Theorem Proving

Pantograph
A Machine-to-Machine Interaction Interface for Lean 4

Pantograph provides interfaces to implement efficient proof search in Lean 4 and is tailored towards machine learning agents.

View on GitHub

Deprecated Tools

Cosa
CoreIR Symbolic Analyzer

CoSA is an SMT-based symbolic model checker for hardware designs. It is succeeded by Pono.

View on GitHub

Cosa2
CoreIR Symbolic Analyzer

CoSA2 is an SMT-based symbolic model checker for hardware designs. It is succeeded by Pono.

View on GitHub

CVC4
SMT Solver

CVC4 is an award-winning automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It is succeeded by cvc5.

View on GitHub