z3prover/z3Высокопроизводительный SMT-решатель для автоматического доказательства теорем, решения ограничений и верификации программ. Поддерживает множество теорий и привязки к языкам для формального анализа.
Z3 — это средство доказательства теорем от Microsoft Research. Он распространяется под лицензией MIT. Бинарные дистрибутивы для Windows включают распространяемые пакеты среды выполнения C++
Если вы не знакомы с Z3, вы можете начать здесь.
Готовые бинарные сборки для стабильных и ночных релизов доступны здесь.
Z3 можно собрать с помощью [CMake][3], [vcpkg][4] или [Bazel][5]. Он предоставляет [привязки для нескольких языков программирования][6].
См. примечания к выпуску с информацией о различных стабильных релизах Z3.
| Сборка WASM | Сборка Windows | CI | Привязка OCaml |
|---|---|---|---|
 |  |  |  |
| Линтер детерминизма | Детерминизм решателя |
|---|---|
 |  |
| Сборка Android | Колесо Pyodide (PyPI) | Ночная сборка | Кросс-сборка | Сборка F* Master |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Static | MSVC Clang-CL | Кэш сборки Z3 | Безопасность памяти | Отметка PR как готовых |
|---|---|---|---|---|
 |  |  |  |  |
| Отчёт о предупреждениях Clang-Tidy |
|---|
 |
| Документация | Сборка релиза | Релиз WASM |
|---|---|---|
 |  |  |
| Ночная валидация | Настройка Copilot | Обслуживание Agentics | Запуск формального аудита NFV |
|---|---|---|---|
 |  |  |  |
| Комментарий PR линтера детерминизма | Комментарий PR детерминизма решателя |
|---|---|
 |  |
