A formally verified algorithm for interactive consistency under a hybrid fault model

P. Thambidurai and Y.-K. Park (1988) have proposed an algorithm for interactive consistency that retains resilience to the arbitrary (or Byzantine) fault mode, while tolerating more faults of simpler kinds than standard Byzantine-resilient algorithms. Unfortunately, and despite a published proof of correctness, their algorithm is flawed. The authors detected this while undertaking a formal verification of the algorithm. They present a corrected algorithm that has been subjected to mechanically checked formal verification. Because informal proofs seem unreliable in this domain, and the consequences of failure could be catastrophic, the authors believe formal verification should become standard for algorithms intended for safety-critical applications.