z3prover/z3High-performance SMT solver for automated theorem proving, constraint solving, and program verification. Supports multiple theories and language bindings for formal analysis.
Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Windows binary distributions include C++ runtime redistributables
If you are not familiar with Z3, you can start here.
Pre-built binaries for stable and nightly releases are available here.
Z3 can be built using [CMake][3], [vcpkg][4], or [Bazel][5]. It provides [bindings for several programming languages][6].
See the release notes for notes on various stable releases of Z3.
| WASM Build | Windows Build | CI | OCaml Binding |
|---|---|---|---|
 |  |  |  |
| Determinism Linter | Solver Determinism |
|---|---|
 |  |
| Android Build | Pyodide Wheel (PyPI) | Nightly Build | Cross Build | F* Master Build |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready |
|---|---|---|---|---|
 |  |  |  |  |
| Clang-Tidy Warning Report |
|---|
 |
| Documentation | Release Build | WASM Release |
|---|---|---|
 |  |  |
| Nightly Validation | Copilot Setup | Agentics Maintenance | Dispatch NFV Formal Audit |
|---|---|---|---|
 |  |  |  |
| Determinism Linter PR Comment | Solver Determinism PR Comment |
|---|---|
 |  |
| API Coherence | Code Simplifier | Release Notes | Workflow Suggestion | Academic Citation |
|---|---|---|---|---|
 |  |  |  |  |
