Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization

Schneider [Sch87] generalizes a number of protocols for Byzantine fault-tolerant clock synchronization and presents a uniform proof for their correctness. We present a mechanical verification of Schneider's protocol leading to several significant clarifications and revisions. The verification was carried out with the Ehdm system [RvHO91] developed at the SRI Computer Science Laboratory. The mechanically checked proofs include the verification that the egocentric mean function used in Lamport and Melliar-Smith's Interactive Convergence Algorithm [LMS85] satisfies the requirements of Schneider's protocol. Our mechanical verification raises a number of issues regarding the verification of fault-tolerant, distributed, real-time protocols that are germane to the design of a special-purpose logic for such problems