Z3 Integration

Z3 is the workhorse behind Deppy's automatic proofs. Most simple properties — bounds checks, arithmetic invariants, boolean conditions — are discharged entirely by Z3 without any user interaction. Your Python code stays exactly as it is; Deppy reads it, translates the relevant fragments to SMT queries, and asks Z3 for a verdict. This chapter explains how that translation works and how to work with the solver effectively when automatic verification isn't enough.

How Deppy Encodes Python to Z3

Deppy walks the Python AST of your function and builds a corresponding Z3 expression tree. The mapping is mostly straightforward:

Python operations translate to their Z3 counterparts. Arithmetic operators (+, -, *, //, %) become Z3 arithmetic; comparisons (==, !=, <, >) become Z3 predicates; logical operators (and, or, not) become Z3 And, Or, Not. Control flow via if/else becomes Z3's If (ITE — If-Then-Else).

Here's a side-by-side showing a Python function and its Z3 encoding:

def clamp(x: int, lo: int, hi: int) -> int:
    if x < lo:
        return lo
    elif x > hi:
        return hi
    else:
        return x

;; Generated by Deppy
(declare-const x Int)
(declare-const lo Int)
(declare-const hi Int)
(define-fun clamp () Int
  (ite (< x lo) lo
    (ite (> x hi) hi x)))

Automatic SMT Queries for Simple Properties

When you annotate a function with @guarantee, Deppy parses the guarantee string, converts it to a Z3 formula, and checks whether the function body implies the guarantee for all valid inputs. The generated query has the shape:

# Conceptual form of the Z3 query:
ForAll([inputs],
    Implies(preconditions, postcondition)
)

If Z3 reports unsat for the negation of this formula, the guarantee holds. If Z3 reports sat, there exists a counterexample and verification fails. Let's trace the full pipeline on a concrete function:

def abs_value(x: int) -> int:
    """Return the absolute value of x."""
    if x >= 0:
        return x
    else:
        return -x

Deppy reads the guarantee "result >= 0" from a sidecar proof file (or from inline annotation) and produces:

The generated SMT-LIB output (logged when DEPPY_Z3_DEBUG=1 or surfaced by the foundations_z3_* counters in <file>.json) looks like:

;; abs_value: guarantee result >= 0
(declare-const x Int)
(define-fun result () Int
  (ite (>= x 0) x (- x)))
(assert (< result 0))
(check-sat)
;; => unsat

When Z3 Succeeds vs When You Need Manual Proofs

Z3 is a decision procedure for several theories. It excels at some things and struggles with others. Knowing the boundary saves time:

For example, Z3 proves commutativity of addition instantly:

# Z3 proves this automatically — no user guidance needed
def add(x: int, y: int) -> int:
    return x + y

# Sidecar proof file (add_proof.py):
# guarantee: add(x, y) == add(y, x)
# Z3 result: unsat in 0.002s ✅

But Z3 cannot prove the Gauss summation formula without help, because it requires induction over n:

# Z3 times out on this — needs an inductive lemma
def triangle(n: int) -> int:
    if n <= 0:
        return 0
    return n + triangle(n - 1)

# guarantee: triangle(n) == n * (n + 1) // 2
# Z3 result: timeout ⏱️ — needs induction (see Lemmas chapter)

Controlling Z3 Timeout and Strategies

By default, Deppy gives Z3 five seconds per query. You can change this globally via deppy.config.DeppyConfig, or per-function with the @z3_config sidecar decorator:

from deppy.config import DeppyConfig

# Global Z3 settings (passed to the safety pipeline)
config = DeppyConfig(
    z3_timeout=10000,        # ms (10 seconds)
    z3_rlimit=10_000_000,    # deterministic resource budget
)

Per-function configuration lives in the sidecar proof file:

# my_module_proof.py — sidecar proof for my_module.py
from deppy.sidecar import proof_for, z3_config

@proof_for("heavy_computation")
@z3_config(timeout=30000)
def prove_heavy_computation():
    """Give Z3 thirty seconds for this complex function."""
    pass  # auto-generated query, just increase timeout

@proof_for("bitwise_hash")
@z3_config(
    timeout=15000,
    tactics=["simplify", "solve-eqs", "bit-blast"]
)
def prove_bitwise_hash():
    """Use bit-blasting for bitvector-heavy proofs."""
    pass

The tactics parameter tells Z3 which proof strategies to apply. Common tactics include:

Quantifier Patterns and Triggers

When a verification condition involves universal quantifiers (e.g., "for all elements in the list, …"), Z3 needs patterns (also called triggers) to know when to instantiate the quantifier. Deppy auto-generates patterns from the function structure, but sometimes Z3 needs a nudge.

# Original Python — no modification
def all_positive(lst: list[int]) -> bool:
    for x in lst:
        if x <= 0:
            return False
    return True

The sidecar proof can provide a quantifier hint to help Z3:

# all_positive_proof.py — sidecar
from deppy.sidecar import proof_for, z3_hint

@proof_for("all_positive")
@z3_hint(
    pattern="lst[i]",
    # Tell Z3: instantiate the quantifier whenever you see lst[i]
)
def prove_all_positive():
    """
    guarantee: result == True implies
               forall i: 0 <= i < len(lst) implies lst[i] > 0
    """
    pass

Without the pattern hint, Z3 might time out on this property because it doesn't know when to instantiate the forall i. With the hint, Z3 knows to try lst[i] for every array access and the proof goes through in under a second.

Array Bounds Checking Example

One of the most common verification tasks is proving that array accesses are within bounds. Here's a full worked example — a binary search implementation that Deppy verifies is safe:

# binary_search.py — ordinary Python, no annotations
def binary_search(arr: list[int], target: int) -> int:
    """Return index of target in sorted arr, or -1 if absent."""
    lo = 0
    hi = len(arr) - 1

    while lo <= hi:
        mid = lo + (hi - lo) // 2

        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            lo = mid + 1
        else:
            hi = mid - 1

    return -1

The sidecar proof proves three properties: bounds safety, correctness of the found index, and the meaning of a -1 return:

# binary_search_proof.py — sidecar
from deppy.sidecar import proof_for, guarantee, loop_invariant

@proof_for("binary_search")
@guarantee("result == -1 or (0 <= result < len(arr) and arr[result] == target)")
@loop_invariant(
    loop=0,
    invariant="0 <= lo and hi < len(arr)"
)
def prove_binary_search():
    """
    Z3 proves the loop invariant holds at entry and is preserved
    by each branch. From the invariant, mid is always in bounds.
    """
    pass

Deppy generates the following verification conditions for Z3:

Debugging Z3 Failures

When Z3 can't prove a property, Deppy offers several tools to understand why.

Viewing the Generated SMT-LIB

# Inspect the SMT-LIB that ``deppy.z3_bridge`` would build
# for a single foundation/identity:
$ python -c "
from deppy.z3_bridge import z3_prove_real_identity
import z3
z3.set_param('verbose', 1)
z3_prove_real_identity(lambda R: [R('lo') <= R('hi')])
"

# A typical query Deppy would emit for a clamp postcondition:
(declare-const x Int)
(declare-const lo Int)
(declare-const hi Int)
(assert (<= lo hi))
(define-fun result () Int
  (ite (< x lo) lo (ite (> x hi) hi x)))
(assert (not (and (<= lo result) (<= result hi))))
(check-sat)

Getting Counterexamples

# When the sidecar pipeline runs counterexample search against an
# admitted foundation, hits are recorded in the JSON sidecar:
$ python -m deppy.pipeline.run_verify buggy_module.deppy --out buggy.lean
$ jq '.section_counters | {counterexamples_attempted, counterexamples_found}' \
     buggy.json
{
  "counterexamples_attempted": 3,
  "counterexamples_found": 1
}

# When at least one counterexample is found, ``certified``
# flips to false and ``failures`` lists the offending foundation:
$ jq '{certified, failures}' buggy.json
{
  "certified": false,
  "failures": ["1 counterexample(s) found for admitted foundations"]
}

Adding Intermediate Assertions

If Z3 times out, it often helps to break the proof into smaller steps. You can add intermediate assert_lemma calls in the sidecar:

# complex_proof.py — sidecar
from deppy.sidecar import proof_for, guarantee, assert_lemma

@proof_for("complex_function")
@guarantee("result > 0")
def prove_complex():
    # Break into two sub-goals that Z3 can handle individually
    assert_lemma("intermediate >= 1", at_line=12)
    assert_lemma("intermediate * factor > 0", at_line=15)