| 2025 | Scott's Representation Theorem and the Univalent Karoubi Envelope. | Arnoud van der Leer, Kobe Wullaert, Benedikt Ahrens |
| 2025 | Barendregt's Theory of the λ-Calculus, Refreshed and Formalized. | Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs |
| 2025 | Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. | Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jrg Schurr, Clark W. Barrett, Cesare Tinelli |
| 2025 | Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic. | Robbert Krebbers, Luko van der Maas, Enrico Tassi |
| 2025 | A Natural Language Formalization of Perfectoid Rings in ℕaproche. | Peter Koepke |
| 2025 | On Verifying Secret Control Flow Elimination. | David Knothe, Oliver Bringmann |
| 2025 | Verification of the CVM Algorithm with a Functional Probabilistic Invariant. | Emin Karayel, Seng Joe Watt, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan |
| 2025 | Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper). | Nadeem Abdul Hamid |
| 2025 | Automatically Generalizing Proofs and Statements. | Anshula Gandhi, Anand Rao Tadipatri, Timothy Gowers |
| 2025 | Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness la Fitting. | Asta Halkjr From, Anders Schlichtkrull |
| 2025 | Formalising Subject Reduction and Progress for Multiparty Session Processes. | Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida |
| 2025 | Verifying an Efficient Algorithm for Computing Bernoulli Numbers. | Manuel Eberl, Peter Lammich |
| 2025 | A Certified Proof Checker for Deep Neural Network Verification in Imandra. | Remi Desmartin, Omri Isac, Grant O. Passmore, Ekaterina Komendantskaya, Kathrin Stark, Guy Katz |
| 2025 | Sledgehammering Without ATPs (Short Paper). | Martin Desharnais, Jasmin Blanchette |
| 2025 | Formalising Inductive and Coinductive Containers. | Stefania Damato, Thorsten Altenkirch, Axel Ljungstrm |
| 2025 | A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. | Joshua M. Cohen |
| 2025 | A Verified Cost Model for Call-By-Push-Value. | Zhuo Zoey Chen, Johannes man Pohjola, Christine Rizkallah |
| 2025 | A Formalization of Divided Powers in Lean. | Antoine Chambert-Loir, Mara Ins de Frutos-Fernndez |
| 2025 | Program Optimisations via Hylomorphisms for Extraction of Executable Code. | David Castro-Perez, Marco Paviotti, Michael Vollmer |
| 2025 | Formalizing Colimits in 𝒞at. | Mario Carneiro, Emily Riehl |
| 2025 | Animating MRBNFs: Truly Modular Binding-Aware Datatypes in Isabelle/HOL. | Jan van Brgge, Andrei Popescu, Dmitriy Traytel |
| 2025 | Formalizing the Hidden Number Problem in Isabelle/HOL. | Sage Binder, Eric Ren, Katherine Kosaian |
| 2025 | Formally Verifying a Vertical Cell Decomposition Algorithm. | Yves Bertot, Thomas Portet |
| 2025 | Formalizing Splitting in Isabelle/HOL. | Ghilain Bergeron, Florent Krasnopol, Sophie Tourret |
| 2025 | A Formal Proof of Complexity Bounds on Diophantine Equations. | Jonas Bayer, Marco David |