provably

Formal verification for Python — via decorators, refinement types, and Z3/Lean4 backends

✓ Self-proving Zero solver overhead at call time Counterexample extraction

from provably import verified

@verified(
    pre=lambda val, lo, hi: lo <= hi,
    post=lambda val, lo, hi, result: (result >= lo) & (result <= hi),
)
def clamp(val: float, lo: float, hi: float) -> float:
    if val < lo:
        return lo
    elif val > hi:
        return hi
    else:
        return val

clamp.__proof__.verified   # True — for ALL inputs where lo <= hi
clamp.__proof__.status     # Status.VERIFIED
str(clamp.__proof__)       # "[Q.E.D.] clamp"

verified=True is a mathematical proof -- not a test, not a sample. The contract holds for every possible input satisfying the precondition.

Python source → AST parse → Z3 constraints → SMT query ¬post → UNSAT → Q.E.D.

Install

pipuv

pip install provably

uv add provably

What makes provably different

### Proof certificates Z3 returns UNSAT. The proof attaches to `func.__proof__` at import time.

cert = clamp.__proof__
cert.verified       # True
cert.solver_time_ms # 2.4

### Counterexamples When a contract fails, Z3 returns the exact input that breaks it.

@verified(post=lambda n, r: r * r == n)
def bad(n: int) -> int:
    return n // 2

bad.__proof__.counterexample
# {'n': 2, '__return__': 1}

### Refinement types Embed bounds directly in type annotations via `Annotated`.

@verified
def scale(
    p: Annotated[float, Between(0, 1)],
    x: Annotated[float, Gt(0)],
) -> NonNegative:
    return p * x

### Compositionality Reuse verified contracts without re-examining function bodies.

@verified(
    contracts={"abs": abs.__contract__},
    post=lambda x, y, r: r >= 0,
)
def dist(x: float, y: float) -> float:
    return abs(x) + abs(y)

### Runtime checking `@runtime_checked` asserts contracts at call time. No Z3 required.

@runtime_checked(
    pre=lambda x: x >= 0,
    post=lambda x, r: r * r <= x + 1,
)
def isqrt(x: int) -> int:
    ...

### Self-verifying provably proves 16 of its own functions on every CI push — including while loops, walrus operators, and type casts. If it can't prove its own builtins, the build breaks. [Self-Proof →](self-proof.md)

### While loops & match/case Bounded `while` loops (unrolled up to 256 iterations), `match`/`case` statements, and walrus `:=` operator — all verified.

@verified(
    pre=lambda n: (n >= 0) & (n <= 10),
    post=lambda n, result: result == 0,
)
def countdown(n: int) -> int:
    while n > 0:
        n = n - 1
    return n

### Lean4 backend Cross-check Z3 proofs with Lean4's type checker, or export theorems to `.lean` files.

from provably import verify_with_lean4

cert = verify_with_lean4(
    clamp, pre=..., post=...
)
cert.z3_version  # "lean4:v4.x.0"

### Tuple returns & new builtins Verify functions returning `(a, b, ...)` tuples. `pow`, `bool`, `int`, `float`, `len`, `round` all supported as builtins.

@verified(
    post=lambda x, result:
        result >= 0,
)
def cast_nonneg(x: Annotated[int, Ge(0)]) -> float:
    return float(x)

Documentation

Getting started	Install, first proof, what Q.E.D. means
How it works	AST translation, Z3 queries, the TCB
Refinement types	Annotated markers, convenience aliases
Contracts	Pre/post lambda syntax, &/| vs and/or
Compositionality	Modular verification, proof dependencies
Soundness	What "proven" means, epistemological limits
Supported Python	Supported and unsupported constructs
Pytest integration	CI assertions, verify_module()
Errors and debugging	Counterexamples, TranslationError fixes
Self-proof	provably verifies its own functions
FAQ	Common questions, Lean4 backend, @verified vs @runtime_checked