home

Abstract: Fault-tolerant distributed algorithms, such as Consensus algorithms, are often quite subtle in the way they operate and in the assumptions they make. Moreover, it is difficult to compare existing algorithms because they are presented in different computational models and with different assumptions about message synchrony and failure hypotheses, they are also rarely proved correct in a formal system. We have formally verified different Consensus algorithms tolerating various kinds of failures (including benign and Byzantine failures). All algorithms were expressed in the Heard-Of model, a uniform computational model that allows us to compare the assumptions under which the algorithms operate. Our proofs are made possible by the observation that (almost) all known Consensus algorithms are structured in communication-closed rounds. Formally, we prove a reduction theorem that can be retraced to Lipton's seminal paper (1975) or Zwiers' work communication-closed layers in the early 1990s, and that allows us to pretend that nodes operate in lock-step. In this talk, we will present the main ideas underlying our development, and particularly insist on the importance of choosing appropriate high-level abstractions.