# Iris in Lean > Iris-Lean fully reimplements Iris in Lean, outperforming Iris-Rocq in automation speed, and enabling probabilistic program verification via Mathlib integration. - **Source:** [arXiv](https://arxiv.org/abs/2609.24252) - **Published:** 2026-09-26 - **Permalink:** https://picx.dev/p/h0gsGi - **Whiteboard:** https://picx.dev/p/h0gsGi/image ## Summary ## Summary (Overview) - **Iris-Lean** is a comprehensive reimplementation of the Iris framework for concurrent separation logic, originally developed in Rocq (Coq), now rebuilt in the Lean proof assistant. - The project covers all non-experimental features of Iris, including the base logic, the Iris Proof Mode (IPM), the algebraic hierarchy, and the HeapLang program logic. - Key innovations include: a novel IPM implementation leveraging Lean's metaprogramming, use of quotient types to simplify OFE equivalence handling, integration with Mathlib for heavy mathematical reasoning, and a Diaframe-like automation tactic called *Wander*. - The authors demonstrate the framework's utility through a *Continuous Probabilistic Program Logic* (CTE) for reasoning about programs manipulating random real numbers. - Performance benchmarks suggest significant speedups in proof automation compared to Iris-Rocq, and the project is open-source on GitHub and Zenodo. --- ## Introduction and Theoretical Foundation Iris is a well-established framework for **higher-order concurrent separation logic**, used to verify safety, security, and probabilistic properties of programs. Its mechanization in Rocq has been crucial for adoption, providing both a sound foundation and the **Iris Proof Mode (IPM)**—a tactic language for interactive reasoning inside the embedded logic. The motivation for reimplementing Iris in Lean is threefold: 1. **Metaprogramming**: Lean's flexible metaprogramming enables a more powerful and ergonomic IPM. 2. **Automation**: Lean's `simp` and typeclass synthesis infrastructure can replace custom-built automation in Rocq. 3. **Mathlib integration**: Access to Lean's extensive mathematical library supports program logics with heavy mathematical dependencies (e.g., measure theory for probabilistic verification). The theoretical foundation rests on: - **Step-indexed semantics** for reasoning about recursive and coinductive features. - **Bunched implications (BI)** as the logical core. - **OFEs (Ordered Families of Equivalences)** for modeling resources. - **Ghost resources** and **monotone predicates** for separation logic resources. --- ## Methodology ### Algebraic Hierarchy and Bundling Iris-Lean reimplements the algebraic hierarchy using a **mixed bundling strategy**: - **Unbundled typeclasses** for type-level operations (e.g., `Dist`, `Equiv`). - **Bundled structures** for properties like `OFE` and `BI` to enable typeclass inference. Lean's lack of cumulative universes required a novel approach: Iris-Lean uses **universe-polymorphic structures** with explicit universe parameters, avoiding the limitations of Rocq's design. This also enabled a merge request to Iris-Rocq adopting the same approach. ### Quotient Types for Equivalences Iris-Rocq uses setoids for OFE equivalences (≡). Iris-Lean instead: - Requires `≡` to coincide with `=` (Leibniz equality) for most structures. - Uses **quotient types** when equivalence does not hold definitionally. - This simplifies rewriting and reduces boilerplate, leveraging Lean's built-in quotient support. ### Proof Mode (IPM) in Lean The IPM is reimplemented using: - A single inductive tree type `Hyps` for the spatial and persistent context. - **Typed expressions** (`Lean.Expr`) for metaprogrammatic manipulation. - A custom typeclass synthesizer built on Lean's own, reusing infrastructure for `TC` and `Hint Mode`-like annotations. - Direct parser integration for tactic syntax (no string literals), improving usability and type information. ### Automation: Wander *Wander* is a tactic mimicking Diaframe's automation for Iris proofs. It: - Reuses Lean's `simp` for simplification. - Implements proof search for separation logic goals. - Supports automatic introduction, framing, and solving of goals. ### Fixed Point Elaborators Iris-Lean provides custom elaborators for defining **Iris fixed points** (least/greatest fixed points of monotone functions, and contractive fixed points) in a style similar to Lean's `def` and `inductive`, reducing boilerplate. --- ## Empirical Validation / Results - **HeapLang port**: Over 80% of the HeapLang separation logic and examples are ported, including a concurrent counter and quicksort specification. - **Performance**: Benchmarks show Iris-Lean's IPM and automation outperform Iris-Rocq in several cases, with significant speedups in proof search. - **Probabilistic Program Logic**: The CTE logic was successfully implemented, requiring: - Equipping program expressions with a `MeasurableSpace`. - Generalizing countable sums to Lebesgue integrals. - Proving adequacy and soundness results. The authors also used **temporary linters and attributes** to track generalization of definitions during the CTE development, preserving build integrity. --- ## Theoretical and Practical Implications - **Design insights**: The paper shows how Lean's features (quotients, metaprogramming, typeclass synthesis) can simplify and improve upon Rocq-based designs. - **Interoperability**: The `rocq_alias` tool helps maintain correspondence with Iris-Rocq, easing future synchronization. - **Broader impact**: Iris-Lean could become canonical infrastructure for program verification in Lean, with potential integration with `CSLib` and `Std.Do`. - **Mathematical integration**: The ability to use Mathlib enables program logics with heavy mathematical content (e.g., measure theory), opening new application areas. --- ## Conclusion Iris-Lean is a complete reimplementation of Iris in Lean, demonstrating that Lean's modern features can enhance both the ergonomics and performance of separation logic frameworks. The project achieves full coverage of Iris's non-experimental features, introduces novel automation and metaprogramming techniques, and validates its approach through a probabilistic program logic. **Future directions**: - Continued synchronization with Iris-Rocq. - Integration with Lean's evolving standard library and CSLib. - Exploration of further automation and user-facing tooling. The authors envision Iris-Lean as a foundation for future program verification research in Lean, with the full codebase available at [GitHub](https://github.com/leanprover-community/iris-lean) and Zenodo. --- _Markdown view of https://picx.dev/p/h0gsGi, served by PicX — AI-generated visual whiteboard summaries of research papers._