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 [Visual Studio][1], a [Makefile][2], using [CMake][3], using [vcpkg][4], or using [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 |
|---|---|---|---|
 |  |  |  |
| Open Bugs | Android Build | Pyodide Wheel (PyPI) | Nightly Build | Cross Build |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready |
|---|---|---|---|---|
 |  |  |  |  |
| Documentation | Release Build | WASM Release | NuGet Build |
|---|---|---|---|
 |  |  |  |
| Nightly Validation | Copilot Setup | Agentics Maintenance |
|---|---|---|
 |  |  |
| API Coherence | Code Simplifier | Release Notes | Workflow Suggestion | Academic Citation |
|---|---|---|---|---|
 |  |  |  |  |
| Issue Backlog | Memory Safety Report | QF-S Benchmark | Specbot Crash Analyzer | SMTLIB Benchmark Finder |
|---|---|---|---|---|
 |  |  |  |  |
