The Yices SMT Solver

Rust bindings for the Z3 solver.

The efficient SMT-based context-bounded model checker (ESBMC)

Code and exercises for a workshop on z3 and angr

A fuzzing framework for SMT solvers

My sandbox for experimenting with solver algorithms.

Jupyter notebooks for tutorial on the Z3 SMT solver

Automated Reasoning in Nonlinear Theories of Reals

Go (golang) bindings to the Z3 SMT Solver

A modular sat/smt solver with proof output.

Agda bindings to SMT-LIB2 compatible solvers.

The Eldarica model checker

Counter-example guided inductive synthesis (CEGIS) implementation for the SMT solver Z3 by Microsoft Research

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.

KeY Theorem Prover for Deductive Java Verification

gradient-based symbolic execution engine implemented from scratch

An SMT Solver for string constraints

Kotlin/Java API for various SMT solvers

SMT solver for the theory of floating-point arithmetic