| 2022 | Formal verification of a distributed dynamic reconfiguration protocol. | William Schultz, Ian Dardik, Stavros Tripakis |
| 2022 | On homotopy of walks and spherical maps in homotopy type theory. | Jonathan Prieto-Cubides |
| 2022 | Formalising lie algebras. | Oliver Nash |
| 2022 | Structural embeddings revisited (invited talk). | Csar Muoz |
| 2022 | Specification and verification of a transient stack. | Alexandre Moine, Arthur Charguraud, Franois Pottier |
| 2022 | An extension of the framework types-to-sets for Isabelle/HOL. | Mihails Milehins |
| 2022 | Undecidability, incompleteness, and completeness of second-order logic in Coq. | Mark Koch, Dominik Kirst |
| 2022 | A machine-checked direct proof of the Steiner-lehmus theorem. | Ariel Kellison |
| 2022 | CertiStr: a certified string solver. | Shuanglong Kan, Anthony Widjaja Lin, Philipp Rmmer, Micha Schrader |
| 2022 | (Deep) induction rules for GADTs. | Patricia Johann, Enrico Ghiorzi |
| 2022 | Semantic cut elimination for the logic of bunched implications, formalized in Coq. | Dan Frumin |
| 2022 | Reflection, rewinding, and coin-toss in EasyCrypt. | Denis Firsov, Dominique Unruh |
| 2022 | Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting. | Michael Frber |
| 2022 | Verbatim++: verified, optimized, and semantically rich lexing with derivatives. | Derek Egolf, Sam Lasser, Kathleen Fisher |
| 2022 | A drag-and-drop proof tactic. | Pablo Donato, Pierre-Yves Strub, Benjamin Werner |
| 2022 | A compositional proof framework for FRETish requirements. | Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle |
| 2022 | Overcoming restraint: composing verification of foreign functions with cogent. | Louis Cheung, Liam O'Connor, Christine Rizkallah |
| 2022 | Windmills of the minds: an algorithm for fermat's two squares theorem. | Hing-Lun Chan |
| 2022 | Applying formal verification to microkernel IPC at meta. | Quentin Carbonneaux, Noam Zilberstein, Christoph Klee, Peter W. O'Hearn, Francesco Zappa Nardelli |
| 2022 | A verified algebraic representation of cairo program execution. | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
| 2022 | Coq's vibrant ecosystem for verification engineering (invited talk). | Andrew W. Appel |
| 2022 | The sel4 verification: the art and craft of proof and the reality of commercial support (invited talk). | June Andronick |
| 2022 | Certified abstract machines for skeletal semantics. | Guillaume Ambal, Sergue Lenglet, Alan Schmitt |
| 2022 | Implementing a category-theoretic framework for typed abstract syntax. | Benedikt Ahrens, Ralph Matthes, Anders Mrtberg |
| 2021 | Contextual refinement of the Michael-Scott queue (proof pearl). | Simon Friis Vindum, Lars Birkedal |