Symbolic execution tool

Verification framework and tool for higher-order Scala programs

Constraint solver based on coverage-guided fuzzing

Small tool for generating ropchains using unicorn and z3

Code and exercises for a workshop on z3 and angr

A compiler for automatically re-targeting sequential Java code to Apache Spark.

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

An overlay for the OCaml Z3 binding.

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

Racket bindings for Z3

An interactive development environment for SMT-LIB files and Z3

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

Vagrant setup for building a machine for CTF/exploit development

a GRId LOgic Puzzle Solver library

A toy code generator (i.e. "program synthesis") using the Z3 solver

A simple Prolog API for the Z3 constraint solver

Intrepyd Model Checker

Files for http://deniable.org/reversing/symbolic-execution

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.

Superoptimizer using the z3 SMT solver

Jupyter notebooks for tutorial on the Z3 SMT solver

A Kotlin library for running workers on Kafka

Z3 via emscripten

The Z3 Theorem Prover bindings for Delphi

Sudoku Solver using Z3

A bounded model checker for an IMP-style imperative language.

Finding bugs in the P4 Compiler using Translation Validation

https://regexcrossword.com/ solver using Z3py

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.