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. É licenciado sob a licença MIT. As distribuições binárias para Windows incluem redistribuíveis de runtime C++
Se você não está familiarizado com o Z3, você pode começar aqui.
Binários pré-compilados para versões estáveis e nightly estão disponíveis aqui.
O Z3 pode ser compilado usando [CMake][3], [vcpkg][4] ou [Bazel][5]. Ele fornece [bindings para várias linguagens de programação][6].
Consulte as notas de versão para notas sobre as várias versões estáveis do Z3.
| Build WASM | Build Windows | CI | Binding OCaml |
|---|---|---|---|
 |  |  |  |
| Linter de Determinismo | Determinismo do Solver |
|---|---|
 |  |
| Build Android | Wheel Pyodide (PyPI) | Build Nightly | Build Cruzado | Build F* Master |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Segurança de Memória | Marcar PRs como Prontos |
|---|---|---|---|---|
 |  |  |  |  |
| Relatório de Avisos do Clang-Tidy |
|---|
 |
| Documentação | Build de Release | Release WASM |
|---|---|---|
 |  |  |
| Validação Nightly | Configuração do Copilot | Manutenção Agentics | Dispatch NFV Formal Audit |
|---|---|---|---|
 |  |  |  |
| Comentário de PR do Linter de Determinismo | Comentário de PR do Determinismo do Solver |
|---|---|
 |  |
