z3prover/z3Solucionador SMT de alto desempenho para prova automatizada de teoremas, resolução de restrições e verificação de programas. Suporta múltiplas teorias e bindings de linguagem para análise formal.
Z3 é um provador de teoremas da Microsoft Research. Está licenciado sob a licença MIT. Distribuições binárias para Windows incluem redistribuíveis de tempo de execução C++
Se você não está familiarizado com o Z3, pode começar aqui.
Binários pré-construídos para versões estáveis e noturnas estão disponíveis aqui.
O Z3 pode ser construído usando [Visual Studio][1], um [Makefile][2], [CMake][3], [ vcpkg][4] ou [Bazel][5]. Ele fornece [bindings para várias linguagens de programação][6].
Consulte as notas de lançamento para obter notas sobre várias versões estáveis do 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 |
|---|---|---|---|---|
 |  |  |  |  |
