New releaseAug 4, 2026
z3 z3-5.0.0
Solveur SMT haute performance pour la démonstration automatique de théorèmes, la résolution de contraintes et la vérification de programmes. Prend en charge plusieurs théories et des liaisons de langage pour l'analyse formelle.
Z3
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.
Build status
Pull Request & Push Workflows
| WASM Build | Windows Build | CI | Finite-Field Regressions |
|---|---|---|---|
 |  |  |  |
| Determinism Linter | Solver Determinism | Pulse Native Checker Build |
|---|---|---|
 |  |  |
Scheduled Workflows
| Android Build | Nightly Build | Cross Build | F* Master Build |
|---|---|---|---|
 |  |  |  |
| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready |
|---|---|---|---|---|
 |  |  |  |  |
| Clang-Tidy Warning Report |
|---|
 |
Manual & Release Workflows
| Documentation | Release Build | WASM Release | Pyodide Wheel (PyPI) |
|---|---|---|---|
 |  |  |  |
Specialized Workflows
| Nightly Validation | Copilot Setup | Agentics Maintenance | Dispatch NFV Formal Audit |
|---|---|---|---|
 |  |  |  |
Follow-up / Comment Workflows
| Determinism Linter PR Comment | Solver Determinism PR Comment | Pulse Checker Regressions |
|---|---|---|
 |  |  |