z3

{
  "aliases": [],
  "alternatives": [
    "CVC5",
    "Yices",
    "SMT2",
    "Alt-Ergo"
  ],
  "build_dependencies": [
    "cmake",
    "python@3.14"
  ],
  "categories": [
    "solver",
    "library",
    "binding"
  ],
  "caveats": null,
  "conflicts_with": [],
  "dependencies": [],
  "deprecated": 0,
  "deprecation_reason": null,
  "desc": "High-performance theorem prover",
  "disable_reason": null,
  "disabled": 0,
  "enrichment_fetched_at": "2026-06-20T23:40:39+00:00",
  "first_seen": "2026-06-20T23:34:18+00:00",
  "full_name": "z3",
  "github_default_branch": "master",
  "github_last_commit_at": "2026-06-20T21:48:32Z",
  "github_readme_excerpt": "# Z3\n\nZ3 is a theorem prover from Microsoft Research. \nIt is licensed under the [MIT license](LICENSE.txt). Windows binary distributions include [C++ runtime redistributables](https://visualstudio.microsoft.com/license-terms/vs2022-cruntime/)\n\nIf you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background).\n\nPre-built binaries for stable and nightly releases are available [here](https://github.com/Z3Prover/z3/releases).\n\nZ3 can be built using [Visual Studio][1], a [Makefile][2], using [CMake][3],\nusing [vcpkg][4], or using [Bazel][5].\nIt provides [bindings for several programming languages][6].\n\nSee the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3.\n\n[![Try the online Z3 Guide](z3guide.jpeg)](https://microsoft.github.io/z3guide/)\n\n## Build status\n\n### Pull Request \u0026 Push Workflows\n| WASM Build | Windows Build | CI | OCaml Binding |\n| ------------|---------------|----|-----------| \n| [![WASM Build](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [![Windows](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [![CI](https://github.com/Z3Prover/z3/actions/workflows/ci.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/ci.yml) | [![OCaml Binding CI](https://github.com/Z3Prover/z3/actions/workflows/ocaml.yaml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/ocaml.yaml) |\n\n### Scheduled Workflows\n| Open Bugs | Android Build | Pyodide Build | Nightly Build | Cross Build |\n| -----------|---------------|---------------|---------------|-------------|\n| [![Open Issues](https://github.com/Z3Prover/z3/actions/workflows/wip.yml/badge.svg)](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) | [![Android Build](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml/badge.svg)](https://github.com/Z3Prover/",
  "github_repo": "Z3Prover/z3",
  "github_stars": 12378,
  "github_topics": [],
  "homepage": "https://github.com/Z3Prover/z3",
  "homepage_og_description": null,
  "homepage_og_image": null,
  "homepage_title": null,
  "installs_30d": 59523,
  "installs_365d": 564420,
  "installs_90d": 142140,
  "keg_only": 0,
  "keg_only_reason": null,
  "last_seen": "2026-06-20T23:34:18+00:00",
  "license": "MIT",
  "llm_generated_at": "2026-06-20T23:42:45+00:00",
  "llm_model": "claude-haiku-4-5",
  "name": "z3",
  "oldnames": [],
  "one_liner": "High-performance theorem prover and SMT solver from Microsoft Research for constraint satisfaction and formal verification.",
  "optional_dependencies": [],
  "rank_30d": 105,
  "rank_365d": 129,
  "rank_90d": 148,
  "raw_hash": "f85dd32cbe2396c7",
  "recommended_dependencies": [],
  "revision": 0,
  "ruby_source_path": "Formula/z/z3.rb",
  "tap": "homebrew/core",
  "test_dependencies": [
    "python@3.14"
  ],
  "uses_from_macos": [],
  "version_head": "HEAD",
  "version_stable": "4.16.0",
  "versioned_formulae": [],
  "why_use_this": "Z3 is essential for formal methods workflows, program verification, and constraint-solving problems. It\u0027s widely used as a backend in static analyzers, fuzzing frameworks, and model checkers. Provides language bindings (Python, C, C++, OCaml, Java) making it a library dependency for verification tools, not primarily a CLI tool."
}