provably

Z3-backed formal verification for Python — via decorators and refinement types.

An awkronos library. The Python sibling of provably for Rust.

fromprovablyimportverified@verified(pre=lambdaval, lo, hi: lo<=hi,post=lambdaval, lo, hi, result: (result>=lo) & (result<=hi),)defclamp(val: float, lo: float, hi: float) ->float:
ifval<lo:
returnloelifval>hi:
returnhielse:
returnvalclamp.__proof__.verified# True — for ALL inputs where lo <= histr(clamp.__proof__) # "[Q.E.D.] clamp"

verified=True is a mathematical proof. Z3 determined that no input satisfying the precondition can violate the postcondition.

Install

pip install provably
# or: uv add provably

Examples

Pre/post contracts

@verified(pre=lambdaa, b: b>0,post=lambdaa, b, result: (result>=0) & (result<b),)defmodulo(a: int, b: int) ->int:
returna%bmodulo.__proof__.verified# Truemodulo.__proof__.solver_time_ms# ~2ms

Refinement types

fromtypingimportAnnotatedfromprovably.typesimportBetween, Gt, NonNegative@verified(post=lambdap, x, result: result>=0)defscale(
p: Annotated[float, Between(0, 1)],
x: Annotated[float, Gt(0)],
) ->NonNegative:
returnp*xscale.__proof__.verified# True

Counterexample extraction

@verified(pre=lambdan: n>=0,post=lambdan, result: result*result==n, # wrong)defbad_sqrt(n: int) ->int:
returnn//2bad_sqrt.__proof__.counterexample# e.g. {'n': 7, '__return__': 3} — 3*3 != 7# Z3 returns *some* input that breaks the contract; the exact value may vary.

Compositionality

@verified(contracts={"my_abs": my_abs.__contract__},post=lambdax, y, result: result>=0,)defmanhattan(x: float, y: float) ->float:
returnmy_abs(x) +my_abs(y)
manhattan.__proof__.verified# True

While loops

Bounded while loops are unrolled (up to 256 iterations), just like for loops:

@verified(pre=lambdan: (n>=0) & (n<=10),# Use `2 * result == n * (n + 1)`, not `result == n * (n + 1) // 2`:# `//` is not defined on Z3 expressions inside a contract lambda.post=lambdan, result: 2*result==n* (n+1),)deftriangle(n: int) ->int:
total=0i=0whilei<n: # variant: n - ii+=1total+=ireturntotaltriangle.__proof__.verified# True

Walrus operator

@verified(post=lambdax, result: (result>=0) & ((result==x) | (result==-x)),)defmy_abs(x: float) ->float:
return (neg:=-x) ifx<0elsexmy_abs.__proof__.verified# True

Match/case (Python 3.10+)

match/case statements are desugared to if/elif/else for Z3:

@verified(pre=lambdacode: (code>=0) & (code<=3),post=lambdacode, result: (result>=10) & (result<=40),)defdispatch(code: int) ->int:
matchcode:
case0: return10case1: return20case2: return30case _: return40dispatch.__proof__.verified# True

Tuple returns

Subscript the result with a constant index — result is a tuple, so a bare result >= 0 is a type error:

@verified(post=lambdax, y, result: (result[0] ==x+y) & (result[1] ==x-y),)defsum_and_diff(x: float, y: float) ->tuple:
return (x+y, x-y)
sum_and_diff.__proof__.verified# True

Lean 4 backend

Cross-check Z3 results with an independent proof assistant:

fromprovablyimportverify_with_lean4, export_lean4cert=verify_with_lean4(clamp, pre=lambdav, lo, hi: lo<=hi,
post=lambdav, lo, hi, r: (r>=lo) & (r<=hi))
lean_code=export_lean4(clamp, output_path="clamp.lean")

Supported constructs

Construct	Supported
+, -, *, //, /, %, **n	Yes
<, <=, >, >=, ==, !=	Yes
and, or, not, &, |, ~	Yes
if/elif/else/ternary	Yes
match/case (Python 3.10+)	Yes (desugared to if/elif/else)
min, max, abs	Yes
pow, bool, int, float, len, round	Yes
sum, any, all	Yes
Annotated refinement types	Yes
Calls via contracts=	Yes
Walrus operator (:=)	Yes
Tuple returns + constant subscript (t[0])	Yes
while loops (bounded, max 256 iterations)	Yes (unrolled)
for i in range(N) (literal N, max 256)	Yes (unrolled)
assert statements	Yes (become proof obligations)
x in [...] / x not in [...] over a list literal	Yes (expanded to a disjunction)
List comprehensions over range(N) inside sum/any/all	Yes (unrolled)
Lean 4 backend (verify_with_lean4)	Yes (requires Lean 4)
Recursion	No
str, dict	No
list as a parameter or return type	No (list literals are supported — see the two rows above)
Unbounded loops, generators, async	No

Comparison

Library	Approach	Proof strength	Call-site overhead
provably	SMT / Z3	Mathematical proof	Zero solver overhead
deal	Runtime contracts	Bug finding	Per-call
icontract	Runtime contracts	Bug finding	Per-call
CrossHair	Symbolic execution	Property testing	Test-time
beartype	Runtime types	Type checking	Per-call

Benchmark

make bench proves the same property — ERC-20 transfer overflow safety, end-to-end — with provably and with real contract-verification tooling (halmos, pysmt-z3, cvc5, raw z3, solc SMTChecker), then compares wall time.

make bench # writes /tmp/kagami-provably-bench.json# {"actual": ..., "sota": ..., "sota_name": ..., "efficiency_pct": ..., "competitors": [...]}# efficiency_pct > 100 means provably beat the fastest competitor.

Links

• Product architecture — Python ↔ Rust ↔ pcc-core ↔ pcc-sp1
• Documentation
• Getting started
• How it works
• Self-proof
• API reference
• Sibling crates: provably-rs · pcc-core · pcc-sp1
• Changelog · License (MIT)

---

awkronos — a small penguin with snow on its head. We prove the math you've been meaning to do.

awkronos.com · essays