http://www.cs.famaf.unc.edu.ar/~damian/
This is an unofficial reimagining of the Archive of Formal Proofs
Instances of Schneider's generalized protocol of clock synchronizationby Damián Barsotti