From Fault-Tolerant Computing Symposium, FTCS 23.
IEEE Computer Society, Toulouse, France.
June, 1993.
Pages 402–411.

Thambidurai and Park 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-resilent algorithms. Unfortunately, and despite a published proof of correctness, their algorithm is flawed. We detected this while undertaking a formal verification of the algorithm.

We 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, we believe formal verification should become standard for algorithms intended for safety-critical applications.

@inproceedings{ftcs93,
    AUTHOR = {Patrick Lincoln and John Rushby},
    TITLE = {{A} Formally Verified Algorithm for Interactive Consistency Under a Hybrid Fault Model},
    BOOKTITLE = {Fault-Tolerant Computing Symposium, {FTCS} 23},
    YEAR = {1993},
    PAGES = {402--411},
    ADDRESS = {Toulouse, France},
    MONTH = {jun},
    ORGANIZATION = {{IEEE} Computer Society},
    URL = {http://www.csl.sri.com/papers/ftcs93/}
}

• ftcs93.pdf