z3prover/z3Solveur 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 est un démonstrateur de théorèmes de Microsoft Research. Il est distribué sous la licence MIT. Les distributions binaires Windows incluent les redistribuables du runtime C++
Si vous ne connaissez pas Z3, vous pouvez commencer ici.
Des binaires précompilés pour les versions stables et nightly sont disponibles ici.
Z3 peut être compilé avec [CMake][3], [vcpkg][4] ou [Bazel][5]. Il fournit des [bindings pour plusieurs langages de programmation][6].
Consultez les notes de version pour des informations sur les différentes versions stables de Z3.
| Build WASM | Build Windows | CI | Binding OCaml |
|---|---|---|---|
 |  |  |  |
| Linter de déterminisme | Déterminisme du solveur |
|---|---|
 |  |
| Build Android | Wheel Pyodide (PyPI) | Build nightly | Build croisé | Build F* Master |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Static | MSVC Clang-CL | Cache de build Z3 | Sécurité mémoire | Marquer les PR prêtes |
|---|---|---|---|---|
 |  |  |  |  |
| Rapport d'avertissements Clang-Tidy |
|---|
 |
| Documentation | Build de release | Release WASM |
|---|---|---|
 |  |  |
| Validation nightly | Configuration Copilot | Maintenance Agentics | Dispatch d'audit formel NFV |
|---|---|---|---|
 |  |  |  |
| Commentaire PR du linter de déterminisme | Commentaire PR du déterminisme du solveur |
|---|---|
 |  |
