Iris in Lean
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu, Oliver Soeser, Fernando Leal, Alvin Tang, Max Vistrup, Ralf Jung, Mario Carneiro, Joseph Tassarotti, Michael Sammler, Lars Birkedal
cs.LO
Sep 21, 2026 · v1
cs.PL
TL;DR
Reimplements the Iris concurrent separation logic framework in Lean 4, using metaprogramming and quotient types, and integrates with Mathlib.
Abstract
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-quality mechanization in Rocq. This mechanization uses a number of Rocq features in sophisticated ways, including a carefully constructed algebraic hierarchy for modeling separation logic resources, and a proof mode for embedded separation logic proofs, which combines custom Ltac with extensible typeclasses. The library has been developed for over a decade with dozens of contributors, with an emphasis on modularity and maintainability. We explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris. Using these features, we provide a novel implementation of the Iris proof mode with improved performance, simplify the handling of equivalences through quotient types, build a variant of Diaframe proof automation, and provide convenience features like automatic construction of Iris fixed points. Building on Lean lets us integrate with the extensive Mathlib library, allowing us to re-use results from this library for program verification tasks that have heavy mathematical dependencies, as we demonstrate with an application to probabilistic program verification.
Problem
Iris, a framework for higher-order concurrent separation logic, is mechanized in Rocq using sophisticated Ltac and typeclass machinery. Reproducing and extending this in a way that supports better automation and reuse of mechanized mathematics is challenging, particularly for probabilistic program logics needing measure theory.
Approach
Iris-Lean is a from-scratch port of Iris to Lean 4, tracking correspondence to Iris-Rocq per declaration. It reimplements the Iris Proof Mode (based on MoSeL) using Lean metaprogramming to manipulate hypotheses and goals as first-class objects, replaces setoid equivalences with equality via quotient types, and builds a Diaframe-style automation variant. Integration with Mathlib enables reuse of measure-theoretic results for program verification.
Results
The Lean IPM implementation improves performance and offers the same functionality as the Rocq version. As a case study, the authors develop Continuous Total Eris, described as the first program logic able to verify higher-order, stateful, continuous probabilistic programs using conventional measure theory, addressing limitations of prior Iris-based probabilistic logics.
