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

arXiv · 2609.24252

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

View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LO cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

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. 2026-09-21. Iris in Lean. https://arxiv.org/abs/2609.24252

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

KEEP EXPLORING

Related papers

arXiv2026

PICID: Proof-Driven Clause Learning in Neural Network Verification

Current Deep Neural Network (DNN) verifiers are typically designed to prioritize scalability over reliability. Reliability can be reinforced through the generation of proofs that are checkable by trusted, external proof checkers. To date, only a handful of verifiers support proof production; and these rely on verifier-specific formats, and balance between scalability, proof detail, and the trustworthiness of their proof checker. In this tool paper, we introduce PICID, a DNN verifier that produces proofs in the standard Alethe format for SMT solving, checkable by an independent checker. PICID implements a parallel CDCL(T) architecture that integrates the state-of-the-art, proof-producing CaDiCaL SAT solver with the Marabou DNN verifier. Furthermore, PICID leverages UNSAT proofs to derive conflict clauses. Our evaluation shows that PICID generates valid proofs in the vast majority of cases and significantly outperforms existing tools that produce comparable proofs.

cs.LO↗

arXiv2026

Confluence of conditional rewriting modulo

Sets of equations E play an important computational role in rewriting-based systems R. The equivalence relation =E induced by E introduces a partition of terms into E-equivalence classes on which rewriting computations, denoted ->R/E and called rewriting modulo E, are issued. This paper investigates confluence of ->R/E, usually called E-confluence, for conditional rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize such a framework to be used with conditional systems. Then, we show how to define appropriate finite sets of conditional pairs to prove and disprove E-confluence. We introduce (i) Logic-based Conditional Critical Pairs, which do not require the use of (often infinitely many) E-unifiers to provide a finite representation of the local peaks considered in the abstract framework. We also introduce (ii) parametric Conditional Variable Pairs which are essential to deal with conditional rules in the analysis of E-confluence. Finally, we introduce (iii) Down Conditional Pairs which are often necessary to disprove E-confluence. Our results apply to well-known classes of rewriting-based systems, improving on previous results. As for unconditional systems, our results apply to Equational Term Rewriting Systems, first investigated by Huet and then by Jouannaud, and Jouannaud and Kirchner, among others. As for conditional systems, our results also apply to conditional rewrite theories and Maude.

cs.LO↗

arXiv2026

Verifying Numerical Methods with Isabelle/HOL

Modern machine learning pipelines are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. Therefore, we contribute a framework for verified numerical methods in Isabelle/HOL based on ITrees. Our user-friendly specification language enables the direct declaration of numerical programs that can be annotated with variants and invariants for reasoning about correctness specifications. The generated verification conditions can be discharged via automated proof methods and lemmas from the HOL-Analysis library. The ITrees foundation interacts with Isabelle's code generator to export source code. This provides an end-to-end path from formal specifications with machine-checked guarantees to executable sources. We illustrate the process of modelling numerical methods and demonstrate the effectiveness of the verification by focusing on two well-known methods, the bisection method and the fixed-point iteration method. We also contribute crucial extensions to the libraries of formalised mathematics required for this objective: higher-order derivatives and Taylor's theorem in Peano form. Finally, we qualitatively evaluate the use of the framework for verifying numerical methods.

cs.LO↗