z3
« Back to VersTracker
Description:
High-performance theorem prover
Type: Formula  |  Latest Version: 4.15.4@0  |  Tracked Since: Oct 11, 2025
Links: Homepage  |  formulae.brew.sh
Category: Developer tools
Tags: theorem-prover smt verification logic research
Install: brew install z3
About:
Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over various theories. Its main value is in automated reasoning for software verification, analysis, and testing.
Key Features:
  • High-performance SMT solving
  • Supports multiple theories (bit-vectors, arrays, etc.)
  • Extensive language bindings (C++, Python, OCaml)
  • Used as a backend for many verification tools
Use Cases:
  • Formal verification of software and hardware systems
  • Symbolic execution for bug finding
  • Constraint solving in program analysis
Alternatives:
  • CVC5 – Another leading SMT solver, often competitive with Z3.
Version History
Detected Version Rev Change Commit
Oct 11, 2025 12:19pm 0 VERSION_BUMP da6afb13
Sep 15, 2025 5:47pm 0 VERSION_BUMP ec4cca15
Dec 17, 2024 5:57pm 0 VERSION_BUMP 6afcc696
Nov 23, 2024 11:52pm 0 VERSION_BUMP 87cec62a
Oct 29, 2024 12:26am 0 VERSION_BUMP 1a200890
Oct 11, 2024 1:26am 0 VERSION_BUMP 2eda2dc3
Sep 17, 2024 1:31am 0 VERSION_BUMP 054c1be8