新发布Aug 4, 2026
z3 z3-5.0.0
高性能SMT求解器，用于自动定理证明、约束求解和程序验证。支持多种理论和语言绑定，用于形式化分析。
Z3
Z3 是微软研究院开发的一款定理证明器。它采用 MIT 许可证 进行授权。Windows 二进制发行版包含 C++ 运行时可再分发组件。
如果你不熟悉 Z3，可以从这里开始了解。
稳定版和 nightly 版本的预编译二进制文件可在此处获取。
Z3 可以使用 [Visual Studio][1]、[Makefile][2]、[CMake][3]、[vcpkg][4] 或 [Bazel][5] 构建。它还为[多种编程语言提供了绑定][6]。
有关 Z3 各个稳定版本的说明，请参阅发布说明。
构建状态
Pull Request 和 Push 工作流
| WASM 构建 | Windows 构建 | CI | OCaml 绑定 |
|---|---|---|---|
 |  |  |  |
计划性工作流
| 开放缺陷 | Android 构建 | Pyodide Wheel (PyPI) | Nightly 构建 | 交叉构建 |
|---|---|---|---|---|
 |  |  |  |  |
| MSVC 静态 | MSVC Clang-CL | 构建 Z3 缓存 | 内存安全 | 标记 PR 就绪 |
|---|---|---|---|---|
 |  |  |  |  |
手动和发布工作流
| 文档 | 发布构建 | WASM 发布 | NuGet 构建 |
|---|---|---|---|
 |  |  |  |
专门工作流
| Nightly 验证 | Copilot 设置 | Agentics 维护 |
|---|---|---|
 |  |  |
智能体工作流
| API 一致性 | 代码简化器 | 发布说明 | 工作流建议 | 学术引用 |
|---|---|---|---|---|
 |  |  |  |  |
| 问题积压 | 内存安全报告 | QF-S 基准测试 | Specbot 崩溃分析器 | SMTLIB 基准查找器 |
|---|---|---|---|---|
 |  |  |  |  |
| TPTP 基准测试 |
|---|
 |