Part 1: Programming & Proving with Pure Python

Part 1 introduces the foundations of formal verification with Deppy: how to attach precise specifications to ordinary Python functions and have those specifications machine-checked. Every function we verify in this part is pure — no mutation, no I/O, no side effects — which keeps reasoning tractable while we build intuition for the tools.

By the end of Part 1 you will be able to write refinement-typed Python, discharge proof obligations with Z3, prove lemmas by induction, argue termination, and combine all of these techniques in a verified quicksort implementation.

What You'll Learn

• How to install Deppy and run the verifier on a Python file
• Refinement types: constraining values beyond their base type
• How Deppy dispatches proof obligations to the Z3 SMT solver
• Defining algebraic data types with Python dataclasses
• Proving termination of recursive functions via decreasing measures
• Writing lemmas and structuring inductive proofs
• Putting it all together: a fully verified quicksort

Philosophy: Verify What You Already Write

Most verification systems ask you to rewrite your code in a new language. Deppy takes the opposite approach: your existing Python is the program. Specifications live in a sidecar file or in lightweight decorators that the Python runtime ignores. The verifier reads your .py source, builds a cubical type-theoretic model of its behaviour, and checks that model against your specs — all without executing your code.

This means:

• No new syntax to learn — it's just Python.
• No runtime overhead — verification happens at check time.
• No language lock-in — remove the decorators and you have plain Python.

Where F* asks you to program in its language, Deppy asks you to program in Python and prove alongside it.

Unverified Python vs. Deppy-Verified Python

Consider a function that computes the absolute value of an integer. Here is the standard, unverified version:

def abs_val(x: int) -> int:
    if x >= 0:
        return x
    return -x

This is perfectly good Python, but nothing stops a caller from misunderstanding the return type. With Deppy we can add a machine-checked refinement:

from deppy import guarantee, Nat

@guarantee("result >= 0")
def abs_val(x: int) -> Nat:
    # Nat is a refinement: int where value >= 0
    if x >= 0:
        return x
    return -x

The function body is identical. The only additions are the @guarantee decorator and the Nat return type — both of which the Python runtime ignores. Deppy's verifier reads them, encodes the obligation result >= 0 as a Z3 query, and discharges it automatically.

Your First Taste

Here is a slightly richer example: a function that doubles every element in a list, with a postcondition relating the output length to the input length.

from deppy import guarantee, assume, check

@guarantee("len(result) == len(xs)")
def double_all(xs: list[int]) -> list[int]:
    """Return a new list with every element doubled."""
    if not xs:
        return []

    head, *tail = xs
    rest = double_all(tail)

    # Deppy checks this inductively:
    # len(rest) == len(tail)  by recursive guarantee
    # len([head*2] + rest) == 1 + len(tail) == len(xs)  ✓

    return [head * 2] + rest

Running python -m deppy.pipeline.run_verify double_all.py produces:

$ python -m deppy.pipeline.run_verify double_all.py
double_all ··· len(result) == len(xs)
  ├─ base case (xs = []):  Z3 ✓  0.02s
  ├─ inductive step:       Z3 ✓  0.04s
  └─ termination:          structural (len) ✓
All 1 function(s) verified.

Chapter Summary

# Create and activate a virtual environment
python3 -m venv .venv
source .venv/bin/activate

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

# Optional: Z3 for strongest verification
pip install z3-solver

A Peek at Refinement Types

Refinement types are the workhorse of Part 1. A refinement type takes an existing Python type and narrows it with a logical predicate. For example, Nat is int refined by value >= 0.

from deppy import refined, guarantee, Nat, Pos
from deppy.types import PyIntType

# Two equivalent ways to spell the same refinement
Nat_t = Nat()                                     # shorthand
Pos_t = refined(PyIntType(), "x > 0", "x")        # explicit

@guarantee("result > 0")
def successor(n: int) -> int:
    return n + 1

@guarantee("result >= x and result >= y")
def max_of(x: int, y: int) -> int:
    if x >= y:
        return x
    return y

Deppy translates each @guarantee into a Z3 assertion and checks it against every execution path. If successor returned n instead of n + 1, the verifier would report a counterexample: n = 0 ⇒ result = 0, which violates Pos.

What Comes Next

Ready to start? Head to Getting Started to install Deppy, verify your first function, and set up your editor for inline verification feedback. Each subsequent chapter builds on the last, culminating in the Quicksort Case Study where we prove both correctness and termination of a classic sorting algorithm — written in plain Python.