The Yices SMT Solver

• UpdatedApr 26, 2025
• SMT

Rust bindings for the Z3 solver.

• UpdatedDec 9, 2024
• Rust

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

• UpdatedApr 27, 2025
• C

Code and exercises for a workshop on z3 and angr

• UpdatedDec 29, 2020
• Python

A fuzzing framework for SMT solvers

• UpdatedJul 27, 2023
• Python

Automated Reasoning in Nonlinear Theories of Reals

• UpdatedJun 8, 2024
• SMT

Jupyter notebooks for tutorial on the Z3 SMT solver

• UpdatedNov 3, 2023
• Jupyter Notebook

My sandbox for experimenting with solver algorithms.

• UpdatedApr 28, 2025
• Haskell

Go (golang) bindings to the Z3 SMT Solver

• UpdatedJul 16, 2022
• Go

A modular sat/smt solver with proof output.

• UpdatedJan 8, 2024
• OCaml

Agda bindings to SMT-LIB2 compatible solvers.

• UpdatedOct 7, 2024
• Agda

The Eldarica model checker

• UpdatedApr 24, 2025
• Scala

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.

• UpdatedAug 17, 2019

KeY Theorem Prover for Deductive Java Verification

• UpdatedApr 25, 2025
• Java

• UpdatedMar 26, 2016
• C++

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

• UpdatedJan 8, 2017
• C++

An SMT Solver for string constraints

• UpdatedMar 17, 2025
• Scala

gradient-based symbolic execution engine implemented from scratch

• UpdatedDec 16, 2023
• C++

Kotlin/Java API for various SMT solvers

• UpdatedMar 23, 2025
• Kotlin

SMT solver for the theory of floating-point arithmetic

• UpdatedJan 30, 2018
• C++