Z3 是来自 Microsoft Research 的定理证明器。 它采用 MIT 许可证 授权。Windows 二进制发行版包含 C++ 运行时可再发行组件
如果你不熟悉 Z3，可以从这里开始。
稳定版和每夜构建版的预编译二进制文件可在此处获取。
Z3 可以使用 [CMake][3]、[vcpkg][4] 或 [Bazel][5] 构建。 它提供了[多种编程语言的绑定][6]。
有关 Z3 各个稳定版本的说明，请参阅发行说明。
| WASM 构建 | Windows 构建 | CI | OCaml 绑定 |
|---|---|---|---|
 |  |  |  |
| 确定性 Linter | 求解器确定性 |
|---|---|
 |  |
| Android 构建 | Pyodide Wheel (PyPI) | 每夜构建 | 交叉构建 | F* Master 构建 |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC 静态 | MSVC Clang-CL | 构建 Z3 缓存 | 内存安全 | 标记 PR 就绪 |
|---|---|---|---|---|
 |  |  |  |  |
| Clang-Tidy 警告报告 |
|---|
 |
| 文档 | 发布构建 | WASM 发布 |
|---|---|---|
 |  |  |
| 每夜验证 | Copilot 设置 | Agentics 维护 | 调度 NFV 形式化审计 |
|---|---|---|---|
 |  |  |  |
| 确定性 Linter PR 评论 | 求解器确定性 PR 评论 |
|---|---|
 |  |
| API 一致性 | 代码简化器 | 发行说明 | 工作流建议 | 学术引用 |
|---|---|---|---|---|
 |  |  |  |  |
| Issue 积压 | 内存安全报告 | SMTLIB 基准查找器 |
|---|---|---|
 |  |  |
