Parameterized model checking [1]} works for an
arbitrary number \(n\)  of processes [2]}.
Although the problem is undecidable [3]} in general, one
can verify specific classes of algorithms [4]}.
Indeed, distributed algorithms with a ring-based topology were checked with automata-theoretic method [5]} and with Presburger arithmetics formulae verified by an SMT solver [6]}.
Bosco [7]} has been the focus of various parameterized verification techniques [8]}, [9]}, however,
it acts as a fast path wrapper around
a separate correct consensus algorithm that remains itself to be proven.
The condition-based consensus algorithm [10]}, [11]} was verified [9]} with the Byzantine model checker ByMC [13]}, [14]}, [15]}, only under the condition that the difference between the numbers of processes initialized with 0 and 1 differ by at least \(t\) .
Recently, the crash fault tolerant Ben-Or consensus algorithm was proved correct with a probabilistic reasoning extension of ByMC [16]}.
In this paper, we also exploit ByMC but prove the Byzantine consensus algorithm [17]} of an existing blockchain [18]}.
