PastaLean: Deterministic transpilation from Python to Lean for Verification

Anirudh Gupta, Petros Markopoulos, Siddhartha Gadgil

cs.PL Oct 25, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

Transpiles Python into shallow Lean 4 embeddings via Lean metaprogramming, producing a provable twin with contract theorems and a runnable twin for execution.

Abstract

We present PastaLean, an extensible system for deterministic translation from Python to Lean via the Abstract Syntax Tree of Python. This allows for verification of Python code, especially auxiliary code used by AI. Every program is translated into a provable twin written in the form Lean's verification tooling can reason about, and a runnable twin that gives a fast and correct computation support. We also introduce our Type Inference engine TypeInfer which provides static typing support for untyped Python code. Our tool provides coverage of more than 92% for LeetCode and HumanEval\textsuperscript{+} and more than 98% for LiveCodeBench ground truth Python files. Further, at least 97% of each dataset's (numerical) test cases pass, with 100% on HumanEval\textsuperscript{+} and LiveCodeBench. The TypeInfer engine is the best-scoring tool on the TypeEvalPy static leaderboard, and on a repository-level TypyBench benchmark it scores above every competing repository-level inference tool.

Problem

Code produced by AI agents is mostly Python, while formal verification is done in languages such as Lean 4. Python's dynamic typing, mutable state and object model make translating it into a verifiable form difficult.

Approach

PastaLean parses Python with the built-in ast module, serializes the nodes to JSON, and recursively generates typed Lean syntax using extensible translation functions registered in a Lean environment extension. The Lean code is a shallow embedding with two twins: a provable twin for verification and a computable twin for execution. Contracts written in Python are translated into Lean theorems. A type inference engine, TypeInfer, supplies static types for untyped Python.

Results

The generated Lean elaborates for 92.1% of HumanEval+, 92.4% of LeetCode and 98.5% of LiveCodeBench programs. Test agreement with CPython on elaborated programs is 100%, 97.0% and 100% respectively. TypeInfer scores best on the TypeEvalPy static leaderboard and on the repository-level TypyBench benchmark, and the translator outperforms direct LLM translation into Lean.

Dataset	Problems	Elaborated (%)	Tests	Passed (%)
HumanEval+	164	151 (92.1)	7,007	7,007 (100.0)
LeetCode	2,589	2,391 (92.4)	215,126	208,736 (97.0)
LiveCodeBench	476	469 (98.5)	10,213	10,213 (100.0)

Code generation and execution (elaborated programs and passed tests)

Papers With

PastaLean: Deterministic transpilation from Python to Lean for Verification