z3prover/z3Hochleistungs-SMT-Löser für automatisiertes Theorembeweisen, Constraint-Lösen und Programmverifikation. Unterstützt mehrere Theorien und Sprachbindungen für formale Analysen.
Z3 ist ein Theorembeweiser von Microsoft Research. Er ist unter der MIT-Lizenz lizenziert. Windows-Binärdistributionen enthalten C++-Runtime-Redistributables
Wenn Sie mit Z3 nicht vertraut sind, können Sie hier beginnen.
Vorgefertigte Binärdateien für stabile und nächtliche Releases sind hier verfügbar.
Z3 kann mit [CMake][3], [vcpkg][4] oder [Bazel][5] gebaut werden. Es bietet [Bindings für mehrere Programmiersprachen][6].
Siehe die Release Notes für Hinweise zu verschiedenen stabilen Releases von 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 |
|---|---|
 |  |
