Decorator Form

@foundation / @axiom / @verify — proof annotations inline with Python.

Two Equivalent Sidecar Forms

Deppy supports two interchangeable shapes for the proof-relevant metadata attached to a module:

• .deppy sidecar files — a separate-file YAML-shaped form for the case where you are retrofitting proof obligations onto code you didn't write (sympy, numpy, …). The sympy_geometry case study uses this form.
• Decorators inside a Python module — for the case where you are writing the module yourself and want the proof metadata to live next to the implementation it constrains.

Both produce a SidecarModule and feed the same verify pipeline. There is no semantic difference.

Quick Start

A complete example. Place this in my_module.py:

from deppy.proofs.sidecar_decorators import (
    foundation, axiom, verify, spec, lemma,
    psdl_proof, by_lean, code_type, predicate, constant,
    lean_import, lean_preamble,
)


@foundation
def Real_sqrt_nonneg():
    """sqrt(x) >= 0 when x >= 0"""


@axiom(
    target="my_module.Point.distance",
    statement="Point.distance(p, q) >= 0",
)
def dist_nonneg():
    """Distance is non-negative."""


@spec(
    # guarantees must be Python expressions / lean: / smt: —
    # NL strings are rejected by ``_validate_formal``.
    guarantees=["Point.distance(p, q) >= 0"],
    axioms=["dist_nonneg"],
)
class Point:
    def __init__(self, x, y):
        self.x = x
        self.y = y

    @verify(
        property="Point.distance(p, q) >= 0",
        via="foundation Real_sqrt_nonneg",
        binders={"p": "Point", "q": "Point"},
    )
    @psdl_proof("""
if isinstance(other, Point):
    inline(Point.distance, sqrt(sum_zip_sub_sq(self, other)))
    apply(Real_sqrt_nonneg)
    assert sum_zip_sub_sq(self, other) >= 0, "z3"
else:
    raise NotImplementedError
""")
    def distance(self, other):
        from math import sqrt
        return sqrt((self.x - other.x) ** 2 + (self.y - other.y) ** 2)

Run:

$ python -m deppy.pipeline.run_verify --from-module my_module

Or programmatically:

import my_module
from deppy.proofs.sidecar_decorators import extract_sidecar_module
sm = extract_sidecar_module(my_module)

from deppy.lean.sidecar_runner import _run_with_module
from pathlib import Path
rr = _run_with_module(
    sm,
    out_path=Path("my_module.lean"),
    sidecar_path=Path(my_module.__file__),
)
print(rr.certified)  # True / False

The repository ships examples/decorated_geometry.py as a fully verified worked example — running python -m deppy.pipeline.run_verify --from-module examples.decorated_geometry produces ✓ CERTIFIED — top-level certify_or_die: PASS end-to-end.

Decorator Reference

How Extraction Works

Each decorator stamps the function (or class) with a __deppy_*__ attribute carrying the metadata as a dict. At extraction time, extract_sidecar_module(module) walks the module's members (including methods of classes) and reassembles a SidecarModule with the same fields a parsed .deppy file would produce.

The pipeline that runs after extraction is identical:

1. Foundation Z3 discharge.
2. Mechanization to concrete Lean Props.
3. Per-method body translation.
4. Per-verify-block kernel verification + counterexample search.
5. PSDL compilation when @psdl_proof is set.
6. Lean certificate emission + lean_runner round-trip.
7. JSON sidecar emission.
8. certify_or_die verdict.

When to Use Which Form

The decorator form is best when:

• The function being verified IS the function carrying the @verify decorator.
• You want refactors to keep the proof metadata aligned with the implementation (renaming the function automatically renames the verify block's function: target via __qualname__).
• You want the proof obligations to be discoverable via dir(mod).

The .deppy form is best when:

• The module being verified is read-only (third-party library).
• Multiple .deppy files compose via import (one per sub-module of a large library).
• You want to publish the proof metadata as a separate artefact (audit log, reproducibility manifest).

Composition with .deppy

A module may use both: decorators inline define one piece of the sidecar; a separate .deppy file describes external dependencies. The two are unioned at extraction time.

# my_module.py
@foundation
def MyFact():
    """x + 0 == x"""

# my_module.deppy
import generic_arith.deppy   # external foundations

axiom external_claim:
  target: third_party.lib
  statement: "…"

# Run both — decorator form adds the inline foundations; .deppy
# adds the external claims.
$ python -m deppy.pipeline.run_verify --from-module my_module
$ python -m deppy.pipeline.run_verify my_module.deppy

End-to-End Verification

Running the shipped example produces this exact output (run on 2026-04-27):

$ python -m deppy.pipeline.run_verify \
    --from-module examples.decorated_geometry \
    --out decorated_geometry.lean

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