Volume
LIPIcs, Volume 382
17th International Conference on Interactive Theorem Proving (ITP 2026)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP)
Event
Editors
Publication Details
- published at: 2026-07-16
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-436-9
Access Numbers
- Detailed Access Statistics available here
-
Total Accesses (updated on a weekly basis)
0Documents
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 382, ITP 2026, Complete Volume
Abstract
LIPIcs, Volume 382, ITP 2026, Complete Volume
Cite as
17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 1-652, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@Proceedings{komendantskaya_et_al:LIPIcs.ITP.2026,
title = {{LIPIcs, Volume 382, ITP 2026, Complete Volume}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {1--652},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026},
URN = {urn:nbn:de:0030-drops-273071},
doi = {10.4230/LIPIcs.ITP.2026},
annote = {Keywords: LIPIcs, Volume 382, ITP 2026, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 0:i-0:xvi, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{komendantskaya_et_al:LIPIcs.ITP.2026.0,
author = {Komendantskaya, Ekaterina and Nipkow, Tobias},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {0:i--0:xvi},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.0},
URN = {urn:nbn:de:0030-drops-273066},
doi = {10.4230/LIPIcs.ITP.2026.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk)
Abstract
Cloud computing relies on hypervisors to enforce isolation between co-tenanted virtual machines. Hypervisors are therefore critical security infrastructure, and assurance of their correctness is paramount. Traditional engineering techniques - code review, testing, fuzzing - provide strong assurance but cannot exhaustively verify that isolation holds across all possible execution paths. Formal verification extends and complements these approaches by establishing mathematical guarantees about system behaviour.
This talk presents our experience applying interactive theorem proving to verify a production hypervisor component: the Nitro Isolation Engine. This is a trusted, minimalist computing base written in Rust, enforcing isolation between virtual machines on AWS Graviton5 EC2 instances. Designed for verification from inception, we have specified the intended behaviour of this component and verified correctness in the Isabelle/HOL interactive theorem prover, producing approximately 330,000 lines of machine-checked models and proofs, and establishing three key classes of property:
1) Functional correctness: The system behaves as specified for all operations including virtual machine creation, memory mapping, and abort handling. Our total verification approach additionally establishes memory-safety, termination, and absence of runtime errors.
2) Confidentiality: A noninterference-style property demonstrates that guest virtual machine state remains hidden from an expansive definition of observer monitoring system actions, formalised as indistinguishability preservation up to permitted declassification flows.
3) Integrity: Guest virtual machine private state is unaffected by operations on distinct virtual machines. Currently, our proof coverage extends to verification of the core virtual machine-management hypercalls, guest power management, various utility hypercalls, and a subset of data, instruction, and asynchronous abort handling, and will continue to expand to cover more functionality including PCI device management and virtual GIC (Generic Interrupt Controller) handling.
The talk will discuss the verification approach, key proof techniques, and challenges in applying formal methods to production systems. Note that this work builds on decades of academic research across interactive theorem proving, formal specification, separation logic and its automation, and programming language semantics.
Cite as
Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, and Konrad Slind. Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{becker_et_al:LIPIcs.ITP.2026.1,
author = {Becker, Hanno and Chong, Nathan and Dockins, Robert and Grundy, Jim and Hu, Jason and Mulder, Ike and Mulligan, Dominic P. and Mure, Paul and Parno, Bryan and Paulson, Lawrence C. and Slind, Konrad},
title = {{Nitro Isolation Engine: Formally Verifying a Production Hypervisor}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {1:1--1:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.1},
URN = {urn:nbn:de:0030-drops-269757},
doi = {10.4230/LIPIcs.ITP.2026.1},
annote = {Keywords: Isabelle/HOL, Rust, verification, separation logic, hypervisors}
}
Document
Invited Talk
Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk)
Abstract
We describe our experience developing qrhl-tool, a theorem prover for verifying quantum cryptographic protocols, both in the post-quantum and the full quantum setting. The tool is built around quantum relational Hoare logic (qRHL), a relational program logic for reasoning about pairs of quantum programs in the style of game-based cryptographic proofs. We discuss the design choices underlying the tool: in particular, a hybrid architecture that delegates ambient-logic reasoning to Isabelle/HOL while qrhl-tool itself handles qRHL judgments and the program language; an advanced memoization mechanism (hashed computations) that enables efficient incremental proof checking; and a deliberate path towards a foundational implementation. We walk through a small worked example (the hardness of inverting f∘f given a one-way permutation f) to illustrate how these pieces fit together in practice. Along the way we highlight what we got right, what we got wrong, and which limitations (procedure parameters, local variables, runtime reasoning) we would approach differently if starting over today.
Cite as
Dominique Unruh. Developing a Quantum Crypto Theorem Prover from Scratch (Invited Talk). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 2:1-2:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{unruh:LIPIcs.ITP.2026.2,
author = {Unruh, Dominique},
title = {{Developing a Quantum Crypto Theorem Prover from Scratch}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {2:1--2:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.2},
URN = {urn:nbn:de:0030-drops-269763},
doi = {10.4230/LIPIcs.ITP.2026.2},
annote = {Keywords: Formalized mathematics, functional analysis, bounded operators}
}
Document
Complex Bounded Operators in Isabelle/HOL
Abstract
We present a formalization of bounded operators on complex vector spaces in Isabelle/HOL. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces, Hilbert spaces) that complements and goes beyond the developments of real vectors spaces in the Isabelle/HOL standard library. We define the type of bounded operators between complex vector spaces (cblinfun) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the Jordan_Normal_Form AFP entry.
Cite as
Dominique Unruh and José Manuel Rodríguez Caballero. Complex Bounded Operators in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{unruh_et_al:LIPIcs.ITP.2026.3,
author = {Unruh, Dominique and Caballero, Jos\'{e} Manuel Rodr{\'\i}guez},
title = {{Complex Bounded Operators in Isabelle/HOL}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {3:1--3:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.3},
URN = {urn:nbn:de:0030-drops-269772},
doi = {10.4230/LIPIcs.ITP.2026.3},
annote = {Keywords: Formalized mathematics, functional analysis, bounded operators}
}
Document
Formally Verified Liveness with Multiparty Session Types in Rocq
Abstract
Multiparty session types (MPST) offer a framework for the description of communication-based protocols involving multiple participants. In the top-down approach to MPST, the communication pattern of the session is described using a global type. Then the global type is projected on to a local type for each participant, and the individual processes making up the session are type-checked against these projections. Typed sessions possess certain desirable properties such as safety, deadlock-freedom and liveness.
In this work, we present the first mechanised proof of liveness for synchronous multiparty session types in the Rocq Proof Assistant. Building on recent work, we represent global and local types as coinductive trees using the Paco library. We use a coinductively defined subtyping relation on local types together with another coinductively defined plain-merge projection relation relating local and global types. We then associate collections of local types, or local type environments, with global types using these projection and subtyping relations, and prove an operational correspondence between a local type environment and its associated global type. We utilise this association relation to prove the safety and liveness of associated local type environments and, consequently, the multiparty sessions typed by these environments.
Besides clarifying the often informal proofs found in the MPST literature, our Rocq mechanisation also enables the certification of liveness properties of communication protocols. Our contribution amounts to around 14K lines of Rocq code, available at https://github.com/omerskeskin/mpstlive.
Cite as
Omer Keskin, Nobuko Yoshida, and Rob van Glabbeek. Formally Verified Liveness with Multiparty Session Types in Rocq. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{keskin_et_al:LIPIcs.ITP.2026.4,
author = {Keskin, Omer and Yoshida, Nobuko and van Glabbeek, Rob},
title = {{Formally Verified Liveness with Multiparty Session Types in Rocq}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {4:1--4:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.4},
URN = {urn:nbn:de:0030-drops-269787},
doi = {10.4230/LIPIcs.ITP.2026.4},
annote = {Keywords: Multiparty Session Types, Liveness, Safety, Fairness, Deadlock-Freedom, Endpoint Projection, Subtyping, Rocq, Coinduction, Property Verification}
}
Document
Enhancing Interactive Theorem Prover Error Messages with Hints
Abstract
Interactive theorem provers (ITPs) are promising tools for ensuring program correctness, but users often complain about their poor usability and steep learning curve. A common complaint, especially among new users, are confusing error messages that expose details of the ITP’s underlying theory or implementation details. In this work, we investigate how adding hints to three types of scope and type checking error messages in the Agda ITP affects the new users' debugging experience. We evaluate the effectiveness and perceived helpfulness of those error messages by conducting a between-subjects user study where we provide a series of Agda code snippets, each containing a single error that the participants have to fix based on the error message. We measure the success rate, time taken to fix the error, and perceived helpfulness for each code snippet with the original as well as the enhanced error message and determine the statistical significance of adding the hint. Our results show that correct hints can improve the success rate and time taken to fix the error, and that error messages with hints are rated significantly more helpful than those without. Additionally, we find that while error messages with incorrect hints are often rated as more misleading, they do not significantly impact the success rate or time taken to fix the error. These results show that adding hints to error messages is a viable step on the path towards making ITPs more widely accessible.
Cite as
Maria Khakimova, Sára Juhošová, Jaro Reinders, and Jesper Cockx. Enhancing Interactive Theorem Prover Error Messages with Hints. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{khakimova_et_al:LIPIcs.ITP.2026.5,
author = {Khakimova, Maria and Juho\v{s}ov\'{a}, S\'{a}ra and Reinders, Jaro and Cockx, Jesper},
title = {{Enhancing Interactive Theorem Prover Error Messages with Hints}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {5:1--5:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.5},
URN = {urn:nbn:de:0030-drops-269791},
doi = {10.4230/LIPIcs.ITP.2026.5},
annote = {Keywords: Agda, error messages, hints, new users}
}
Document
Lazy Proof Automation for Separation Logic
Abstract
Separation Logic is an established formalism for deductive verification of heap-manipulating programs. Proofs of symbolic heap entailment, an analogue of the ordinary logical implication, are amongst the most common reasoning steps in Separation Logic, and many existing heap verifiers provide automation for discharging valid heap entailments.
We observe that existing techniques for automating entailment proofs in foundational Separation Logic verifiers embedded into provers such as Rocq, suffer from three main drawbacks: (a) poor performance due to metaprogramming overhead, (b) limited expressivity, and (c) restricted extensibility. To address these shortcomings, we propose lazy proof automation - an approach to entailment proofs inspired by translation validation. Our key idea is to implement an entailment checker as a combination of (1) an efficient but unverified prover, suitable for fast-paced interactive proofs, and (2) a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori. We implemented these ideas in Yolo - a generic and extensible heap entailment prover built in Lean. We instantiate Yolo for two Lean-embedded Separation Logics and show its practical benefits, both in terms of user experience and proof-checking speed, compared with the automation available in state-of-the-art foundational Separation Logics.
Cite as
Valentin Mikhalchuk, Vladimir Gladshtein, and Ilya Sergey. Lazy Proof Automation for Separation Logic. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mikhalchuk_et_al:LIPIcs.ITP.2026.6,
author = {Mikhalchuk, Valentin and Gladshtein, Vladimir and Sergey, Ilya},
title = {{Lazy Proof Automation for Separation Logic}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {6:1--6:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.6},
URN = {urn:nbn:de:0030-drops-269801},
doi = {10.4230/LIPIcs.ITP.2026.6},
annote = {Keywords: Lean, proof engineering, meta-programming}
}
Document
Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations
Abstract
Commutative regular expressions describe sets of unordered words, and are used, for example, when building type systems for process calculi. In these applications, an important operation is finding the intersection of two expressions, but no algorithm currently exists. We remedy this by proposing an algorithm for computing intersections of commutative regular expressions, which we implement and prove correct in the Rocq prover. The algorithm encodes the intersection of two expressions as systems of linear Diophantine equations, and extracts from their solution an intersection expression. To solve these systems we implement and verify the algorithm proposed by Contejean and Devie. We detail the implementation of the intersection algorithm, highlight essential aspects of the proofs (including the complex proof of termination of the equation system solver), and evaluate the OCaml-extracted solver on random and real-world commutative regular expressions.
Cite as
Ricardo Almeida, Blair Archibald, Basile Pesin, and Michele Sevegnani. Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{almeida_et_al:LIPIcs.ITP.2026.7,
author = {Almeida, Ricardo and Archibald, Blair and Pesin, Basile and Sevegnani, Michele},
title = {{Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.7},
URN = {urn:nbn:de:0030-drops-269813},
doi = {10.4230/LIPIcs.ITP.2026.7},
annote = {Keywords: commutative regular expressions, linear Diophantine equations, interactive theorem provers, Rocq}
}
Document
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral
Abstract
Understanding and certifying the generalization performance of machine learning algorithms - i.e. obtaining theoretical estimates of the test error from the training error - is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, Rademacher complexity yields sharp, data-dependent bounds that apply well beyond classical VC-dimension theory. In this study, we formalize the generalization error bound by Rademacher complexity in Lean 4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from countable hypothesis classes (where measurability of suprema is straightforward in Mathlib) to separable topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under 𝓁₂ and 𝓁₁ regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.
Cite as
Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sonoda_et_al:LIPIcs.ITP.2026.8,
author = {Sonoda, Sho and Kasaura, Kazumi and Mizuno, Yuma and Tsukamoto, Kei and Onda, Naoto},
title = {{Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {8:1--8:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.8},
URN = {urn:nbn:de:0030-drops-269824},
doi = {10.4230/LIPIcs.ITP.2026.8},
annote = {Keywords: Lean, generalization error bound, Rademacher complexity, McDiarmid’s inequality, Hoeffding’s lemma, symmetrization arguments, chaining, Dudley’s entropy integral}
}
Document
Functional Correctness of an Optimized Modular Inversion Algorithm
Abstract
This article describes the first mechanized proof of functional correctness of an algorithm due to Pornin (2020), for computing modular inverses via an optimized extended binary GCD algorithm. This algorithm is widely used in cryptography applications, due to its speed and constant-timeness. But this speed comes from the use of approximate computations during its loop iterations. In particular, the pen-and-paper proof of the fact that sufficiently many loop iterations were performed is especially intricate (and the originally published version was actually wrong), which negatively impacts the trust in the applications that rely on the algorithm. In this work, we expand the notes provided in the original description by Pornin into a complete formal proof. We discuss the challenges raised by its mechanization, which eventually relies on the collaboration of deductive program verification and interactive theorem proving through the use of the tools Rocq and Why3.
Cite as
Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, and Tomás Vallejos Parada. Functional Correctness of an Optimized Modular Inversion Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mahboubi_et_al:LIPIcs.ITP.2026.9,
author = {Mahboubi, Assia and Melquiond, Guillaume and Strub, Pierre-Yves and Vallejos Parada, Tom\'{a}s},
title = {{Functional Correctness of an Optimized Modular Inversion Algorithm}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {9:1--9:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.9},
URN = {urn:nbn:de:0030-drops-269839},
doi = {10.4230/LIPIcs.ITP.2026.9},
annote = {Keywords: deductive program verification, modular inversion algorithm, formal verification, Rocq, Why3}
}
Document
Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL
Abstract
We present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems.
Cite as
Fang Yan, Benoît Ballenghien, Simon Foster, Ana Cavalcanti, James Baxter, and Burkhart Wolff. Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 10:1-10:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{yan_et_al:LIPIcs.ITP.2026.10,
author = {Yan, Fang and Ballenghien, Beno\^{i}t and Foster, Simon and Cavalcanti, Ana and Baxter, James and Wolff, Burkhart},
title = {{Automated Verification of Robot Software Models with Assume-Guarantee Reasoning in Isabelle/HOL}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {10:1--10:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.10},
URN = {urn:nbn:de:0030-drops-269849},
doi = {10.4230/LIPIcs.ITP.2026.10},
annote = {Keywords: process algebra, Isabelle/HOL, automated proof methods, deadlock freedom}
}
Document
Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language
Abstract
Intermediate Verification Languages (IVLs) play the same role in verification as Intermediate Representations in compilation, a layer that separates a verifier’s language-specific front-end from its logic automation back-end. Successful IVL tools such as Boogie, Why3, and Viper generate Verification Conditions (VCs) that are sent to an SMT solver. The verifier output can be trusted only if these VCs are sound with respect to the formal semantics of the IVL. Formalizing the semantics of IVLs and verifying the soundness of corresponding VC Generators with respect to this semantics is challenging if one wants to model realistic features of IVLs such as mutually recursive definitions, lexical variable and control-flow labeled scopes, interpreted and uninterpreted functions, and unbounded loops.
B3 is a new IVL. This paper presents a formalization of B3’s semantics, a VC Generator for the language, and a soundness proof that these two correspond. A key practical contribution of this work is that all three components are authored in the Dafny programming language and verifier. This makes it easy for a tool maintainer to maneuver between the semantic definitions, the proofs, and the VCG’s executable code. The key theoretical contribution of the work is a methodology to split the IVL’s semantic encodings into two layers of abstraction to cover realistic aspects of the semantics, while keeping the proofs amenable to automation. Optimized for Dafny-style automation, the first layer is used to verify the correctness of the VC Generator procedure. Optimized for expressiveness, the second layer is used to capture the semantics in a natural way.
Cite as
Vladimir Gladshtein and K. Rustan M. Leino. Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gladshtein_et_al:LIPIcs.ITP.2026.11,
author = {Gladshtein, Vladimir and Leino, K. Rustan M.},
title = {{Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.11},
URN = {urn:nbn:de:0030-drops-269855},
doi = {10.4230/LIPIcs.ITP.2026.11},
annote = {Keywords: Intermediate verification language, Soundness, Verification, B3, Dafny, SMT solvers}
}
Document
TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq
Abstract
The free-variable tableau method has been widely used in order to automate proofs in multiple kinds of logics. Many automated theorem provers rely on this approach, either because it is the only available method - e.g. in certain modal logics - or because it facilitates the generation of proof certificates. However, as far as the authors know, its results have never been formalized in a proof assistant. In this paper, we present TableauxRocq, a deep embedding of free-variable first-order tableaux in the Rocq prover. The formalized calculus is proved sound and provides a modular Skolemization system that enables the use of Skolemization-based optimizations. Moreover, we show how TableauxRocq can be used as a certifier for automated theorem provers by adapting the Goeland prover - that can already output Rocq terms - to output proofs in the TableauxRocq format. By using the power of reflection, thereby providing a fully certified proof checker for free, we show that Goeland’s exported Rocq terms and TableauxRocq’s proof certificates can be checked in a similar time frame without proof optimizations, and that the latter has strictly better performances in presence of Skolemization-related optimizations.
Cite as
Johann Rosain and Julie Cailler. TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{rosain_et_al:LIPIcs.ITP.2026.12,
author = {Rosain, Johann and Cailler, Julie},
title = {{TableauxRocq: A Deep Embedding of Free-Variable Tableaux in Rocq}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {12:1--12:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.12},
URN = {urn:nbn:de:0030-drops-269869},
doi = {10.4230/LIPIcs.ITP.2026.12},
annote = {Keywords: The Rocq Prover, First-Order Tableaux, Automated Reasoning, Interoperability, Proof Translation}
}
Document
Verification of the Garsia-Wachs Algorithm
Abstract
The Garsia-Wachs algorithm is an algorithm for finding a leaf-labeled binary tree whose leaf sequence exactly matches the input weight sequence and whose cost is as small as possible, where the cost is the sum of the weights labeling the leaves multiplied by their levels. The algorithm, along with a proof of correctness due to Kingston, is presented in Knuth’s The Art of Computer Programming, Vol. 3. The algorithm comes in two versions, the naive and the optimized. Both versions have quadratic time complexity, but the optimized version can be fine-tuned with a suitable data structure to yield an O(n log n)-time algorithm. I implement and verify a variant of each version of the algorithm in the verification-aware programming language Dafny. Unlike all previous presentations of the algorithm, these variants construct the desired optimum tree directly, without detour through a "nonalphabetic" tree whose leaf sequence is a rearrangement of the input sequence.
Cite as
Makoto Kanazawa. Verification of the Garsia-Wachs Algorithm. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{kanazawa:LIPIcs.ITP.2026.13,
author = {Kanazawa, Makoto},
title = {{Verification of the Garsia-Wachs Algorithm}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {13:1--13:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.13},
URN = {urn:nbn:de:0030-drops-269877},
doi = {10.4230/LIPIcs.ITP.2026.13},
annote = {Keywords: Garsia-Wachs algorithm, Dafny}
}
Document
Certified Infinite Descent Criteria in Isabelle/HOL
Abstract
Infinite Descent is the global trace condition that underpins the soundness of cyclic reasoning and, in program analysis, the size change termination principle. Many (semi-)decision procedures for Infinite Descent are known, based on criteria ranging from automata-based constructions and relation-based characterizations, to effective (but incomplete) heuristics. Although these criteria are well studied on paper and implemented in tools, a unified, machine-checked account that relates them to the (abstract) Infinite Descent property has been missing. We present an Isabelle/HOL mechanization of this landscape. We develop a reusable, locale-based framework of sloped graphs that defines Infinite Descent at an abstract level, independently of any concrete graph encoding. Within this framework we formalize standard complete criteria and prove their equivalence to the locale-level InfiniteDescent predicate. We also formalize tool-facing sufficient criteria, prove their soundness, and certify incompleteness where appropriate via verified counterexamples. Along the way we contribute reusable Isabelle lemmas for ω-regular reasoning over streams and for Büchi-automata constructions needed by the inclusion proofs.
Cite as
Jamie Wright, Liron Cohen, Reuben N. S. Rowe, and Andrei Popescu. Certified Infinite Descent Criteria in Isabelle/HOL. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{wright_et_al:LIPIcs.ITP.2026.14,
author = {Wright, Jamie and Cohen, Liron and Rowe, Reuben N. S. and Popescu, Andrei},
title = {{Certified Infinite Descent Criteria in Isabelle/HOL}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {14:1--14:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.14},
URN = {urn:nbn:de:0030-drops-269882},
doi = {10.4230/LIPIcs.ITP.2026.14},
annote = {Keywords: Cyclic Proof, Infinite Descent, Size-Change termination, B\"{u}chi automata}
}
Document
Formalizing a Hoare Calculus for Choreographic Programming
Abstract
Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Choreographies formalize the way many practitioners think about distributed protocols, and are a natural framework in which to prove properties of such protocols.
Previous work has introduced a Hoare calculus for reasoning about choreographies. In this article, we show how a formalization of that work in a theorem prover revealed several issues with the pen-and-paper development. We discuss the extent to which these issues can be fixed, and conclude with some considerations on the need for more formal verification of research results.
Cite as
Luís Cruz-Filipe and Thomas Wulff Heissel. Formalizing a Hoare Calculus for Choreographic Programming. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2026.15,
author = {Cruz-Filipe, Lu{\'\i}s and Heissel, Thomas Wulff},
title = {{Formalizing a Hoare Calculus for Choreographic Programming}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {15:1--15:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.15},
URN = {urn:nbn:de:0030-drops-269896},
doi = {10.4230/LIPIcs.ITP.2026.15},
annote = {Keywords: choreographic programming, theorem proving, Hoare calculus}
}
Document
Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees
Abstract
Verifying existing software is hard: Programs are developed in languages not amenable to verification, involve complicated optimizations that obscure the underlying logic, and are gigantic in size. In this paper, we propose a way to ease this pain via a simplification framework that employs interaction trees as a language-agnostic interface. We show that local variable lifting, the technique underlying AutoCorres for the Simpl language, can be generalized to interaction trees via an implementation in Rocq. A key challenge with simplifying interaction trees is that they are highly dynamic structures and we would like our approach to work with mostly uninterpreted trees. We address this challenge via metaprogramming. Our metaprogramming framework is semi-automatic and proof-guided, i.e.ie we obtain the simplified code via a constructive proof of equivalence that can be automated via proof tactics, by utilizing Rocq’s Derive extension. This approach gives us simplified code and the equivalence theorem in one step. We demonstrate that our approach is practical using examples inspired by real-world applications.
Cite as
Yiming Lin, Ian Kariniemi, and Yao Li. Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lin_et_al:LIPIcs.ITP.2026.16,
author = {Lin, Yiming and Kariniemi, Ian and Li, Yao},
title = {{Don't Sweat Interaction Trees: Proof-Guided Local Variable Lifting for Interaction Trees}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {16:1--16:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.16},
URN = {urn:nbn:de:0030-drops-269903},
doi = {10.4230/LIPIcs.ITP.2026.16},
annote = {Keywords: interaction trees, formal verification, metaprogramming}
}
Document
Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages
Abstract
We benchmark four proof assistants (Agda, Idris 2, Lean 4 and Rocq) through a single test suite. We focus our benchmarks on the basic features that all systems based on a similar foundations (dependent type theory) have in common. We do this by creating an "over language" in which to express all the information we need to be able to output correct and idiomatic syntax for each of our targets. Our benchmarks further focus on "basic engineering" of these systems: how do they handle long identifiers, long lines, large records, large data declarations, and so on.
Our benchmarks reveals both flaws and successes in all systems. We give a thorough analysis of the results.
We also detail the design of our extensible system. It is designed so that additional tests and additional system versions can easily be added. A side effect of this work is a better understanding of the common abstract syntactic structures of all four systems.
Cite as
Reed Mullanix and Jacques Carette. Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mullanix_et_al:LIPIcs.ITP.2026.17,
author = {Mullanix, Reed and Carette, Jacques},
title = {{Panbench: A Comparative Benchmarking Tool for Dependently-Typed Languages}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {17:1--17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.17},
URN = {urn:nbn:de:0030-drops-269915},
doi = {10.4230/LIPIcs.ITP.2026.17},
annote = {Keywords: Benchmarking, dependent types, testing}
}
Document
Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
Abstract
In Isabelle/HOL, declarative proofs written in the Isar language are widely appreciated for their readability and robustness. However, some users may prefer writing procedural "apply-style" proofs since they enable rapid exploration of the search space. To get the best of both worlds, we introduce Apply2Isar, a tool for Isabelle/HOL that automatically converts apply-style proofs to declarative Isar. This allows users to write complex, possibly fragile apply-style proofs, and then automatically convert them to more readable and robust declarative Isar proofs. To demonstrate the efficacy of Apply2Isar in practice, we evaluate it on a large benchmark set consisting of apply-style proofs from the Isabelle Archive of Formal Proofs.
Cite as
Sage Binder, Hanna Lachnitt, and Katherine Kosaian. Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{binder_et_al:LIPIcs.ITP.2026.18,
author = {Binder, Sage and Lachnitt, Hanna and Kosaian, Katherine},
title = {{Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {18:1--18:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.18},
URN = {urn:nbn:de:0030-drops-269925},
doi = {10.4230/LIPIcs.ITP.2026.18},
annote = {Keywords: Proof Assistants, Isabelle/HOL, Isabelle/ML, Isabelle/Isar, Proof Refactoring}
}
Document
Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean
Abstract
We present a formalization of combinatorial design theory in Lean 4, with a focus on balanced incomplete block designs (BIBDs) and their algebraic properties. The flagship result is the Bruck-Ryser-Chowla theorem, which gives the best known necessary conditions for the existence of a symmetric BIBD, formalized here in a proof assistant for the first time. Reaching this result required us to develop substantial infrastructure beyond combinatorics: we formalize Witt’s cancellation theorem for quadratic forms, prove new results on matrix congruence and block matrices, and extend Mathlib’s linear algebra library in several directions. We also provide the first formalization of Fisher’s inequality in Lean and the first formalization of the Kramer-Mesner theorem in any proof assistant, along with a reusable double-counting argument that supports standard combinatorial reasoning. The cross-domain nature of these contributions reflects a distinctive feature of design theory itself: it draws on and feeds back into many areas of mathematics, making it a particularly rewarding target for formalization within a large-scale library like Mathlib.
Cite as
Eric Jonathan Wang and Elif Uskuplu. Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{wang_et_al:LIPIcs.ITP.2026.19,
author = {Wang, Eric Jonathan and Uskuplu, Elif},
title = {{Formalizing the Bruck-Ryser-Chowla Theorem: Combinatorial Design Theory in Lean}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {19:1--19:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.19},
URN = {urn:nbn:de:0030-drops-269936},
doi = {10.4230/LIPIcs.ITP.2026.19},
annote = {Keywords: Lean theorem prover, combinatorial design theory, BIBD, matrix theory, Bruck-Ryser-Chowla theorem, quadratic forms}
}
Document
Completing Almost Fair Simulations
Abstract
The paper Almost Fair Simulations recently introduced a collection of deductive systems for interactive proofs of language inclusion between Büchi automata. These deductive systems enable intuitive proofs via cyclic reasoning principles, but are unfortunately incomplete for fair similarity, a standard notion of refinement for Büchi automata. In this paper, we address this shortcoming by presenting a new deductive system for language inclusion of Büchi automata that preserves the simplicity of Almost Fair Simulations, with the additional benefit of being complete for fair similarity. We mechanized the soundness and the completeness proofs of our new system in the Rocq proof assistant. The proofs rely on a new technique we call nested parameterized coinduction, an adaptation of Hur’s et al. parameterized coinduction for the difficult case of proofs by coinduction-induction-coinduction.
Cite as
Arthur Correnson, Iona Kuhn, and Bernd Finkbeiner. Completing Almost Fair Simulations. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{correnson_et_al:LIPIcs.ITP.2026.20,
author = {Correnson, Arthur and Kuhn, Iona and Finkbeiner, Bernd},
title = {{Completing Almost Fair Simulations}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {20:1--20:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.20},
URN = {urn:nbn:de:0030-drops-269944},
doi = {10.4230/LIPIcs.ITP.2026.20},
annote = {Keywords: Fair Simulation, Deductive Systems, Interactive Proof Assistants, Coinduction, Language Containment}
}
Document
Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean
Abstract
The theory of simplicial complexes is a cornerstone of topology, offering a sophisticated tool for computing invariants. We present a formalization of abstract simplicial complexes and stellar subdivisions in the Lean proof assistant. We adopt a purely combinatorial framework in order to provide a cohesive foundation for studying the theory of stellar subdivisions as seen in many contexts of combinatorial topology. In particular, we provide formalizations of morphisms between abstract simplicial complexes; several crucial constructions and operations on complexes, such as links and joins; and perform a comprehensive study of how stellar subdivisions interact with these operations. We state and prove a number of identities commonly used in the study of triangulated manifolds, such as deriving equivalences between links in an abstract simplicial complex K and in a stellar subdivision σ_s K, including results with no references in the standard literature. To our knowledge, this is the first formalization of stellar subdivisions in any proof assistant.
Cite as
Garett Cunningham, Daniel Zach, and Stefan Friedl. Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 21:1-21:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{cunningham_et_al:LIPIcs.ITP.2026.21,
author = {Cunningham, Garett and Zach, Daniel and Friedl, Stefan},
title = {{Formalizing Abstract Simplicial Complexes \& Stellar Subdivisions in Lean}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {21:1--21:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.21},
URN = {urn:nbn:de:0030-drops-269956},
doi = {10.4230/LIPIcs.ITP.2026.21},
annote = {Keywords: Lean, mathlib, simplicial complex, stellar subdivision, combinatorial topology}
}
Document
Feedback & Synthesis in LLM-Assisted Termination Proofs
Abstract
Termination - proving there are no inputs on which a function runs forever - is one of the most fundamental problems in software verification, and competitions comparing termination analysis tools have run for over twenty years. We integrate two state-of-the-art, open-weight LLMs with a theorem prover’s built-in automation to generate termination proofs, solving 39% more problems than the best LLM alone and more than tripling the number solved by the built-in analysis on our benchmark. This is the first, to our knowledge, integration of an LLM with a termination-analysis algorithm, and is generalizable to any theorem prover based on a functional language. Our design is informed by nine ablations considering what theorem-prover feedback helps the LLM and four experiments on how the model decomposes problems.
Cite as
Zeke Medley and Panagiotis Manolios. Feedback & Synthesis in LLM-Assisted Termination Proofs. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{medley_et_al:LIPIcs.ITP.2026.22,
author = {Medley, Zeke and Manolios, Panagiotis},
title = {{Feedback \& Synthesis in LLM-Assisted Termination Proofs}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {22:1--22:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.22},
URN = {urn:nbn:de:0030-drops-269965},
doi = {10.4230/LIPIcs.ITP.2026.22},
annote = {Keywords: termination analysis, theorem proving, large language models, ACL2}
}
Document
From Weierstraß to Dedekind via Jacobi: Formalising Foundations of Modular Forms
Abstract
We present an Isabelle/HOL formalisation of the foundations of analytic number theory related to modular forms. We begin by refactoring and extending the existing library on elliptic functions, adding the theorem that every elliptic function can be written in terms of the Weierstraß elliptic function ℘ and the addition theorem for ℘, which links complex lattices to elliptic curves. Next, we develop an extensive library on the Jacobi theta functions, including well-known results such as the Jacobi triple product, the Pentagonal Number Theorem, and the Rogers-Ramanujan identities. Finally, we apply this library to the study of the Dedekind η function and "forbidden" Eisenstein series G₂. In all of this, we aim for short and clean proofs, building a library of reusable lemmas.
Cite as
Manuel Eberl, Wenda Li, and Lawrence C. Paulson. From Weierstraß to Dedekind via Jacobi: Formalising Foundations of Modular Forms. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{eberl_et_al:LIPIcs.ITP.2026.23,
author = {Eberl, Manuel and Li, Wenda and Paulson, Lawrence C.},
title = {{From Weierstra{\ss} to Dedekind via Jacobi: Formalising Foundations of Modular Forms}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.23},
URN = {urn:nbn:de:0030-drops-269976},
doi = {10.4230/LIPIcs.ITP.2026.23},
annote = {Keywords: Isabelle/HOL, elliptic functions, Eisenstein series, modular forms, theta functions, number theory, complex analysis, formalisation of mathematics}
}
Document
ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
Abstract
Neural approaches to theorem proving require robust infrastructure for interfacing with interactive theorem provers (ITPs), extracting structured proof data, and executing proof search at scale. However, existing tooling is often assistant-specific and oriented toward interactive, file-level execution, making repository-scale analysis and parallel experimentation challenging. We present ProofWala, a multilingual proof engineering framework built around itp-interface, a reusable library for programmatic interaction with ITPs. For Lean 4, we implement a meta-programmed interaction layer that executes inside the elaborator, enabling semantically faithful tactic-level tracing together with declaration- and dependency-level extraction across entire repositories. This design extends beyond traditional REPL-style interaction by supporting project-wide analysis, environment cloning, and pooled execution of proof states. The implementation is robust across Lean 4 versions after 4.15.0 with forward compatibility support. The same interface abstraction supports tactic execution and data extraction for multiple versions of Rocq, yielding a unified cross-assistant pipeline.
Built on this infrastructure, ProofWala provides standardized multilingual proof datasets, model training utilities, and parallel proof search algorithms. Using the framework, we demonstrate that multilingual training across Lean and Rocq enables cross-lingual and cross-domain transfer. In particular, we observe statistically significant improvements on the largest benchmark (Lean/Mathlib) and in domain adaptation (CategoryTheory), while other settings exhibit consistent but not statistically significant trends in favor of multilingual training. We open-source the full framework, including the parallel proof search module, the itp-interface library, multilingual datasets, and trained models, providing a scalable foundation for proof mining, neural theorem proving, and cross-assistant experimentation.
Cite as
Amitayush Thakur, George Tsoukalas, Greg Durrett, and Swarat Chaudhuri. ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{thakur_et_al:LIPIcs.ITP.2026.24,
author = {Thakur, Amitayush and Tsoukalas, George and Durrett, Greg and Chaudhuri, Swarat},
title = {{ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {24:1--24:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.24},
URN = {urn:nbn:de:0030-drops-269983},
doi = {10.4230/LIPIcs.ITP.2026.24},
annote = {Keywords: neural theorem proving, ITP, automated reasoning, LLM guided theorem proving, ITP framework}
}
Document
LeanArchitect: Automating Blueprint Generation for Humans and AI
Abstract
Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are central to human collaboration, existing tooling treats the informal (LaTeX) and formal (Lean) components as largely decoupled artifacts, leading to maintenance overhead and limiting integration with AI automation. We present LeanArchitect, a Lean package for extracting, managing, and exporting blueprint data directly from Lean code. LeanArchitect introduces a declarative annotation mechanism that associates formal declarations with blueprint metadata, automatically infers dependency information, and generates LaTeX blueprint content synchronized with the Lean development. This design eliminates duplication between formal and informal representations and eases fine-grained progress tracking for both human contributors and AI-based theorem provers. We demonstrate the practicality of LeanArchitect through the automated conversion of several large existing blueprint-driven projects, and through a human-AI collaboration case study formalizing a multivariate Taylor theorem. Our results show that LeanArchitect improves maintainability, exposes latent inconsistencies in existing blueprints, and provides an effective interface for integrating AI tools into real-world formalization workflows.
Cite as
Thomas Zhu, Pietro Monticone, Sean Welleck, and Jeremy Avigad. LeanArchitect: Automating Blueprint Generation for Humans and AI. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{zhu_et_al:LIPIcs.ITP.2026.25,
author = {Zhu, Thomas and Monticone, Pietro and Welleck, Sean and Avigad, Jeremy},
title = {{LeanArchitect: Automating Blueprint Generation for Humans and AI}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {25:1--25:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.25},
URN = {urn:nbn:de:0030-drops-269992},
doi = {10.4230/LIPIcs.ITP.2026.25},
annote = {Keywords: Lean theorem prover, interactive theorem proving, proof assistants, formal methods, human-computer interface, software development tools}
}
Document
An End-To-End Verification of Keller’s Conjecture
Abstract
In 1930, Keller conjectured that every gap-free tiling of ℝⁿ by n-dimensional unit cubes must contain cubes that fully share an (n - 1)-dimensional face. Keller’s conjecture holds for n ≤ 7 and fails for n ≥ 8. The final case, n = 7, was settled in 2020 using a mix of traditional and automated reasoning. The result was obtained by reducing the conjecture to a set of clique-existence problems, encoding those problems into propositional logic, breaking symmetries, and solving them with a SAT solver.
In this paper, we present an end-to-end verification in Lean 4 of Keller’s conjecture for all dimensions. First, we simplify a prior reduction of Keller’s conjecture to the clique-existence problems. We then verify an improved SAT encoding of those problems, as well as some symmetry reasoning on the encoding. Throughout our work, we sought to maximize the synergy between interactive and automated techniques while minimizing human proof burden. In particular, the symmetry reasoning was split between Lean and a mechanically-checkable proof system, since neither was suitable on their own for verifying all of the symmetry reasoning. We discuss how and why we chose to split the reasoning across these systems based on their relative strengths and weaknesses.
Cite as
James Gallicchio, Cayden Codel, Jeremy Avigad, and Marijn J. H. Heule. An End-To-End Verification of Keller’s Conjecture. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{gallicchio_et_al:LIPIcs.ITP.2026.26,
author = {Gallicchio, James and Codel, Cayden and Avigad, Jeremy and Heule, Marijn J. H.},
title = {{An End-To-End Verification of Keller’s Conjecture}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {26:1--26:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.26},
URN = {urn:nbn:de:0030-drops-270008},
doi = {10.4230/LIPIcs.ITP.2026.26},
annote = {Keywords: Keller’s conjecture, the Lean theorem prover, SAT encodings, SAT solving, Trestle, formal verification}
}
Document
Fractional Separation Logic in Isabelle LLVM
Abstract
We present a shallow embedding of fractional separation logic in Isabelle/HOL, based on fractional separation algebras with unbounded fractions. To support flexible ownership splitting and recombination, we use nominal labels that enable systematic distribution and collection of fractional permissions across separating conjunctions.
The logic is integrated into a verification condition generator that automates substantial parts of fraction arithmetic and label reasoning, significantly reducing manual proof effort. As a backend, we connect the framework to Isabelle LLVM, enabling the verification of executable LLVM code.
As a case study, we verify a parallel matrix-vector multiplication. The example illustrates recursive reasoning, parallel writes to disjoint segments of the result vector, and shared read access to the input vector via fractional permissions.
Cite as
Peter Lammich. Fractional Separation Logic in Isabelle LLVM. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lammich:LIPIcs.ITP.2026.27,
author = {Lammich, Peter},
title = {{Fractional Separation Logic in Isabelle LLVM}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {27:1--27:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.27},
URN = {urn:nbn:de:0030-drops-270016},
doi = {10.4230/LIPIcs.ITP.2026.27},
annote = {Keywords: Fractional Separation Logic, LLVM, verification, Isabelle}
}
Document
String Diagrams for Monoidal Categories, in Rocq
Abstract
We present a Rocq library for monoidal categories, including a decision procedure for proving equality of morphisms as well as notations that make it possible to reason as if these monoidal categories were strict, inferring MacLane isomorphims automatically in the background. Together with an external tool for visualising and editing string diagrams, this make it possible to perform rewriting steps graphically, and to translate them into textual formal proofs which are concise and readable.
Cite as
Damien Pous. String Diagrams for Monoidal Categories, in Rocq. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{pous:LIPIcs.ITP.2026.28,
author = {Pous, Damien},
title = {{String Diagrams for Monoidal Categories, in Rocq}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {28:1--28:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.28},
URN = {urn:nbn:de:0030-drops-270029},
doi = {10.4230/LIPIcs.ITP.2026.28},
annote = {Keywords: Monoidal categories, string diagrams, formal proofs, graphical proofs, Rocq}
}
Document
Securing the Foundations of an Intermediate Language for Probabilistic Program Verification
Abstract
Schröer et al. [Philipp Schröer et al., 2023] developed a verification infrastructure for rapid prototyping of automated verification techniques for probabilistic programs (PPs), which is based on the quantitative intermediate verification language HeyVL. In a nutshell, users encode programs, specifications, and proof rules into a single HeyVL program. The verification conditions obtained from such a HeyVL program are then discharged with SMT solvers or probabilistic model checkers. However, ensuring that a HeyVL encoding is correct can be subtle and error-prone, just like reasoning about PPs in general.
In this paper, we develop mechanized foundations for writing formal correctness proofs for both HeyVL encodings and PP verification techniques that are grounded in the basics of probability theory. To this end, we formalize Markov decision processes (MDPs) - a standard model for assigning operational semantics to PPs. We construct suitable probability spaces for MDPs to ground them in probability theory. Furthermore, we develop least fixed-point characterizations of expected total costs of MDPs, which are useful for relating program logics or denotational semantics to an operational MDP semantics. We apply these characterizations to formalize sound weakest-precondition-style calculi for both partial and total correctness reasoning about the expected behavior of PPs with unbounded loops, nondeterminism, and conditioning. Finally, we develop a deep embedding of the HeyVL intermediate verification language. We apply the above machinery to prove the correctness of various existing HeyVL encodings. During that process, we improved the original HeyVL encoding of an invariant-based proof rule for loops.
All of our results have been formalized in the interactive theorem prover Lean on top of mathlib.
Cite as
Oliver Bøving and Christoph Matheja. Securing the Foundations of an Intermediate Language for Probabilistic Program Verification. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{boving_et_al:LIPIcs.ITP.2026.29,
author = {B{\o}ving, Oliver and Matheja, Christoph},
title = {{Securing the Foundations of an Intermediate Language for Probabilistic Program Verification}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {29:1--29:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.29},
URN = {urn:nbn:de:0030-drops-270035},
doi = {10.4230/LIPIcs.ITP.2026.29},
annote = {Keywords: Verification, Markov decision processes, probabilistic programs, Lean}
}
Document
Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation
Abstract
Craig’s Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the sequent calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed λ-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of Čubrić’s proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.
Cite as
Meven Lennon-Bertrand and Alexis Saurin. Bidirectional Interpolation for the λ-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{lennonbertrand_et_al:LIPIcs.ITP.2026.30,
author = {Lennon-Bertrand, Meven and Saurin, Alexis},
title = {{Bidirectional Interpolation for the \lambda-Calculus: Revisiting and Formalising Craig-\v{C}ubri\'{c} Interpolation}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {30:1--30:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.30},
URN = {urn:nbn:de:0030-drops-270049},
doi = {10.4230/LIPIcs.ITP.2026.30},
annote = {Keywords: Craig Interpolation, Bidirectional Typing, Typed Lambda Calculus}
}
Document
Short Paper
130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper)
Abstract
This is a brief description of a project that has already autoformalized a large portion of the general topology from the Munkres textbook (which has in total 241 pages in 7 chapters and 39 sections). The project has been running since November 21, 2025 and has as of January 4, 2026, produced 160k lines of formalized topology. Most of it (about 130k lines) have been done in two weeks, from December 22 to January 4, for an LLM subscription cost of about $100. This includes a 3k-line proof of Urysohn’s lemma, a 2k-line proof of Urysohn’s Metrization theorem, over 10k-line proof of the Tietze extension theorem, and many more (in total over 1.5k lemmas/theorems).
The approach is quite simple and cheap: build a long-running feedback loop between an LLM and a reasonably fast proof checker equipped with a core foundational library. The LLM is now instantiated as ChatGPT (mostly 5.2) or Claude Sonnet (4.5) run through the respective Codex or Claude Code command line interfaces. The proof checker is Chad Brown’s higher-order set theory system Megalodon, and the core library is Brown’s formalization of basic set theory and surreal numbers (including reals, etc). The rest is some prompt engineering and technical choices which we describe here. Based on the fast progress, low cost, virtually unknown ITP/library, and the simple setup available to everyone, we believe that (auto)formalization may become quite easy and ubiquitous in 2026, regardless of which proof assistant is used.
Cite as
Josef Urban. 130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone? (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 31:1-31:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{urban:LIPIcs.ITP.2026.31,
author = {Urban, Josef},
title = {{130k Lines of Formal Topology in Two Weeks: Simple and Cheap Autoformalization for Everyone?}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {31:1--31:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.31},
URN = {urn:nbn:de:0030-drops-270052},
doi = {10.4230/LIPIcs.ITP.2026.31},
annote = {Keywords: Autoformalization, Automated reasoning, Interactive theorem proving, Formal proof assistants, Machine learning, Language Models}
}
Document
Short Paper
Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper)
Abstract
Real root isolation is a fundamental subroutine in computer algebra, with applications ranging from algebraic number arithmetic to solving polynomial systems. Modern implementations typically employ subdivision methods based on root counting via Descartes' rule of signs. In contrast, most existing formally verified root isolation procedures rely on Sturm's theorem for root counting, leading to a noticeable gap between practical implementations and formally verified approaches.
We take an initial step towards efficient verified real root isolation by formally verifying two simple algorithms based on Descartes' rule of signs: a classical bisection procedure and a Newton-accelerated variant. In this paper, we describe the algorithms, present formal proofs of termination, soundness, and completeness, and discuss our code-generation efforts. Brief experiments show promising performance improvements over existing formally verified algorithms in Isabelle/HOL.
Cite as
Aeacus Sheng, Wenda Li, and Paul B. Jackson. Faster Verified Real Root Isolation with Descartes' Rule of Signs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 32:1-32:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{sheng_et_al:LIPIcs.ITP.2026.32,
author = {Sheng, Aeacus and Li, Wenda and Jackson, Paul B.},
title = {{Faster Verified Real Root Isolation with Descartes' Rule of Signs}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {32:1--32:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.32},
URN = {urn:nbn:de:0030-drops-270068},
doi = {10.4230/LIPIcs.ITP.2026.32},
annote = {Keywords: Isabelle/HOL, Real root isolation, Descartes' rule of signs}
}
Document
Short Paper
Formal Primal-Dual Algorithm Analysis (Short Paper)
Abstract
We present an ongoing effort to build a framework and a library in Isabelle/HOL for formalising primal-dual arguments for the analysis of algorithms. We discuss a number of example formalisations from the theory of matching algorithms, covering classical algorithms like the Hungarian Method, widely considered the first primal-dual algorithm, and modern algorithms like the AdWords algorithm, which models the assignment of search queries to advertisers in the context of search engines.
Cite as
Mohammad Abdulaziz, Thomas Ammer, and Christoph Madlener. Formal Primal-Dual Algorithm Analysis (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 33:1-33:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2026.33,
author = {Abdulaziz, Mohammad and Ammer, Thomas and Madlener, Christoph},
title = {{Formal Primal-Dual Algorithm Analysis}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {33:1--33:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.33},
URN = {urn:nbn:de:0030-drops-270075},
doi = {10.4230/LIPIcs.ITP.2026.33},
annote = {Keywords: Bipartite Matching, Graph Algorithms, Isabelle/HOL, Formal Verification}
}
Document
Short Paper
Three Roads to de Finetti’s Theorem in Lean 4 (Short Paper)
Abstract
We present a Lean 4 formalization of the de Finetti–Ryll-Nardzewski theorem for infinite sequences of random variables on standard Borel spaces, establishing that every exchangeable sequence is conditionally i.i.d. The development closely follows Kallenberg’s modern treatment of probabilistic symmetries and formalizes three distinct proofs of the key implication, with the second and third formalized for real-valued square-integrable sequences: (i) a reverse‑martingale argument due to Aldous, (ii) an elementary L² approach based on contractability bounds and Cesàro convergence, and (iii) an ergodic‑theoretic proof via the Koopman operator and the mean ergodic theorem. The library contains over 42,000 lines of code and was completed in three months with extensive use of Claude and GPT models, together with a reusable Lean proof-engineering skill for agentic coding systems developed during the project. The three proofs share a uniform common ending, so each route had to produce the same finite conditional-factorization interface before the final conclusion. This provided a cross-check on these independent routes during AI-assisted development.
Cite as
Cameron Freer. Three Roads to de Finetti’s Theorem in Lean 4 (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 34:1-34:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{freer:LIPIcs.ITP.2026.34,
author = {Freer, Cameron},
title = {{Three Roads to de Finetti’s Theorem in Lean 4}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {34:1--34:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.34},
URN = {urn:nbn:de:0030-drops-270086},
doi = {10.4230/LIPIcs.ITP.2026.34},
annote = {Keywords: exchangeability, de Finetti’s theorem, Lean 4, formalized mathematics, AI-assisted formalization}
}
Document
Short Paper
A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper)
Abstract
This paper introduces the algebra normalizing tactic for the Lean theorem prover. This tactic expands on the existing ring tactic by additionally supporting a scalar multiplication action over a fixed commutative (semi)ring. It supports rational constants in the base ring even when the main ring is not a field, which lets us implement a suite of tactics for manipulating both univariate and multivariate polynomials. These features are implemented by adapting the existing implementation of ring while retaining support for variable exponents.
Cite as
Arend Mellendijk. A Lean Tactic for Normalizing Expressions in an Algebra over a Ring (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 35:1-35:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{mellendijk:LIPIcs.ITP.2026.35,
author = {Mellendijk, Arend},
title = {{A Lean Tactic for Normalizing Expressions in an Algebra over a Ring}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {35:1--35:8},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.35},
URN = {urn:nbn:de:0030-drops-270099},
doi = {10.4230/LIPIcs.ITP.2026.35},
annote = {Keywords: Lean, Mathlib, algebraic structures, proof algorithms}
}
Document
Short Paper
Lean on Vampire Proofs (Short Paper)
Abstract
Vampire proves theorems completely automatically in first- and higher-order logic extended with theories. Proof checking is increasingly demanded to consolidate user trust in Vampire’s output. We describe ongoing efforts in reconstructing Vampire proofs as trusted proofs in Lean. Our experiments showcase feasibility of generating trusted Vampire proofs that are validated in Lean.
Cite as
Jonas Bodingbauer, Márton Hajdu, Laura Kovács, Axel Polaczek, and Michael Rawson. Lean on Vampire Proofs (Short Paper). In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 36:1-36:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)
Copy BibTex To Clipboard
@InProceedings{bodingbauer_et_al:LIPIcs.ITP.2026.36,
author = {Bodingbauer, Jonas and Hajdu, M\'{a}rton and Kov\'{a}cs, Laura and Polaczek, Axel and Rawson, Michael},
title = {{Lean on Vampire Proofs}},
booktitle = {17th International Conference on Interactive Theorem Proving (ITP 2026)},
pages = {36:1--36:9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-436-9},
ISSN = {1868-8969},
year = {2026},
volume = {382},
editor = {Komendantskaya, Ekaterina and Nipkow, Tobias},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.36},
URN = {urn:nbn:de:0030-drops-270102},
doi = {10.4230/LIPIcs.ITP.2026.36},
annote = {Keywords: Automated Reasoning, Interactive Theorem Provers, Automated Theorem Provers, Lean, Vampire, Proof Reconstruction}
}