z3

Symbolic execution tool

An analysis tool for Python that blurs the line between testing and type systems.

Verification framework and tool for higher-order Scala programs

Constraint solver based on coverage-guided fuzzing

Code and exercises for a workshop on z3 and angr

Small tool for generating ropchains using unicorn and z3

A fuzzing framework for SMT solvers

Jupyter notebooks for tutorial on the Z3 SMT solver

Using z3's never been easier (maybe)

Automated Schedule Generation for Time-Sensitive Networks (TSN).

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

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

a GRId LOgic Puzzle Solver library

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

An overlay for the OCaml Z3 binding.

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

Finding bugs in P4 compilers using translation validation.

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.

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

Racket bindings for Z3