Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.34205

PastaLean: Deterministic transpilation from Python to Lean for Verification

Anirudh Gupta·Petros Markopoulos·Siddhartha Gadgil
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Anirudh Gupta, Petros Markopoulos, Siddhartha Gadgil. 2026-10-25. PastaLean: Deterministic transpilation from Python to Lean for Verification. https://arxiv.org/abs/2610.34205

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

Tanaka et al. proposed a type system for verifying functional correctness properties of programs that use arrays and pointer arithmetic. Their system extends ConSORT--a type system combining fractional ownership and refinement types for imperative program verification--with support for pointer arithmetic. Their idea was to extend fractional ownership so that it can depend on an array index. Their formulation, however, does not handle nested arrays, which are essential for representing practical data structures such as matrices. We extend Tanaka et al.'s type system to support nested arrays by allowing ownership to depend on the indices of enclosing arrays. We formalize the extended calculus in Rocq using a mixed embedding and provide a machine-checked proof of type soundness. We have implemented a verifier based on the proposed type system and demonstrated that it can verify the correctness of programs that manipulate nested arrays, which were beyond the reach of Tanaka et al.

cs.PL↗
arXiv2026

On the Expressive Power of Hook-Indexed State: Comprehending State in the React UI Library (Extended Version)

React is currently the most popular JavaScript library for front-end web development. It endows UI components with state via the useState construct, through a mechanism that we name hook-indexed state. However, React's implementation of hook-indexed state is both fragile and poorly understood. Programmers frequently experience unexpected behavior, and the benefits of programming in this paradigm are wholly unclear. We define $λ^\mathsf{react}_\mathsf{hook}$, a core calculus that captures the essence of hook-indexed state, and give it a type system to statically rule out unexpected behavior. We then translate $λ^\mathsf{react}_\mathsf{hook}$ into a calculus $λ^\mathsf{react}_\mathsf{ref}$ based on ML-style references, and prove that this translation preserves typability and semantics, thus showing that hook-indexed state is expressible in terms of standard references. The translation is local and admits a compositional definition, but involves significant code duplication. As well as illuminating the essence of state in React, our observations can inform the design of future reactive programming systems.

cs.PL↗
arXiv2026

Special Delivery: Programming with Mailbox Types (Extended Version)

The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Behavioural types make it possible to detect communication errors early in the development process, but most work has addressed channel-based languages rather than actor languages. Mailbox types are a novel behavioural type system for actors first introduced for a process calculus, and capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language incorporating mailbox types, and describes an algorithmic type system. Pat is a higher-order functional language with sums, products, and lists, along with interfaces that allow finer-grained reasoning about mailbox contents. Typechecking in Pat detects four classes of behavioural error: protocol violation, unexpected message, forgotten reply and self-deadlock, as well as the usual data type errors. The Pat type system makes essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. We make use of a co-contextual algorithmic type system, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite. This establishes a foundation for applying mailbox typing to practical actor languages.

cs.PL↗