  Blockchain has recently attracted the attention of the industry due, in part,
to its ability to automate asset transfers. It requires distributed
participants to reach a consensus on a block despite the presence of malicious
(a.k.a. Byzantine) participants. Malicious participants exploit regularly
weaknesses of these blockchain consensus algorithms, with sometimes devastating
consequences. In fact, these weaknesses are quite common and are well
illustrated by the flaws in the hand-written proofs of existing blockchain
consensus protocols [63]. Paradoxically, until now, no blockchain consensus has
been holistically verified using model checking.
  In this paper, we remedy this paradox by model checking for the first time a
blockchain consensus used in industry. We propose a holistic approach to verify
the consensus algorithm of the Red Belly Blockchain [20], for any number $n$ of
processes and any number $f<n/3$ of Byzantine processes. We decompose directly
the algorithm pseudocode in two parts -- an inner broadcast algorithm and an
outer decision algorithm -- each modelled as a threshold automaton [36], and we
formalize their expected properties in linear-time temporal logic. We then
automatically check the inner broadcasting algorithm, under a carefully
identified fairness assumption. For the verification of the outer algorithm, we
simplify the model of the inner algorithm by relying on its checked properties.
Doing so, we formally verify not only the safety properties of the Red Belly
Blockchain consensus but also its liveness in about 70 seconds.
