Definition
Plain language
Microsoft's widely used satisfiability and theorem-prover.
As stated in the literature
Microsoft Research's SMT solver, widely used for constraint solving in program analysis and verification.
Why it matters: It is a workhorse behind program verifiers, symbolic execution tools, and many AI-plus-formal-methods pipelines.
For example, Z3 can be given a set of integer constraints and quickly return either a satisfying assignment or a proof that none exists.
Heard on the show
“… They take a sub-one-billion model, hook the auxiliary up to Z3 — the standard satisfiability solver, the kind of program that takes a stack of logical constraints …”Episode 040 — Two Frozen Models Learn to Whisper: Coupling Through Hidden States