### Abstract

Disk Paxos is an algorithm for building arbitrary fault-tolerant distributed systems. The specification of Disk Paxos has been proved correct informally and tested using the TLC model checker, but up to now, it has never been fully formally verified. In this work we have formally verified its correctness using the Isabelle theorem prover and the HOL logic system, showing that Isabelle is a practical tool for verifying properties of TLA+ specifications.

### License

BSD License

### Topics

- Computer science/Algorithms/Distributed

### Session DiskPaxos

- DiskPaxos_Model
- DiskPaxos_Inv1
- DiskPaxos_Inv2
- DiskPaxos_Inv3
- DiskPaxos_Inv4
- DiskPaxos_Inv5
- DiskPaxos_Chosen
- DiskPaxos_Inv6
- DiskPaxos_Invariant
- DiskPaxos

## Cite

×

DiskPaxos-AFP

    @article{DiskPaxos-AFP,
      author  = {Mauro Jaskelioff and Stephan Merz},
      title   = {Proving the Correctness of Disk Paxos},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2005},
      note    = {\url{https://isa-afp.org/entries/DiskPaxos.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jun 30, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Nov 27, 2007 : Isabelle2007
- Oct 14, 2005 : Isabelle2005
- Jun 22, 2005 : Isabelle2004