Formal Analysis of a Proof-of-Stake Blockchain

Blockchain technology relies on consensus algorithms to resolve conflicts in Byzantine environments. New blockchain algorithms are rapidly designed and implemented without a properly conducted formal analysis and verification. In this paper, we conducted a study on Tendermint which is a proof-of-stake consensus algorithm. We verified that the consensus protocol is deadlock-free and is able to reach consensus when at least 2/3 of the network is in agreement. We also proved that a minority set of nodes that compose more than 1/3 of the network is enough to censor the majority of the network and prevent the network from reaching consensus and conclude that the algorithm has some shortcomings on availability.