Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Windows binary distributions include C++ runtime redistributables

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available here.

Z3 can be built using [CMake][3], [vcpkg][4], or [Bazel][5]. It provides [bindings for several programming languages][6].

See the release notes for notes on various stable releases of Z3.

Build status

Pull Request & Push Workflows

WASM Build	Windows Build	CI	Finite-Field Regressions

Determinism Linter	Solver Determinism	Pulse Native Checker Build

Scheduled Workflows

Android Build	Nightly Build	Cross Build	F* Master Build

MSVC Static	MSVC Clang-CL	Build Z3 Cache	Memory Safety	Mark PRs Ready

Clang-Tidy Warning Report

Manual & Release Workflows

Documentation	Release Build	WASM Release	Pyodide Wheel (PyPI)

Specialized Workflows

Nightly Validation	Copilot Setup	Agentics Maintenance	Dispatch NFV Formal Audit

Follow-up / Comment Workflows

Determinism Linter PR Comment	Solver Determinism PR Comment	Pulse Checker Regressions