| 2026 | Cylindrical Algebraic Decomposition in Coq/Rocq. | Quentin Vermande |
| 2026 | Enhancing Symbolic Execution with Machine-Checked Safety Proofs. | David Trabish, Shachar Itzhaky |
| 2026 | Adding Sorts to an Isabelle Formalization of Superposition. | Balzs Tth, Martin Desharnais-Schfer, Jasmin Blanchette |
| 2026 | Foundational Verification of Running-Time Bounds for Interactive Programs. | Andy Tockman, Pratap Singh, Andres Erbsen, Samuel Gruetter, Adam Chlipala |
| 2026 | Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq. | Holger Thies |
| 2026 | Verified VCG and Verified Compiler for Dafny. | Daniel Nezamabadi, Magnus O. Myreen, Yong Kiam Tan |
| 2026 | A Certifying Proof Assistant for Synthetic Mathematics in Lean. | Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey |
| 2026 | Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions. | Tomaz Mascarenhas, Harun Khan, Abdalrhman Mohamed, Andrew Reynolds, Haniel Barbosa, Clark W. Barrett, Cesare Tinelli |
| 2026 | Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic. | Virgil Marionneau, Flix Sassus Bourda, Alejandro Aguirre, Lars Birkedal |
| 2026 | Mechanizing Synthetic Tait Computability in Istari. | Runming Li, Yue Yao, Robert Harper |
| 2026 | Mechanized Dominator Tree Certification. | Jean-Christophe Lchenet |
| 2026 | Brack: A Verified Compiler for Scheme via CakeML. | Pascal Y. Lasnier, Jeremy Yallop, Magnus O. Myreen |
| 2026 | Bar Inductive Predicates for Constructive Algebra in Rocq. | Dominique Larchey-Wendling |
| 2026 | A Rose Tree Is Blooming (Proof Pearl). | Joomy Korkut |
| 2026 | Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis. | Shuanglong Kan, Anthony W. Lin |
| 2026 | Layers of Confluence for Actors. | Ludovic Henrio, Einar Broch Johnsen, smund Aqissiaq Arild Klvstad, Violet Ka I Pun, Yannick Zakowski |
| 2026 | A Lambda-Superposition Tactic for Isabelle/HOL. | Massin Guerdi |
| 2026 | Precise Reasoning about Container-Internal Pointers with Logical Pinning. | Yawen Guan, Clment Pit-Claudel |
| 2026 | Higher Order Differential Calculus in Mathlib. | Sbastien Gouzel |
| 2026 | Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust. | Arnaud Golfouse, Armal Guneau, Jacques-Henri Jourdan |
| 2026 | A Recipe for Modular Verification of Generic Tree Traversals. | Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg |
| 2026 | Certifying the Decidability of the Word Problem in Monoids at Large. | Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, Finn Smith |
| 2026 | Formalizing Polynomial Laws and the Universal Divided Power Algebra. | Antoine Chambert-Loir, Mara Ins de Frutos-Fernndez |
| 2026 | Towards Composable Proofs of Cache Coherence Protocols. | Martina Camaioni, Yann Herklotz, Tz-Ching Yu, Thomas Bourgeat |
| 2026 | Adhesive Category Theory for Graph Rewriting in Rocq. | Samuel Arsac, Russ Harmer, Damien Pous |