Getting Started with Deppy

Deppy verifies existing Python code — you do not need to rewrite anything or learn a new language. You keep writing ordinary Python with standard type hints, add lightweight specification decorators, and Deppy checks that the code actually satisfies those specifications using Z3, cubical homotopy type theory, and optional sidecar proofs.

This chapter walks you through installation, your first verified function, and how to read the verifier's output.

Installation

Install Deppy from GitHub:

# Install directly from GitHub
pip install git+https://github.com/thehalleyyoung/deppy.git

# — or — clone and install in editable mode (for development)
git clone https://github.com/thehalleyyoung/deppy.git
cd deppy
pip install -e .

# Optional but strongly recommended — enables Z3-backed proofs
pip install z3-solver

Without z3-solver Deppy can still run in LLM-judged mode, but you will not get the strongest (Z3_VERIFIED) trust level.

Confirm the installation:

python3 -c "from deppy import guarantee, verify; print('ready')"
# ready

Your First Verified Function

Create a file called mymath.py with the following contents. This is plain Python — the only addition is the @guarantee decorator that states what the function promises to its callers.

from __future__ import annotations
from deppy import guarantee


@guarantee("result >= a and result >= b and (result == a or result == b)")
def max_of(a: int, b: int) -> int:
    """Return the larger of two integers."""
    if a >= b:
        return a
    else:
        return b

Notice that the function body is completely ordinary Python. There are no proof terms, no monadic wrappers, and no special base classes. Deppy reads the AST, extracts proof obligations from the @guarantee specification, and discharges them automatically.

Running the Verifier

Deppy ships with two ways to invoke the verifier on a Python module: a .deppy sidecar file (best for verifying libraries you don't control) or the decorator form (best when the module carries its own @verify annotations). Both feed the same kernel pipeline.

# Verify via a sidecar (mymath.deppy beside mymath.py)
python -m deppy.pipeline.run_verify mymath.deppy --out mymath.lean

# Or verify a module that carries decorators inline
python -m deppy.pipeline.run_verify --from-module mymath --out mymath.lean

You should see output like this (truncated):

  Foundations: N / N Z3-attempted / verified
  ProofTerm subclasses (C1–C7 audit batch):
    constructed / kernel-accepted:         N / N
  ``verify`` blocks (.deppy → kernel.verify):
    accepted by ProofKernel.verify:        N
  ────────────────────────────────────────────────
  deppy.lean.lean_runner round-trip:       OK
  ────────────────────────────────────────────────
  ✓ CERTIFIED — top-level certify_or_die: PASS
  ════════════════════════════════════════════════
  Certificate at: mymath.lean
  JSON sidecar:   mymath.json

Two Styles of Specification: @guarantee vs @ensures

Deppy provides two complementary ways to state postconditions, designed around the principle of gradual formality:

from deppy import guarantee

@guarantee("result is non-negative")
def square(n: int) -> int:
    return n * n

from deppy import ensures

@ensures(lambda n, result: result >= 0)
def square(n: int) -> int:
    return n * n

Similarly, preconditions have two forms:

@requires("xs is non-empty")  # NL string

@requires(lambda xs: len(xs) > 0)  # formal

@guarantee("returns the sorted, deduplicated version of xs")
@ensures(lambda xs, r: len(r) <= len(xs))
@ensures(lambda xs, r: all(r[i] < r[i+1] for i in range(len(r)-1)))
def unique_sorted(xs: list[int]) -> list[int]:
    return sorted(set(xs))

Understanding the Output

Each function annotated with @guarantee produces a verification block in the output. Here is what each piece means:

A Slightly Harder Example

Let's verify an absolute-value function. The guarantee now involves conditionals that Deppy must reason about across both branches.

from __future__ import annotations
from deppy import guarantee


@guarantee("result >= 0 and (result == x or result == -x)")
def abs_val(x: int) -> int:
    """Return the absolute value of x."""
    if x >= 0:
        return x
    else:
        return -x

Running python -m deppy.pipeline.run_verify on this file produces:

abs_val(x: int) -> int
  Proof obligations:
    1. result >= 0                       ✅  Z3_VERIFIED
    2. result == x or result == -x      ✅  Z3_VERIFIED

  Status: ✅ VERIFIED   Trust: Z3_VERIFIED   Time: 0.02s

Z3 handles both branches by case-splitting on the condition x >= 0. In each branch it checks the guarantee independently and merges the results.

When Verification Fails

What happens if the code is wrong? Suppose we make a mistake in our max_of implementation:

from __future__ import annotations
from deppy import guarantee


@guarantee("result >= a and result >= b and (result == a or result == b)")
def max_of(a: int, b: int) -> int:
    """Oops — always returns the first argument."""
    return a  # BUG: ignores b entirely

The verifier will catch this immediately:

max_of(a: int, b: int) -> int
  Proof obligations:
    1. result >= a            ✅  Z3_VERIFIED
    2. result >= b            ❌  FAILED
    3. result == a or result == b  ✅  Z3_VERIFIED

  Status: ❌ FAILED

  Counterexample (from Z3):
    a = 0, b = 1
    result = 0
    Violated: result >= b  (0 >= 1 is False)

──────────────────────────────────────────────────
 0 functions verified · 1 failed · 2/3 obligations discharged
──────────────────────────────────────────────────

The counterexample is concrete: when a = 0 and b = 1, the function returns 0, which violates result >= b. This is one of the great strengths of SMT-backed verification — when something is wrong, you get a witness, not just a vague error.

IDE Integration

Deppy works with any editor that runs Python: the only IDE contract is "show the file, run a process when you save." A typical workflow is to keep a split terminal open running python -m deppy.pipeline.run_verify my_module.deppy --out my_module.lean on every save.

The --out Lean certificate is a plain text file you can diff in source control; the JSON sidecar emitted next to it records every proof obligation, trust level, and discharge method. Together they form a reproducible audit log of what was verified.

Project Configuration

For multi-file projects, place a deppy.toml at your project root. Here is a minimal example:

# deppy.toml
[deppy]
python   = "3.12"
min_trust = "Z3_VERIFIED"     # reject LLM-only judgements
z3_timeout = 30            # seconds per obligation

[deppy.paths]
include = ["src/**/*.py"]
exclude = ["tests/**"]

A deppy.toml file is documentation today — python -m deppy.pipeline.run_verify always takes either a .deppy path or a --from-module DOTTED.PATH argument; multi-file project orchestration is typically handled with a wrapper shell script or a Makefile that enumerates the .deppy files explicitly.

What Deppy Checks (and What It Doesn't)

At this stage Deppy is checking functional correctness — does the return value satisfy the postcondition for every possible input that matches the type annotations? It does not yet check:

• Termination (covered in Chapter 6)
• Side effects or mutation (covered in Part 6)
• Concurrency safety (also Part 6)

Those topics build on the foundation laid here. For now, focus on pure functions with clear input/output contracts.

A Complete Module

Let's put several verified functions together into a small utility module to see how Deppy handles a realistic file.

from __future__ import annotations
from deppy import guarantee, assume


@guarantee("result >= 0")
def square(n: int) -> int:
    return n * n


@guarantee("result >= lo and result <= hi")
def clamp(x: int, lo: int, hi: int) -> int:
    assume("lo <= hi")
    if x < lo:
        return lo
    elif x > hi:
        return hi
    else:
        return x


@guarantee("result == a + b")
def add(a: int, b: int) -> int:
    return a + b


@guarantee("(result == True and n > 0) or (result == False and n <= 0)")
def is_positive(n: int) -> bool:
    return n > 0

Running the safety pipeline directly on utils.py (which understands @guarantee/@requires/@ensures decorators):

$ python -m deppy check utils.py

──────────────────────────────────────────────────
 Deppy v0.1 — verifying utils.py
──────────────────────────────────────────────────

square(n: int) -> int
  1. result >= 0   ✅  Z3_VERIFIED
  Status: ✅ VERIFIED   Trust: Z3_VERIFIED   Time: 0.01s

clamp(x: int, lo: int, hi: int) -> int
  Precondition: lo <= hi
  1. result >= lo   ✅  Z3_VERIFIED
  2. result <= hi   ✅  Z3_VERIFIED
  Status: ✅ VERIFIED   Trust: Z3_VERIFIED   Time: 0.02s

add(a: int, b: int) -> int
  1. result == a + b   ✅  Z3_VERIFIED
  Status: ✅ VERIFIED   Trust: Z3_VERIFIED   Time: 0.01s

is_positive(n: int) -> bool
  1. (result == True and n > 0) or
     (result == False and n <= 0)   ✅  Z3_VERIFIED
  Status: ✅ VERIFIED   Trust: Z3_VERIFIED   Time: 0.01s

──────────────────────────────────────────────────
 4 functions verified · 0 failed · 5 obligations discharged
──────────────────────────────────────────────────

Note how clamp uses assume("lo <= hi") to declare a precondition. Deppy adds this as an axiom when proving the postcondition, and separately generates a proof obligation at every call site of clamp to ensure the precondition actually holds.

Exercise

Next Steps

You now know how to install Deppy, annotate functions with @guarantee and assume, run the verifier, and read its output. In the next chapter we will explore refinement types — a more expressive way to describe the values a function accepts and returns.