PastaLean

Transpiling and Verifying Python in Lean 4 — without LLMs

Anirudh Gupta · IISc Bengaluru

Petros Markopoulos · UC San Diego

Siddhartha Gadgil · Professor · IISc Bengaluru

21 July 2026

GitHub PyAstLean

Overview

• Why verify Python at all — and why in Lean

• How PastaLean turns Python into Lean, node by node

• What we support: control flow, classes, libraries…

• Proving the generated code correct

What are we cooking?

Pasta + Python + Lean 4 =

P·ast·aLean → PastaLean

How to eat(use) PastaLean?

• Take ordinary, logical Python — the kind data scientists and practical logical code's LLMs actually write.

• Preprocess Python code for Type annotations, obtain it's Abstract Syntax Tree(AST) and give Lean it's JSON format.

• Transpile it into Lean 4 — deterministically, with no LLM, so the meaning never drifts.

• Prove it correct — and let Lean's proof automation do the heavy lifting with a little help by LLM's.

The Goal: write in Python, get the guarantees of a proof assistant.

What is the Inspiration for this dish?

• Two things dominate how code gets written today: Python (the language) and LLMs (increasingly, the author).

• A huge and growing share of the Python running in the world was drafted by an LLM.

• But here's the uncomfortable question:

Who checks that the generated code is actually correct?

• Tests only catch the bugs you thought to write — never the ones you didn't.

• To prove correctness (not merely test it), we reach for formal methods: Hoare logic, model checking, multi-modal verification…

• Proof assistants make that practical — and there are several: Lean 4, Rocq (Coq), Isabelle, Dafny, …

• We use Lean 4: a proof assistant that is also a fast, real programming language.

Why Lean?

Lean 4 is a proof assistant and a general-purpose language (it compiles to C — genuinely fast).

• Powerful automation — tactics like simp, grind, aesop, etc. search proofs and close goals for you, often in one line.

• Endlessly customizable — custom syntax, macros, and tactics let you extend the language itself — exactly how PastaLean is built.

• Trusted where it matters — used by Fields medallist Terence Tao, backed by the Lean FRO, applied to industrial verification.

• A small, auditable kernel re-checks every proof — nothing is taken on faith.

See Leo de Moura's blog Why Lean?.

Why convert Python into Lean?

• Blindly trusting an LLM's Python means shipping logic no one has proved — silent wrong answers, bad edge cases, security holes.

PastaLean gives that code a home where the compiler is the reviewer:

• if it type-checks against our runtime, the translation is faithful;

• if the proof closes, the logic is correct.

Write it in Python. Trust it like Lean.

And because pure Python becomes bare Lean terms, we can state and prove theorems about it.

Why transpile — and not just ask an LLM?

The obvious shortcut: "LLM, translate this Python to Lean." We deliberately do not do that for the core translation. LLMs earn their keep elsewhere — proposing contracts — never as the translator.

Other Possible methods maybe?

• Other Methods like using FFI is possible, however theorem proving would not be possible.

• Converting Lean to Python is possible, however legacy python checking would not be possible and there are a lot more python programmers.

How does PastaLean taste code?

It reads Python's AST and emits Lean you can prove:

def sum_to_n(n: int) -> int:
    Requires(n >= 0)
    total = 0
    for i in range(n + 1):
        Invariant(2*total == i*(i - 1))
        total = total + i
    Ensures(2*total == n*(n + 1))
    return total

FunctionDef(name='sum_to_n',
  args=[arg('n', Name('int'))],
  body=[
    Expr(Call(Requires,
      Compare(Name'n', GtE, 0))),
    AnnAssign('total', Name'int', 0),
    For('i', Call(range, …), body=[
      Expr(Call(Invariant, …)),
      Assign('total', BinOp(…, Add, …))]),
    Expr(Call(Ensures, …)),
    Return(Name'total')])

Two Functions for each code

PastaLean converts each function in Python into 2 functions each with it's own purpose:

• Provable - This function is meant to be used for property proving of the function.

• Computable - This function is meant to be computable with #eval. These are marked with 'rn in function name, which stands for run.

Example of Provable/Computable Function

One Python function forks into two Lean definitions:

def euclidean_distance(p1, p2):
    if len(p1) != len(p2):
        raise ValueError("Points must have the same number of dimensions")

    # Using zip, list comprehension, and math.pow
    sq_diffs = [math.pow(a - b, 2) for a, b in zip(p1, p2)]
    return math.sqrt(sum(sq_diffs))

Classes / OOP

A Python class becomes a Lean structure plus namespaced method definitions. self is the structure value, and mutation is value-semantics (C.new builds one):

class Point:
    def __init__(self, x, y):
        self.x = x
        self.y = y

    def norm_sq(self):
        return self.x*self.x \
             + self.y*self.y

obj = Point(1,2)
norm = obj.norm_sq()

Libraries

Implementing Library and integrating it in PastaLean is very trivial.

• All you do is write the Lean function for your Python implementation, use our builtin typeclasses support if needed. All Libraries are independently implementable.

• Now just map the member name to a Lean runtime function. This will automatically integrate with our code generation pipeline.

• numpy, pandas, scipy, math, typing ship today; anything unsupported degrades to a flagged pyUnsupported so the file still compiles.

A slice of numpy:

A major Problem: Python is dynamically typed

• In Python a name has no fixed type — it is just a label on a value, and the type is checked only at runtime.

• One function serves every type (duck typing), and a variable can even change type mid-body.

# one function, many types
def add(a, b):
    return a + b

add(1, 2)          # 3
add("Hi", "!")     # "Hi!"

# one name, two types
x = 1              # int
x = "hello"        # now str

• Native Lean can't paper over it — you'd write an explicit, closed union Int ⊕ String ⊕ … and pattern-match at every single use.

• Python code never declares that union — and it spreads virally through every caller and return.

• Worse. Even len(x), x[i], + need a concrete type for instance resolution; a bare "any" leaves them stuck.

…and Python ignores its own type hints

• Moreover, Python allows multiple return Types from a function!

• Python doesn't even follow it's own type hints, so we can only rely on them with a pinch of salt.

# one function, many types
def add(a: int, b: int) -> int:
    return a + b

add("Hi", "!")  # This works!

We need Python's dynamism without poisoning everything with unions.

Limitations — where the line is

Honest about what PastaLean does not do:

• Not all of Python — only the static "logic" subset; no async, yield, eval, or monkey-patching.

• Proofs aren't free — taste? / mvcgen are best-effort automation; hard goals still need a manual proof.

• Libraries are hand-written — a new library's functions are implemented + mapped once, then reused everywhere.

• Unsupported → pyUnsupported — anything out of scope degrades to a flagged placeholder, so the rest of the file still compiles.

When we can't translate faithfully, we refuse loudly — never miscompile.

Proving we cooked correctly

Is it correct? The proof path forks on one thing — a bare term or a do block:

A preference to Non-monadic pure functional code is given while converting. However it will be lowered to Monadic code with do, when necessary.

Why lower into a monad at all?

Pure functions are total and side-effect free, so they cannot directly express state updates, early exits, or external effects like IO. Lowering into a monad gives these behaviors a precise semantic model while keeping the code composable and type-safe.

• print / input → IO

• raise / try / except → PyExcept = ExceptT PyException IO

• loops / mutation → Id.run do (pure, but still a do block)

Tradeoff : Extensibility vs Harder to Prove

The one place an LLM helps: contracts

How do we even say what we want to prove?

• Annotate Python with contracts — Requires, Ensures, Invariant, Decreases, or a plain assert.

• PastaLean extracts them as preconditions, postconditions, and per-loop obligations.

• The LLM proposes the contracts; mvcgen + taste? discharge the proof.

def factorial(n: int) -> int:
    Requires(n >= 0)
    Ensures(Result() >= 1)
    result, i = 1, 1
    while i <= n:
        Invariant(i >= 1)
        Invariant(n - i + 1 >= 0)
        Invariant(result >= 1)
        Decreases(n - i + 1)
        result = result * i
        i = i + 1
    return result

Best Effort Automatic Proving with taste?

A Python assert on a pure function becomes theorem … := by taste? — the Pastafolio engine searches (simp · grind · ring · nlinarith · fun_induction) and splices the found proof back:

# showcase/linalg/matrix_model.py
def det(a, b, c, d):
    return a*d - b*c

# scaling a 2×2 by k scales det by k²
assert det(k*a, k*b, k*c, k*d) \
    == k**2 * det(a, b, c, d)

The found tactic is spliced back over taste? — the committed proof is concrete.

Proving monadic defs: mvcgen

do-block functions use Std.Do's mvcgen with Hoare triples ⦃P⦄ prog ⦃Q⦄; Python contracts ride along as Invariant / Ensures:

def sum_upto_n(n: int) -> int:
    Requires(n >= 0)
    total = 0
    for i in range(n + 1):
        Invariant(2*total == i*(i - 1))
        total += i
    Ensures(2*total == n*(n + 1))
    return total