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. https://gitlab.epfl.ch/lara/stainless

Proof of thought : LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON DSL)

Coefficient-Based Reconstruction of Arithmetic — a Mixed Boolean-Arithmetic (MBA) expression simplifier for deobfuscation

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

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

Using z3's never been easier (maybe)

a GRId LOgic Puzzle Solver library

An SMT solver frontend for OCaml

SMTscope automatically analyses and visualises SMT solver execution traces.

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.

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

🐍 Solving CTF challenges using Z3 and Python

OxiZ is a high-performance Satisfiability Modulo Theories (SMT) solver written entirely in Rust. This project is part of an initiative to reimplement Z3 in Pure Rust. Pure Rust is a fundamental requirement - no C/C++ dependencies, no FFI bindings, just clean, safe Rust code.