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
Extension of Stateful Intransitive Noninterference with Inputs, Outputs, and Nondeterminism in Language IMP
by Pasquale Noce
Compactness Theorem for Propositional Logic and Combinatorial Applications
by Fabián Fernando Serran Suárez, Thaynara Arielly de Lima and Mauricio Ayala-Rincón
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