Deppy

About This Book

This book is a tutorial and reference for Deppy, a proof-oriented verification system for Python. It is modeled after the F* Tutorial Book, but with a crucial difference: where F* is a language you write new code in, Deppy verifies the Python code you already have.

We cover everything from basic refinement types and Z3 integration to advanced topics: homotopy-theoretic path types, Čech decomposition for modular verification, the cubical heap with epoch-tagged mutation and transport-based reads, coalgebraic generators / coroutines, and GIL-aware concurrency proofs.

Sidecar metadata can be written in two equivalent forms — a separate .deppy file (best for verifying third-party libraries) or decorator-based annotations inline with Python (@foundation, @axiom, @verify, @psdl_proof; best when you write the module yourself). Both feed the same kernel.

A Quick Example

Here is a simple Python function and its Deppy verification. The source code remains untouched — the specification lives in a sidecar file.

# Ordinary Python — no Deppy imports needed if you use a sidecar.
def abs_val(x: int) -> int:
    if x >= 0:
        return x
    return -x

# Separate-file YAML-shaped sidecar; sits beside my_math.py
module: my_math

spec my_math.abs_val:
  guarantee: "abs_val(x) >= 0"

verify abs_val_nonneg:
  function: my_math.abs_val
  property: "abs_val(x) >= 0"
  via: "z3"

Or, with the equivalent decorator form (when you write the module yourself):

from deppy.proofs.sidecar_decorators import verify, psdl_proof

@verify(
    property="abs_val(x) >= 0",
    via="z3",
    binders={"x": "int"},
)
@psdl_proof("""
if x >= 0:
    assert x >= 0, "z3"
else:
    assert -x >= 0, "z3"
""")
def abs_val(x: int) -> int:
    return x if x >= 0 else -x

Run the verifier — both forms feed the same kernel and the same Lean-export round-trip:

$ python -m deppy.pipeline.run_verify my_math.deppy --out my_math.lean
$ python -m deppy.pipeline.run_verify --from-module my_math --out my_math.lean

  ────────────────────────────────────────────────
  deppy.lean.lean_runner round-trip:       OK
  ────────────────────────────────────────────────
  ✓ CERTIFIED — top-level certify_or_die: PASS

Why Deppy?

Existing proof-oriented systems require you to learn a new language and rewrite your code. Deppy meets Python developers where they are.

Table of Contents

A Taste of Verification

Deppy supports several styles of specification. Here's a richer example using the @guarantee decorator for inline annotation, refined for refinement types, and Nat() as the canonical non-negative integer type:

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

# Nat() is shorthand for refined(PyIntType(), "x >= 0", "x")
Nat_t = Nat()

@guarantee("result == n * (n + 1) // 2")
def triangle(n: int) -> int:
    """Sum of integers from 0 to n."""
    return n * (n + 1) // 2

$ python -m deppy.pipeline.run_verify triangle.deppy --out triangle.lean

  ────────────────────────────────────────────────
  deppy.lean.lean_runner round-trip:       OK
  ────────────────────────────────────────────────
  ✓ CERTIFIED — top-level certify_or_die: PASS

Verification is fast. Z3 handles arithmetic obligations automatically, and Deppy decomposes complex proofs into manageable pieces using Čech decomposition from algebraic topology.

Getting Started

Ready to dive in? We recommend reading the pages in order:

1. Structure of this Book — understand the six parts and prerequisites
2. Introduction — the key ideas behind Deppy
3. Getting Started — install Deppy and verify your first function