Symbolic execution tool

Verification system for effectful programs

Triton is a Dynamic Binary Analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a dynamic taint engine, AST representations of the x86, x86-64, ARM32 and AArch64 Instructions Set Architecture (ISA), SMT simplification passes, an SMT solver interface and, the last but not least, Python bindings.

Liquid Types For Haskell

pySMT: A library for SMT formulae manipulation and solving

Simple Theorem Prover, an efficient SMT solver for bitvectors

SMACK Software Verifier and Verification Toolchain

Verification framework and tool for higher-order Scala programs

Automatic verification of LLVM optimizations

APALACHE: symbolic model checker for TLA+

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.

JavaSMT - Unified Java API for SMT solvers.

Rust bindings for the Z3 solver.

Automatic program repair and patch generation system for Java based on dynamic analysis and code synthesis with SMT, developed at University of Lille and Inria, France.

MonoSAT - An SMT solver for Monotonic Theories

Synthesis of Heap-Manipulating Programs from Separation Logic

TouIST, the IDE & Language for Logic (backed by SAT, SMT and QBF solvers)

Formally prove properties of Haskell programs using SBV/SMT.

Haskell bindings to Microsoft's Z3 API (unofficial).

This plugin allows you to configure email notifications for build results

A simple SMT solver.

A VIM plugin that adds support for the SMT-LIB2 format (including Z3's extensions)

prototyping logic programming in Scala

CLP(SMT) on top of miniKanren

This a type-checker plugin to rule all type checker plugins involving type-equality reasoning using smt solvers.

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

SMT solver for the theory of floating-point arithmetic

Targoman SMT framework source code

[research] A modular SMT solver in OCaml, based on mcSAT