  To implement a blockchain, the trend is now to integrate a non-trivial
Byzantine fault tolerant consensus algorithm instead of the seminal idea of
waiting to receive blocks to decide upon the longest branch. After a decade of
existence, blockchains trade now large amounts of valuable assets and a simple
disagreement could lead to disastrous losses. Unfortunately, Byzantine
consensus solutions used in blockchains are at best proved correct "by hand" as
we are not aware of any of them having been formally verified. In this paper,
we propose two contributions: (i) we illustrate the severity of the problem by
listing six vulnerabilities of blockchain consensus including two new
counter-examples; (ii) we then formally verify two Byzantine fault tolerant
components of Red Belly Blockchain using the ByMC model checker. First, we
specify a simple broadcast primitive in 116 lines of code that is verified in
40 seconds on a 2-core Intel machine. Then, we specify a blockchain consensus
algorithm in 276 lines of code that is verified in 17 minutes on a 64-core AMD
machine using MPI. To conclude, we argue that it has now become both relatively
simple and crucial to formally verify the correctness of blockchain consensus
protocols.
