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
Automated Schedule Generation for Time-Sensitive Networks (TSN).
Code and exercises for a workshop on z3 and angr
Proof of thought : LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON DSL)
Jupyter notebooks for tutorial on the Z3 SMT solver
Constraint solver based on coverage-guided fuzzing
An SMT solver frontend for OCaml
Coefficient-Based Reconstruction of Arithmetic — a Mixed Boolean-Arithmetic (MBA) expression simplifier for deobfuscation
FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.
Deterministic policy language for AI agents. Z3 + TLA+ dual-engine formal verification. Runtime enforcement <1ms.
A toy code generator (i.e. "program synthesis") using the Z3 solver
A Formal Method playground for limboole, Z3, nuXmv, Alloy, Spectra, Dafny, and more...
Scripts and Javascript Glue code to use Z3 in the browser using WASM
To associate your repository with the z3 topic, visit your repo's landing page and select "manage topics."