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).

a GRId LOgic Puzzle Solver library

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

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

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.

🐍 Solving CTF challenges using Z3 and Python

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

Finding bugs in P4 compilers using translation validation.

An overlay for the OCaml Z3 binding.

A Dockerfile with a collections of ready to use open source EDA tools: Yosys, SimbiYosys (with Z3, boolector and Yices2), nextpnr-ice40, netxpnr-ecp5, nextpnr-gowin, Amaranth HDL, Silice and Verilator.