New releaseAug 4, 2026
z3 z3-5.0.0
自動定理証明、制約解決、プログラム検証のための高性能SMTソルバー。形式的解析のための複数の理論と言語バインディングをサポート。
Z3
Z3 は Microsoft Research による定理証明器です。 MIT ライセンスの下でライセンスされています。Windows 用バイナリ配布物には C++ ランタイム再頒布可能パッケージが含まれています。
Z3 に馴染みがない場合は、こちらから始めることができます。
安定版およびナイトリリースのビルド済みバイナリはこちらで入手できます。
Z3 は [CMake][3]、[vcpkg][4]、または [Bazel][5] を使用してビルドできます。 [複数のプログラミング言語向けのバインディング][6]を提供しています。
Z3 の各種安定版リリースに関する注意事項については、リリースノートを参照してください。
ビルドステータス
プルリクエストおよびプッシュのワークフロー
| WASM ビルド | Windows ビルド | CI | 有限体リグレッション |
|---|---|---|---|
 |  |  |  |
| 決定性リンター | ソルバーの決定性 | Pulse ネイティブチェッカーのビルド |
|---|---|---|
 |  |  |
スケジュールされたワークフロー
| Android ビルド | ナイトリービルド | クロスビルド | F* マスタービルド |
|---|---|---|---|
 |  |  |  |
| MSVC Static | MSVC Clang-CL | Build Z3 Cache | Memory Safety | Mark PRs Ready |
|---|---|---|---|---|
 |  |  |  |  |
| Clang-Tidy Warning Report |
|---|
 |
手動およびリリースワークフロー
| Documentation | Release Build | WASM Release | Pyodide Wheel (PyPI) |
|---|---|---|---|
 |  |  |  |
特化ワークフロー
| Nightly Validation | Copilot Setup | Agentics Maintenance | Dispatch NFV Formal Audit |
|---|---|---|---|
 |  |  |  |
フォローアップ / コメントワークフロー
| Determinism Linter PR Comment | Solver Determinism PR Comment | Pulse Checker Regressions |
|---|---|---|
 |  |  |