Structure of this Book

This book is organized into six progressive parts, plus an "Under the Hood" appendix. Each part builds on the previous ones, but experienced readers can skip ahead — we note dependencies where they arise.

The book follows a verify-existing-code philosophy throughout. Every example starts with ordinary Python and adds verification externally. You never need to modify your source code to use Deppy.

Who Is This Book For?

This book is aimed at three audiences:

Python developers who want to add formal guarantees to their code without learning a new language. If you've used type hints or mypy, you already have the right intuitions.
Verification engineers familiar with F*, Dafny, or Coq who want to apply their skills to the Python ecosystem. Deppy will feel familiar but with key differences around dynamic typing and sidecar proofs.
Researchers interested in the application of homotopy type theory to practical programming language verification. Parts 5 and the appendix provide theoretical depth.

Prerequisites

Required

Comfortable reading and writing Python 3.10+
Basic understanding of type hints (int, list[str], Optional)
Familiarity with pip, virtual environments, and the command line

Helpful but Not Required

Experience with property-based testing (Hypothesis)
Exposure to formal logic or proof assistants
Basic knowledge of abstract algebra or topology (for Part 5)
Familiarity with async/await and threading (for Part 6)

We introduce every concept from scratch with Python examples. You do not need prior experience with formal verification, type theory, or homotopy theory to read Parts 1–4.

The Six Parts

Part 1

Pure Python — Refinement Types & Z3

We begin with the bread and butter of formal verification: refinement types. You'll learn how to annotate Python functions with preconditions and postconditions, and have Z3 discharge the proof obligations automatically. We cover termination checking, lemma-based reasoning, structural induction, and culminate in a fully verified quicksort implementation.

Key idea: Even without homotopy theory, Deppy's refinement types and Z3 integration provide a powerful verification experience comparable to Liquid Haskell or Dafny — but for Python.

Part 2

Advanced Proofs — Generics, Dependent Types & Metatheory

Building on Part 1, we tackle more expressive type-level reasoning: generic types with type-variable constraints, length-indexed vectors, cryptographic Merkle trees with hash-collision proofs, equality and path types, logical connectives as types, and a formalization of the simply typed lambda calculus with type safety proofs.

Key idea: Python's dynamic nature doesn't prevent dependent-type reasoning. Deppy lifts runtime values into the type level using refinements and path types.

Part 3

Python Specifics — Duck Typing, Decorators & Dynamic Types

Python has features that no other verified language deals with: pervasive duck typing, decorators that transform function signatures, metaclasses, and a fully dynamic type system where type(x) can change at runtime. This part shows how Deppy uses homotopy-theoretic paths to model structural subtyping (duck typing as path equivalence), decorator composition as fibrations, and dynamic type changes as transport along paths.

Key idea: Duck typing is not chaos — it is structural equivalence, and homotopy type theory is the natural language for reasoning about it.

Part 4

Sidecar Proofs — Verifying Libraries Without Modification

The defining feature of Deppy: verifying code you didn't write and can't modify. We explain the .deppy sidecar file format, the equivalent decorator form for code you do control, trust levels and verification confidence, and a full case study verifying parts of SymPy's symbolic algebra engine.

Key idea: Proofs about library code live beside the library — either in .deppy sidecars or in @verify / @psdl_proof decorators stamped on the functions. The kernel pipeline is the same either way.

Part 5

Homotopy Methods — Paths, Transport, Čech, Fibrations & PSDL

The theoretical heart of Deppy. We develop cubical path types for reasoning about type equivalences, transport for moving proofs across equivalent types, Čech decomposition for breaking complex verification into local patches that glue together, and fibrations for modeling dependent structures. The PSDL chapter introduces the Python-syntax tactic language: every proof body is just Python parsed via ast and translated to kernel ProofTerms.

Key idea: Homotopy type theory provides a compositional framework — verify locally, assemble globally — that scales to large codebases in ways that monolithic SMT queries cannot. PSDL is the surface syntax that makes the homotopy machinery feel like ordinary Python.

Part 6

Heap & Concurrency — Cubical Heap, Separation Logic vs Pulse, Threading & Async

Python is not a purely functional language: it has mutable references, arrays, shared state, the GIL, threads, and async/await. This part introduces the cubical heap — Deppy's epoch-tagged world-path model of mutation — then contrasts it with classical separation logic and the Pulse verifier (Microsoft Research). It then verifies mutable data structures, proves thread-safety properties (with GIL-awareness), and shows how to verify async Python code with structured concurrency guarantees.

Key idea: Mutation is a path in the world category. Aliases are DuckPaths at the cell level; reads after mutations require TransportProof; per-cell invariants live in the fibre over each cell. This is a different soundness story from Pulse's separating-conjunction frame rule, with different tradeoffs we make explicit chapter by chapter.

Appendix

Under the Hood — Implementation Details

For the curious reader: how Deppy is built. We describe the internal architecture, how Python ASTs are translated into the type-theoretic core, how Z3 is used as a leaf-obligation solver within the homotopy framework, and how sidecar files are parsed and bound to their targets.

How to Read This Book

Linear Path (Recommended for Beginners)

Read Parts 1 through 4 in order. These take you from zero to productive Deppy usage. Part 5 (homotopy methods) and Part 6 (heap/concurrency) can then be read in either order depending on your interests.

Fast Track for Verification Engineers

If you've used F*, Dafny, or Liquid Haskell:

Skim Introduction for the key differences
Read Getting Started for setup
Jump to Part 3: Python Specifics
Then Part 4: Sidecar Proofs

Theory Track for Researchers

If you're interested in the homotopy-theoretic foundations:

Read the Introduction
Skim Refinement Types and Equality & Path Types
Dive into Part 5: Homotopy Methods
Read Under the Hood

Conventions Used in This Book

Throughout this book we use the following visual conventions:

Code Blocks

Python source code that you would write or already have:

def greet(name: str) -> str:
    return f"Hello, {name}!"

Deppy specifications in .deppy sidecar files:

spec module.greet:
  guarantee: "len(greet(name)) > 0"

verify greet_nonempty:
  function: module.greet
  property: "len(greet(name)) > 0"
  via: "z3"

Or equivalently, in decorator form:

from deppy.proofs.sidecar_decorators import verify, psdl_proof

@verify(property="len(greet(name)) > 0", via="z3")
@psdl_proof('auto()')
def greet(name: str) -> str:
    return f"Hello, {name}!"

Callout Boxes

Informational notes provide additional context or clarify subtleties.

Tips offer practical advice for common patterns.

Warnings flag common pitfalls or surprising behavior.

Exercises invite you to practice what you've learned. Solutions are provided at the end of each chapter.

Verification Badges

When we show verification output, we use colored badges to indicate the result:

Z3_VERIFIED — Obligation discharged by Z3 with a machine-checked proof.

LEAN_KERNEL_VERIFIED — Proof exported to Lean 4 and checked by its kernel.

FAILED — Verification failed — either a bug or an insufficient specification.