Machine checked proofs of the design of a fault-tolerant circuit

We describe a formally verified implementation of the “Oral Messages” algorithm of Pease, Shostak and LamportJ. ACM (1980)27, 228–234;ACM TOPLAS (1982)4, 382–401. An abstract implementation of the algorithm is proved to achieve interactive consistency in the presence of faults. This abstract characterisation is then mapped down to a hardware level implementation which inherits the fault-tolerant characteristics of the abstract version. All steps in the proof were checked with the Boyer-Moore theorem prover. A significant result of this work is the demonstration of a fault-tolerant device that is formally specified and the development of an implementation proved correct with respect to this specification. A significant simplifying assumption is that the redundant processors behave synchronously. We also describe a mechanically checked proof that the Oral Messages algorithm is “optimal” in the sense that no algorithm which achieves agreement via similar message passing can tolerate a larger proportion of faulty processors.