LemmaPy

Status: M0–M2 complete. The pipeline runs end-to-end on the v1 fragment: #@ specs parse (grammar v0.2, frozen), compile to runtime contracts that CrossHair searches for counterexamples, and translate to Dafny for SMT proofs (lemmapy verify). All four soundness layers are built — conformance checking (lemmapy check), boundary guards with the attack gallery demonstrably stopped (lemmapy guard), island integrity with assumptions A1–A7 in the verification report (--report), and continuous translation validation (lemmapy difftest, in CI on every PR). The M2 agent layer is live: structured failures (verify --json), the proof-repair loop (lemmapy repair), benchmark-derived repair and spec-writing exams, and an LSP (lemmapy lsp) that runs at two speeds — instant conformance diagnostics on every keystroke, prover verdicts on explicit request, expiring the moment the buffer changes (docs/EDITOR.md). Sixteen corpus functions are proven — including gcd's full maximality spec, modp's modular-power spec and sum_to_n's closed form via the #@ proof lemma-sidecar mechanism, and isqrt's maximality spec with no proof additions at all — and scored 16/16 on lemmapy-benchmark's assurance ladder (62/77 mutants refuted by the specs, 81%; 13 more crash and 2 diverge under mutation — caught by the interpreter or the wall rather than by the specification, so reported separately and never credited). Licensed under MIT.

Developers (and LLM agents) annotate production Python with specifications in #@ comments. The toolchain translates a precisely defined typed fragment into Dafny, where an SMT-backed verifier discharges the proofs — with LLM assistance for the ones automation misses. The Python file stays the source of truth: CPython ignores the annotations, and no code is rewritten in another language.

#@ verified
#@ requires forall i in range(len(xs) - 1) :: xs[i] <= xs[i + 1]
#@ ensures result == -1 or (0 <= result < len(xs) and xs[result] == target)
def binary_search(xs: list[int], target: int) -> int:
    lo, hi = 0, len(xs)
    while lo < hi:
        #@ invariant 0 <= lo <= hi <= len(xs)
        #@ invariant forall k in range(lo) :: xs[k] < target
        #@ invariant forall k in range(hi, len(xs)) :: xs[k] > target
        mid = (lo + hi) // 2
        if xs[mid] < target:
            lo = mid + 1
        elif xs[mid] > target:
            hi = mid
        else:
            return mid
    return -1

Try it

pip install -e ".[dev]"

Hunt for counterexamples at runtime (no proof needed — CrossHair searches the compiled #@ contracts):

lemmapy hunt examples/clamp.py

This prints false when calling clamp(-1, 0, 0) — a concrete counterexample to the seeded bug in examples/clamp.py, found from the specs alone, with no test written.

Prove a function correct for all inputs (typed fragment → Dafny → SMT; requires Dafny on PATH):

lemmapy verify examples/contact/he_humaneval_13.py --time-limit 60

That's Euclid's gcd verified against its full spec — divides both arguments and is the greatest such divisor — with the divisibility lemma pack supplied in a .proofs.dfy sidecar referenced from a #@ proof clause. Failures map back to the Python source line.

Score the whole task corpus on the assurance ladder (gate → hunt → mutants → encode → prove → fidelity):

lemmapy benchmark

Why this is not "just run a verifier on Python"

Python is dynamically typed, and a type checker's acceptance is not soundness. The project's central claim is that dynamic typing decomposes into four distinct threats, each answered by an independently checkable mechanism (ARCHITECTURE.md):

The result is a precise, honest guarantee: verified properties hold for every execution entering through the generated guards with all executable checks passing, in programs the conformance checker accepts, under stated assumptions, with the encoder continuously cross-checked against CPython.

Design commitments (v1)

How this differs from adjacent work

• Strata-Python (AWS) — the nearest neighbor, one layer down: it translates Python into the Laurel IVL for SMT verification, but specs are machine-oriented serialized files, there is no protection for verified code called from untyped Python, and no proof-repair workflow. Laurel is a candidate second backend for this toolchain, not a substitute for it.
• Nagini — proves the front-end shape works (typed Python, shallowly encoded into an IVL); this project trades its Viper permission logic for SMT/LLM automation and adds the boundary-guard and translation-validation layers.
• CrossHair / icontract / beartype — the dynamic-checking ecosystem; used by this project (M0 compiles the same #@ specs to runtime checks) rather than competed with.
• TensorGuard / TorchLean — domain-specific (tensor metadata / neural-network mathematics); this project verifies user-stated functional properties of general typed Python.

Documentation map