z3prover/z3Высокопроизводительный SMT-решатель для автоматического доказательства теорем, решения ограничений и верификации программ. Поддерживает множество теорий и привязки к языкам для формального анализа.
Z3 — это средство доказательства теорем от Microsoft Research. Оно лицензировано под лицензией MIT. Двоичные дистрибутивы для Windows включают перенаправляемые компоненты среды выполнения C++.
Если вы не знакомы с Z3, можете начать здесь.
Предварительно собранные двоичные файлы для стабильных и ночных сборок доступны здесь.
Z3 может быть собран с помощью [Visual Studio][1], [Makefile][2], [CMake][3], [vcpkg][4] или [Bazel][5]. Он предоставляет [привязки для нескольких языков программирования][6].
Смотрите примечания к выпуску для получения информации о различных стабильных версиях 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 |
|---|---|---|---|---|
 |  |  |  |  |
