Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker

Threshold guards are a basic primitive of many fault-tolerant algorithms thatsolve classical problems in distributed computing, such as reliable broadcast,two-phase commit, and consensus. Moreover, threshold guards can be found inrecent blockchain algorithms such as, e.g., Tendermint consensus. In thisarticle, we give an overview of techniques for automated verification ofthreshold-guarded fault-tolerant distributed algorithms, implemented in theByzantine Model Checker (ByMC). These threshold-guarded algorithms have thefollowing features: (1) up to $t$ of processes may crash or behave Byzantine;(2) the correct processes count messages and make progress when they receivesufficiently many messages, e.g., at least $t+1$; (3) the number $n$ ofprocesses in the system is a parameter, as well as the number $t$ of faults;and (4) the parameters are restricted by a resilience condition, e.g., $n >3t$. Traditionally, these algorithms were implemented in distributed systemswith up to ten participating processes. Nowadays, they are implemented indistributed systems that involve hundreds or thousands of processes. To makesure that these algorithms are still correct for that scale, it is imperativeto verify them for all possible values of the parameters