Prove Your Python Code Correct with the Z3 SMT Solver

What you'll build

You'll take a small Python scheduling function, mirror it as symbolic constraints in the Z3 SMT solver, and have Z3 check its invariants against every possible input — not a sample of them. Along the way Z3 will find a genuine edge-case bug, hand you the exact input that triggers it, and then, once you fix it, prove the function correct and optimal.

Prerequisites

• Python 3.9 or newer. Verified below with Python 3.13.5.
• z3-solver 5.0.0.0 (released July 17, 2026) — the official Python bindings, published by the Z3 team. Prebuilt wheels exist for Linux, macOS (Intel and Apple Silicon), and Windows, so there's nothing to compile.
• Any OS; the commands below are for macOS/Linux. On Windows, activate the venv with .venv\Scripts\activate instead.
• Comfort with Python. No prior SMT or formal-methods experience needed — the one idea you need (proof by failed counterexample search) is explained in step 4.

1. Install Z3

mkdir z3-scheduler && cd z3-scheduler
python3 -m venv .venv && source .venv/bin/activate
pip install z3-solver

The package is z3-solver, not z3 — there's an unrelated package squatting on the short name (see Troubleshooting). Confirm the install:

python -c "import z3; print(z3.get_version_string())"

5.0.0

2. Write the scheduler under test

The function schedules a maintenance job: given the current time and a job duration (both in minutes since midnight), return the earliest start time so the job runs entirely inside the 09:00–17:00 window. If it can't fit today, push it to tomorrow's window. Save this as scheduler.py:

OPEN = 540    # window opens 09:00 (minutes since midnight)
CLOSE = 1020  # window closes 17:00
DAY = 1440

def next_start(now: int, duration: int) -> int:
    """Earliest start >= now so the job fits inside [OPEN, CLOSE)."""
    if now + duration <= CLOSE:
        return now
    return DAY + OPEN  # tomorrow 09:00

It looks plausible, and it passes the obvious spot checks: next_start(600, 60) → 600, next_start(1000, 60) → 1980 (tomorrow). It also has a bug that a casual test suite would likely miss. Instead of hunting for it by staring, we'll make Z3 do it.

3. Mirror the function symbolically

Z3 can't execute your Python — it reasons about mathematical constraints. So you re-express the function's logic over symbolic integers, where If(cond, a, b) replaces if/return. For straight-line arithmetic code like this, the translation is mechanical: each if x: return a chain becomes a nested If. Start verify_scheduler.py with:

from z3 import Int, If, And, Implies, Not, ForAll, Solver, sat

from scheduler import OPEN, CLOSE, DAY

now, duration = Int("now"), Int("duration")

# Symbolic mirror of scheduler.next_start: If() instead of if/return.
result = If(now + duration <= CLOSE, now, DAY + OPEN)

now and duration aren't numbers here — they're unknowns ranging over all integers, and result is an expression tree describing what the function returns for any of them.

4. Negate the invariants and let Z3 hunt

Here's the core trick of SMT-based verification. To prove "for all valid inputs, the invariants hold," you ask the opposite question: "does there exist a valid input where an invariant fails?" If Z3's exhaustive search says unsat — no such input exists — you have a proof. If it says sat, the model it returns is a concrete counterexample. Append this to verify_scheduler.py:

# Preconditions: a time today, and a job that can fit in one window.
pre = And(0 <= now, now < DAY, 1 <= duration, duration <= CLOSE - OPEN)

# Invariants that must hold for EVERY input satisfying the preconditions.
start_of_day = result % DAY
invariants = And(
    result >= now,                     # never schedule in the past
    start_of_day >= OPEN,              # starts after the window opens
    start_of_day + duration <= CLOSE,  # finishes before it closes
)

s = Solver()
s.add(pre, Not(invariants))  # look for an input that breaks an invariant

if s.check() == sat:
    m = s.model()
    print(f"BUG: now={m[now]}, duration={m[duration]} ->",
          f"start={m.eval(result)}")
else:
    print("PROVED: invariants hold for all inputs")

The preconditions matter: without them Z3 would "refute" your function with nonsense like negative durations. result % DAY normalizes tomorrow's slot back to a time of day so the window checks apply to both days. Run it:

python verify_scheduler.py

BUG: now=0, duration=480 -> start=0

Z3 found it instantly (your exact model may differ — any counterexample is fair game). At midnight with an 8-hour job, now + duration <= CLOSE holds (480 ≤ 1020), so the function returns now — scheduling the job at 00:00, hours before the window opens. The first branch never checks that now is inside the window.

5. Fix the bug and get a real proof

Clamp early times to the window's opening. In scheduler.py:

def next_start(now: int, duration: int) -> int:
    """Earliest start >= now so the job fits inside [OPEN, CLOSE)."""
    if now < OPEN:
        return OPEN
    if now + duration <= CLOSE:
        return now
    return DAY + OPEN  # tomorrow 09:00

And update the mirror in verify_scheduler.py to match:

result = If(now < OPEN, OPEN,
         If(now + duration <= CLOSE, now, DAY + OPEN))

Run it again and Z3 reports PROVED: invariants hold for all inputs. Let that sink in: this isn't 100% branch coverage or a million fuzz cases. unsat means Z3 deductively ruled out a violating input across the entire integer space — every minute of the day times every legal duration, with zero exceptions.

6. Prove it's optimal, not just safe

Safety invariants can be satisfied by a lazy scheduler that always says "tomorrow." The spec says earliest start, so let's prove no valid slot exists between now and the returned time. This needs an explicit universal quantifier, ForAll. Append:

# Optimality: no valid start exists between `now` and `result`.
t = Int("t")
fits_today = And(t >= OPEN, t + duration <= CLOSE)
earliest = ForAll(t, Implies(And(now <= t, t < result), Not(fits_today)))

s2 = Solver()
s2.add(pre, Not(earliest))
if s2.check() == sat:
    print("NOT EARLIEST:", s2.model())
else:
    print("PROVED: result is always the earliest valid start")

The claim reads: for every instant t the scheduler skipped over, t wouldn't have worked. Quantified integer formulas aren't decidable in general, but linear ones like this are — Z3 dispatches it in milliseconds.

Verify it works

A full run of the finished script:

python verify_scheduler.py

PROVED: invariants hold for all inputs
PROVED: result is always the earliest valid start

To convince yourself the harness isn't vacuously passing, re-plant the bug: change the mirror back to the two-branch If from step 3 and rerun — you should get the BUG: line again. A verifier you've never seen fail is as untrustworthy as a test you've never seen fail.

Troubleshooting

ImportError: cannot import name 'Int' from 'z3' — you ran pip install z3, which installs an unrelated package (last touched years ago) that shadows the real bindings. Fix: pip uninstall z3 && pip install z3-solver. The import stays import z3.

z3.z3types.Z3Exception: Symbolic expressions cannot be cast to concrete Boolean values. — you used Python's and/or/not (or a chained comparison like 0 <= now < DAY) on symbolic expressions. Python tries to collapse them to True/False, which is meaningless for an unknown. Fix: use And(), Or(), Not(), and split chained comparisons.

z3.z3types.Z3Exception: model is not available — you called s.model() when the last s.check() didn't return sat. In this workflow that's good news (unsat = proved); only read the model inside an if s.check() == sat: branch.

s.check() returns unknown — your constraints wandered outside decidable territory, usually nonlinear integer arithmetic (multiplying two symbolic variables) or heavier quantifier nesting. Fix: restate the property linearly, bound the quantified variable to a finite range, or set s.set("timeout", 5000) to fail fast instead of hanging.

Next steps

• Swap Int for BitVec(name, 32) and re-prove — unbounded integers hide machine-width overflow, and bitvectors catch it. The Z3 guide covers bitvectors, arrays, and strings with runnable examples.
• Keep the z3py API reference open; Optimize (maximize/minimize objectives) and unsat_core() (which constraints conflict) are the next tools you'll want.
• Try CrossHair, which uses Z3 under the hood to check real Python functions against their contracts — no manual mirroring step.
• Wire verify_scheduler.py into CI. A proof that reruns on every commit is a spec that can't silently rot.