| 1 | -- | 8 | Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu 0001, Gregor Snelting. Introduction to Milestones in Interactive Theorem Proving |
| 9 | -- | 32 | Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar |
| 33 | -- | 71 | Yves Bertot, Laurence Rideau, Laurent Théry. Distant Decimals of π : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation |
| 73 | -- | 111 | Fabian Immler. A Verified ODE Solver and the Lorenz Attractor |
| 113 | -- | 139 | Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu 0001, Franco Raimondi. CoSMed: A Confidentiality-Verified Social Media Platform |
| 141 | -- | 189 | Hao Chen, Xiongnan (Newman) Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu. Toward Compositional Verification of Interruptible OS Kernels and Device Drivers |
| 191 | -- | 242 | Cornelius Diekmann, Lars Hupel, Julius Michaelis, Maximilian P. L. Haslbeck, Georg Carle. Verified iptables Firewall Analysis and Verification |
| 243 | -- | 332 | Andreas Lochbihler. Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler |
| 333 | -- | 365 | Jasmin Christian Blanchette, Mathias Fleury, Peter Lammich, Christoph Weidenbach. A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality |
| 367 | -- | 422 | Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, Andrew W. Appel. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs |
| 423 | -- | 453 | Lukasz Czajka 0001, Cezary Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory |
| 455 | -- | 484 | Anders Schlichtkrull. Formalization of the Resolution Calculus for First-Order Logic |
| 485 | -- | 520 | Mohammad Abdulaziz, Michael Norrish, Charles Gretton. Formally Verified Algorithms for Upper-Bounding State Space Diameters |
| 521 | -- | 553 | Christian Doczkal, Gert Smolka. Regular Language Representations in the Constructive Type Theory of Coq |