| 2026 | An End-To-End Verification of Keller's Conjecture. | James Gallicchio, Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2026 | Three Roads to de Finetti's Theorem in Lean 4 (Short Paper). | Cameron E. Freer |
| 2026 | From Weierstra to Dedekind via Jacobi: Formalising Foundations of Modular Forms. | Manuel Eberl, Wenda Li, Lawrence C. Paulson |
| 2026 | Formalizing Abstract Simplicial Complexes & Stellar Subdivisions in Lean. | Garett Cunningham, Daniel Zach, Stefan Friedl |
| 2026 | Formalizing a Hoare Calculus for Choreographic Programming. | Lus Cruz-Filipe, Thomas Wulff Heissel |
| 2026 | Completing Almost Fair Simulations. | Arthur Correnson, Iona Kuhn, Bernd Finkbeiner |
| 2026 | Securing the Foundations of an Intermediate Language for Probabilistic Program Verification. | Oliver Bving, Christoph Matheja |
| 2026 | Lean on Vampire Proofs (Short Paper). | Jonas Bodingbauer, Mrton Hajd, Laura Kovcs, Axel Polaczek, Michael Rawson |
| 2026 | Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar. | Sage Binder, Hanna Lachnitt, Katherine Kosaian |
| 2026 | Nitro Isolation Engine: Formally Verifying a Production Hypervisor (Invited Talk). | Hanno Becker, Nathan Chong, Robert Dockins, Jim Grundy, Jason Z. S. Hu, Ike Mulder, Dominic P. Mulligan, Paul Mure, Bryan Parno, Lawrence C. Paulson, Konrad Slind |
| 2026 | Certified Intersection of Commutative Regular Expressions as Solutions of Systems of Linear Diophantine Equations. | Ricardo Almeida, Blair Archibald, Basile Pesin, Michele Sevegnani |
| 2026 | Formal Primal-Dual Algorithm Analysis (Short Paper). | Mohammad Abdulaziz, Thomas Ammer, Christoph Madlener |
| 2025 | Finiteness of Symbolic Derivatives in Lean. | Ekaterina Zhuchko, Hendrik Maarand, Margus Veanes, Gabriel Ebner |
| 2025 | Front Matter, Table of Contents, Preface, Conference Organization. | |
| 2025 | Algebra Is Half the Battle: Verifying Presentations of Graded Unipotent Chevalley Groups. | Eric Wang, Arohee Bhoja, Cayden R. Codel, Noah G. Singer |
| 2025 | LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean (Short Paper). | Eric Vin, Kyle A. Miller, Daniel J. Fremont |
| 2025 | Taming Floating-Point Rounding Errors with Proofs (Invited Talk). | Laura Titolo |
| 2025 | Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs. | Jrmy Thibault, Joseph Lenormand, Catalin Hritcu |
| 2025 | Verifying Datalog Reasoning with Lean. | Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krtzsch |
| 2025 | Autosubst: On Mechanising Binders in a General-Purpose Proof Assistant (Invited Talk). | Kathrin Stark |
| 2025 | Nondeterministic Asynchronous Dataflow in Isabelle/HOL. | Rafael Castro Gonalves Silva, Laouen Fernet, Dmitriy Traytel |
| 2025 | Formalising New Mathematics in Isabelle: Diagonal Ramsey. | Lawrence C. Paulson |
| 2025 | Canonical for Automated Theorem Proving in Lean. | Chase Norman, Jeremy Avigad |
| 2025 | GOL in GOL in HOL: Verified Circuits in Conway's Game of Life. | Magnus O. Myreen, Mario Carneiro |
| 2025 | Certified Implementability of Global Multiparty Protocols. | Elaine Li, Thomas Wies |