Proving the Correctness of Disk Paxos

Mauro Jaskelioff, Stephan Merz. Proving the Correctness of Disk Paxos. Archive of Formal Proofs, 2005, 2005. [doi]