Z3Prover/z3

Z3 是 Microsoft Research 开源的 SMT 求解器，适合需要判断一组逻辑约束能否同时成立（可满足性），或间接证明某性质成立的场景。它更贴近程序分析、语言工具和形式化验证，而不是日常写代码。

它做什么、怎么用

Z3 接受约束并给出结论：可满足并附带一组赋值，或不可满足，由此支撑性质证明。默认输入格式是 SMTLIB2，项目文档还列出 C、C++、.NET、Java、Python、OCaml 和 Rust 的原生 API，以及 Julia 和 Smalltalk 的社区绑定。多数人可能从语言封装开始：Python API 在 PyPI 上以 z3-solver 发布，WebAssembly/TypeScript 构建发布在 npm 上。官网另有在线指南可供入门。

一个具体工作流来自早期使用者的描述：在带契约或细化类型的语言原型中，把断言压入求解器栈，之后可以撤销，因此每检查一个函数不必重启求解器并重新声明所有变量 一份 SMT 使用报告。这种栈机制影响它如何嵌入编译器和分析器，但这是 2015 年用户的自述，不是当前性能基准。

获取方式

README 指向稳定版和每日构建的预编译二进制，也可用 CMake、vcpkg 或 Bazel 从源码构建 项目 README。CMake 被描述为首选且功能最完整的构建路径；Z3 使用 C++20，Windows 上推荐 Visual Studio 2019 或更高版本。构建依赖不多：C++ 运行时库（含 pthreads），构建时需要 Python，而 Java、.NET、OCaml 和 Julia API 各自需要对应工具链。Go 绑定需要 CGO 和 Go 1.20 或更高版本。GMP 是可选的，因为 Z3 自带多精度实现。

如果只是想试用或嵌入求解器，绑定和预编译二进制可以绕开大部分上述要求；编译器和构建系统的要求属于从源码构建这条路径。在线指南是学习概念的平缓入口 Z3 指南。

许可与贡献条件

Z3 采用 MIT 许可，这对以前需要权衡能否链接 Z3 的项目很重要 MIT 许可证。Windows 二进制发行版包含按 Microsoft 条款授权的 C++ 运行时再发行组件 C++ 运行时条款。

当前维护策略针对 fuzz 报告：只提供复现、没有进一步分析的提交可能不经考虑就被关闭，因为处理 fuzz 缺陷会挤占用户更关心的工作。这会影响提交什么类型的缺陷报告才有价值。

现有材料没有基准测试结果或求解器性能评估，因此应依据接口和构建要求来选择，而不是预期速度。仓库的 GitHub 热度数据不能作为可靠性证据。