Z3 (theorem prover)

Z3 is an open-source SMT solver from Microsoft Research — a theorem prover that checks satisfiability of logical formulas over one or more background theories (arithmetic, bit-vectors, arrays, datatypes, quantifiers). See satisfiability-modulo-theories for the problem class it solves and the SMT-LIB language it speaks.

Key facts

• Authors: Leonardo de Moura and Nikolaj Bjørner, Microsoft Research (Redmond).
• First external release: September 2007; the reference paper is Z3: An Efficient SMT Solver (TACAS 2008, LNCS 4963). A prototype won 4 first places and 7 second places in SMT-COMP’07 before public release.¹
• Implementation: C++, open source (MIT), with APIs for C, .NET, OCaml, Python (z3-solver), Rust and more. Command-line frontend accepts SMT-LIB2.
• Architecture: DPLL(T) — a modern SAT solver + congruence-closure E-graph core + satellite theory solvers, with novel model-based theory combination and incremental E-matching for quantifiers.²

Where it shows up

Z3 is deliberately a component, not an application — “best used in the context of other tools that require solving logical formulas” (the online Z3 guide). By 2008 it was already the reasoning engine inside Spec#/Boogie (program verification), Pex (unit-test generation), VCC, HAVOC, and Yogi, and it has since become the default backend for symbolic execution engines, verification tools, and constraint-solvers-as-a-service.³ It supports all main SMT-LIB2 theories and the standard’s interactive command set (assertion stack, models, proofs, unsat cores).⁴

On this host: the mcplogic MCP server wraps Z3 (alongside SAT/Prolog/Clingo engines) for first-order logic work — note that mcplogic takes Prover9-style syntax, not SMT-LIB; see satisfiability-modulo-theories §“SMT solvers vs. resolution provers” for the dialect split.

Sources

• Leonardo de Moura and Nikolaj Bjørner 2008 — Z3: An Efficient SMT Solver
• Clark Barrett, Pascal Fontaine, Cesare Tinelli 2026 — The SMT-LIB Standard: Version 2.7

Footnotes

1. Leonardo de Moura and Nikolaj Bjørner 2008 — Z3: An Efficient SMT Solver ↩

2. Leonardo de Moura and Nikolaj Bjørner 2008 — Z3: An Efficient SMT Solver ↩

3. Leonardo de Moura and Nikolaj Bjørner 2008 — Z3: An Efficient SMT Solver ↩

4. Clark Barrett, Pascal Fontaine, Cesare Tinelli 2026 — The SMT-LIB Standard: Version 2.7 ↩