# Archive of Formal Proofs

The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. It is organized in the way of a scientific journal, is indexed by dblp and has an ISSN: 2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal publications. To cite an entry, please use the preferred citation style.

**
This is the development version of the archive, referring to a recent Isabelle development version.
Some entries may not be in a working state.
The main archive is available from the front page.
**

## 2024

##### Undecidability Results on Orienting Single Rewrite Rules

by René Thiemann, Fabian Mitterwallner and Aart Middeldorp

##### AutoCorres2

by Matthew Brecknell, David Greenaway, Johannes Hölzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch and Simon Wimmer

##### A Verified Proof Checker for Metric First-Order Temporal Logic

by Andrei Herasimau, Jonathan Julian Huerta y Munive, Leonardo Lima, Martin Raszyk and Dmitriy Traytel

##### Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset)

by Xavier Parent and Christoph Benzmüller

## 2023

##### HOL-CSPM - Architectural operators for HOL-CSP

by Benoît Ballenghien, Safouan Taha and Burkhart Wolff

##### Labeled Transition Systems

by Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba and Dmitriy Traytel

##### Coupled Similarity and Contrasimilarity, and How to Compute Them

by Benjamin Bisping and Luisa Montanari

##### Inner Structure, Determinism and Modal Algebra of Multirelations

by Walter Guttmann and Georg Struth

##### A Formalization of the SCL(FOL) Calculus: Simple Clause Learning for First-Order Logic

by Martin Desharnais

##### The CHSH inequality: Tsirelson's upper-bound and other results

by Mnacho Echenim, Mehdi Mhalla and Coraline Mori

##### Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties

by Thibault Dardinier

##### Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs

by Thibault Dardinier

##### No Faster-Than-Light Observers (GenRel)

by Mike Stannett, Edward Higgins, Hajnal Andreka, Judit Madarasz, István Németi and Gergely Szekely

## 2022

##### A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL

by Katherine Kosaian, Yong Kiam Tan and André Platzer

##### Automation of Boolos' Curious Inference in Isabelle/HOL

by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe

##### A Verified Translation of Multitape Turing Machines into Singletape Turing Machines

by Christian Dalvit and René Thiemann

##### The Balog–Szemerédi–Gowers Theorem

by Angeliki Koutsoukou-Argyraki, Mantas Bakšys and Chelsea Edmonds

##### The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections

by Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel and Patrick Lederer

##### Correctness of a Set-based Algorithm for Computing Strongly Connected Components of a Graph

by Stephan Merz and Vincent Trélat

##### Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL

by Diego Marmsoler and Achim D. Brucker

##### IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols

by Tobias Klenze and Christoph Sprenger

##### Diophantine Equations and the DPRM Theorem

by Jonas Bayer, Marco David, Benedikt Stock, Abhik Pal, Yuri Matiyasevich and Dierk Schleicher

##### A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand

by Thibault Dardinier

##### Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics

by Chelsea Edmonds and Lawrence C. Paulson

##### The Independence of the Continuum Hypothesis in Isabelle/ZF

by Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf and Matías Steinberg

##### Transitive Models of Fragments of ZFC

by Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf and Matías Steinberg

##### A Sequent Calculus Prover for First-Order Logic with Functions

by Asta Halkjær From and Frederik Krogsdal Jacobsen

## 2021

##### Roth's Theorem on Arithmetic Progressions

by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

##### Verified Algorithms for Solving Markov Decision Processes

by Maximilian Schäffeler and Mohammad Abdulaziz

##### Regular Tree Relations

by Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann and Thomas Sternagel

##### Simplicial Complexes and Boolean functions

by Jesús Aransay, Alejandro del Campo and Julius Michaelis

##### Foundation of geometry in planes, and some complements: Excluding the parallel axioms

by Fumiya Iwama

##### Exploring Simplified Variants of Gödel’s Ontological Argument in Isabelle/HOL

by Christoph Benzmüller

##### Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL

by Christoph Benzmüller and Sebastian Reiche

##### Szemerédi's Regularity Lemma

by Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson

##### X86 instruction semantics and basic block symbolic execution

by Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag and Binoy Ravindran

##### Algebras for Iteration, Infinite Executions and Correctness of Sequential Computations

by Walter Guttmann

##### Verified Quadratic Virtual Substitution for Real Arithmetic

by Matias Scharager, Katherine Kosaian, Stefan Mitsch and André Platzer

##### A Formalization of Weighted Path Orders and Recursive Path Orders

by Christian Sternagel, René Thiemann and Akihisa Yamada

##### Category Theory for ZFC in HOL I: Foundations: Design Patterns, Set Theory, Digraphs, Semicategories

by Mihails Milehins

##### CoSMeDis: A confidentiality-verified distributed social media platform

by Thomas Bauereiss and Andrei Popescu

##### CoCon: A Confidentiality-Verified Conference Management System

by Andrei Popescu, Peter Lammich and Thomas Bauereiss

##### Schutz' Independent Axioms for Minkowski Spacetime

by Richard Schmoetten, Jake Palmer and Jacques D. Fleuriot

##### SpecCheck - Specification-Based Testing for Isabelle/ML

by Kevin Kappelmann, Lukas Bulwahn and Sebastian Willenbrink

##### The BKR Decision Procedure for Univariate Real Arithmetic

by Katherine Kosaian, Yong Kiam Tan and André Platzer

##### Formalization of Timely Dataflow's Progress Tracking Protocol

by Matthias Brun, Sára Decova, Andrea Lattuada and Dmitriy Traytel

##### Constructive Cryptography in HOL: the Communication Modeling Aspect

by Andreas Lochbihler and S. Reza Sefidgar

##### Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

by Ralph Bottesch, Jose Divasón and René Thiemann

##### Tarski's Parallel Postulate implies the 5th Postulate of Euclid, the Postulate of Playfair and the original Parallel Postulate of Euclid

by Roland Coghetto

## 2020

##### The Relational Method with Message Anonymity for the Verification of Cryptographic Protocols

by Pasquale Noce

##### Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information

by Anthony Bordg, Hanna Lachnitt and Yijun He

##### A Sound Type System for Physical Quantities, Units, and Measurements

by Simon Foster and Burkhart Wolff

##### A Formal Model of the Safely Composable Document Object Model with Shadow Roots

by Achim D. Brucker and Michael Herzberg

##### A Formal Model of the Document Object Model with Shadow Roots

by Achim D. Brucker and Michael Herzberg

##### From Abstract to Concrete Gödel's Incompleteness Theorems—Part II

by Andrei Popescu and Dmitriy Traytel

##### From Abstract to Concrete Gödel's Incompleteness Theorems—Part I

by Andrei Popescu and Dmitriy Traytel

##### Inference of Extended Finite State Machines

by Michael Foster, Achim D. Brucker, Ramsay G. Taylor and John Derrick

##### A Formal Model of Extended Finite State Machines

by Michael Foster, Achim D. Brucker, Ramsay G. Taylor and John Derrick

##### Extensions to the Comprehensive Framework for Saturation Theorem Proving

by Jasmin Christian Blanchette and Sophie Tourret

##### A Formal Proof of The Chandy--Lamport Distributed Snapshot Algorithm

by Ben Fiedler and Dmitriy Traytel

##### A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles

by Albert Rizaldi and Fabian Immler

##### An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation

by Salomon Sickert

##### Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows

by Lukas Heimes, Dmitriy Traytel and Joshua Schneider

##### Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations

by Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider and Dmitriy Traytel

##### Stateful Protocol Composition and Typing

by Andreas V. Hess, Sebastian Mödersheim and Achim D. Brucker

##### Automated Stateful Protocol Verification

by Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull

##### Strong Eventual Consistency of the Collaborative Editing Framework WOOT

by Emin Karayel and Edgar Gonzàlez

##### Verified Approximation Algorithms

by Robin Eßmann, Tobias Nipkow, Simon Robillard and Ujkan Sulejmani

## 2019

##### An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges

by Pasquale Noce

##### Clean - An Abstract Imperative Programming Language and its Theory

by Frédéric Tuong and Burkhart Wolff

##### Communicating Concurrent Kleene Algebra for Distributed Systems Specification

by Maxime Buyse and Jason Jaskolka

##### A Formal Development of a Polychronous Polytimed Coordination Language

by Hai Nguyen Van, Frédéric Boulanger and Burkhart Wolff

##### Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic

by Joshua Schneider and Dmitriy Traytel

##### Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra

by Peter Lammich and Tobias Nipkow

##### A Compositional and Unified Translation of LTL into ω-Automata

by Benedikt Seidl and Salomon Sickert

##### Quantum Hoare Logic

by Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying and Naijun Zhan

##### Kruskal's Algorithm for Minimum Spanning Forest

by Maximilian P. L. Haslbeck, Peter Lammich and Julian Biendarra

##### Universal Turing Machine

by Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten and Franz Regensburger

##### Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming

by Simon Foster, Frank Zeyda, Yakoub Nemouchi, Pedro Ribeiro and Burkhart Wolff

##### Farkas' Lemma and Motzkin's Transposition Theorem

by Ralph Bottesch, Max W. Haslbeck and René Thiemann

## 2018

##### A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover

by Anders Schlichtkrull, Jasmin Christian Blanchette and Dmitriy Traytel

##### Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL

by David Fuenmayor and Christoph Benzmüller

##### Upper Bounding Diameters of State Spaces of Factored Transition Systems

by Friedrich Kurz and Mohammad Abdulaziz

##### An Incremental Simplex Algorithm with Unsatisfiable Core Generation

by Filip Marić, Mirko Spasić and René Thiemann

##### OpSets: Sequential Specifications for Replicated Datatypes

by Martin Kleppmann, Victor B. F. Gomes, Dominic P. Mulligan and Alastair R. Beresford

##### An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties

by Oliver Bračevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock and Markus Tasch

##### Bounded Natural Functors with Covariance and Contravariance

by Andreas Lochbihler and Joshua Schneider

##### The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency

by Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker

##### A verified factorization algorithm for integer polynomials with polynomial complexity

by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

##### A verified LLL algorithm

by Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

##### Formalization of Bachmair and Ganzinger's Ordered Resolution Prover

by Anders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel and Uwe Waldmann

## 2017

##### Operations on Bounded Natural Functors

by Jasmin Christian Blanchette, Andrei Popescu and Dmitriy Traytel

##### Homogeneous Linear Diophantine Equations

by Florian Messner, Julian Parsert, Jonas Schöpf and Christian Sternagel

##### Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument

by David Fuenmayor and Christoph Benzmüller

##### Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL

by Daniel Kirchner

##### Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus

by Michael Rawson

##### A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes

by Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan and Alastair R. Beresford

##### Partial Semigroups and Convolution Algebras

by Brijesh Dongol, Victor B. F. Gomes, Ian J. Hayes and Georg Struth

##### Refining Authenticated Key Agreement with Strong Adversaries

by Joseph Lallemand and Christoph Sprenger

##### Formal Network Models and Their Application to Firewall Policies

by Achim D. Brucker, Lukas Brügger and Burkhart Wolff

##### Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method

by Pasquale Noce

##### First-Order Logic According to Harrison

by Alexander Birch Jensen, Anders Schlichtkrull and Jørgen Villadsen

## 2016

##### COMPLX: A Verification Framework for Concurrent Imperative Programs

by Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong

##### Separata: Isabelle tactics for Separation Algebra

by Zhe Hou, David Sanan, Alwen Tiu, Rajeev Gore and Ranald Clouston

##### Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

by Jasmin Christian Blanchette, Mathias Fleury and Dmitriy Traytel

##### Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms

by Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

##### Modal Logics for Nominal Transition Systems

by Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström and Ramunas Gutkovas

##### A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor

by Zhe Hou, David Sanan, Alwen Tiu and Yang Liu

##### The Factorization Algorithm of Berlekamp and Zassenhaus

by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

##### Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms

by Jasmin Christian Blanchette, Uwe Waldmann and Daniel Wand

##### Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths

by Romain Aissat, Frederic Voisin and Burkhart Wolff

##### Compositional Security-Preserving Refinement for Concurrent Imperative Programs

by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

##### A Dependent Security Type System for Concurrent Imperative Programs

by Toby Murray, Robert Sison, Edward Pierzchalski and Christine Rizkallah

##### Program Construction and Verification Components Based on Kleene Algebra

by Victor B. F. Gomes and Georg Struth

##### Finite Machine Word Library

by Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk and Thomas Sewell

##### POSIX Lexing with Derivatives of Regular Expressions

by Fahad Ausaf, Roy Dyckhoff and Christian Urban

##### Perron-Frobenius Theorem for Spectral Radius Analysis

by Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada

##### A Constructive Proof for FLP

by Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters and Uwe Nestmann

##### Algorithms for Reduced Ordered Binary Decision Diagrams

by Julius Michaelis, Max W. Haslbeck, Peter Lammich and Lars Hupel

##### Kleene Algebras with Domain

by Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth and Tjark Weber

## 2015

##### Analysing and Comparing Encodability Criteria for Process Calculi

by Kirstin Peters and Rob van Glabbeek

##### VCG - Combinatorial Vickrey-Clarke-Groves Auctions

by Marco B. Caminati, Manfred Kerber, Christoph Lange and Colin Rowat

##### Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO

by Peter Gammie, Tony Hosking and Kai Engelhardt

## 2014

##### A Verified Compiler for Probability Density Functions

by Manuel Eberl, Johannes Hölzl and Tobias Nipkow

##### Formal Specification of a Generic Separation Kernel

by Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Julien Schmaltz

##### Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions

by Dmitriy Traytel and Tobias Nipkow

##### Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm

by Peter Lammich

##### Converting Linear-Time Temporal Logic to Generalized Büchi Automata

by Alexander Schimpf and Peter Lammich

##### A Fully Verified Executable LTL Model Checker

by Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf and Jan-Georg Smaus

##### A Formalization of Declassification with WHAT-and-WHERE-Security

by Sylvia Grewe, Alexander Lux, Heiko Mantel and Jens Sauer

##### A Formalization of Assumptions and Guarantees for Compositional Noninterference

by Sylvia Grewe, Heiko Mantel and Daniel Schoepe

##### Kleene Algebra with Tests and Demonic Refinement Algebras

by Alasdair Armstrong, Victor B. F. Gomes and Georg Struth

##### Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5

by Achim D. Brucker, Frédéric Tuong and Burkhart Wolff

## 2013

##### Sound and Complete Sort Encodings for First-Order Logic

by Jasmin Christian Blanchette and Andrei Popescu

## 2012

##### Proving the Impossibility of Trisecting an Angle and Doubling the Cube

by Ralph Romanos and Lawrence C. Paulson

##### Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model

by Henri Debrat and Stephan Merz

## 2011

##### The Myhill-Nerode Theorem Based on Regular Expressions

by Chunhan Wu, Xingyuan Zhang and Christian Urban

## 2010

##### Executable Multivariate Polynomials

by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp

##### Executable Matrix Operations on Matrices of Arbitrary Dimensions

by Christian Sternagel and René Thiemann

##### Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement

by Viorel Preoteasa and Ralph-Johan Back

## 2009

##### Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer

by Daniel Wasserrab

## 2008

##### A Correctness Proof for the Volpano/Smith Security Typing System

by Gregor Snelting and Daniel Wasserrab

##### A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

by Norbert Schirmer

## 2007

##### Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors

by Peter Lammich and Markus Müller-Olm

##### Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples

by Roelof Oosterhuis

## 2006

## 2005

## 2004

##### A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic

by Tom Ridge