Verifying fault-tolerant distributed algorithms in the heard-of model. Archive of Formal Proofs

Distributed computing is inherently based on replication, promising in-creased tolerance to failures of individual computing nodes or communi-cation channels. Realizing this promise, however, involves quite subtle al-gorithmic mechanisms, and requires precise statements about the kinds and numbers of faults that an algorithm tolerates (such as process crashes, com-munication faults or corrupted values). The landmark theorem due to Fis-cher, Lynch, and Paterson shows that it is impossible to achieve Consensus among N asynchronously communicating nodes in the presence of even a single permanent failure. Existing solutions must rely on assumptions of “partial synchrony”. Indeed, there have been numerous misunderstandings on what exactly a given algorithm is supposed to realize in what kinds of environments. More-over, the abundance of subtly different computational models complicates comparisons between different algorithms. Charron-Bost and Schiper intro-duced the Heard-Of model for representing algorithms and failure assump