http://www.fceia.unr.edu.ar/~mauro/
This is an unofficial reimagining of the Archive of Formal Proofs
Proving the Correctness of Disk Paxosby Mauro Jaskelioff and Stephan Merz