Today I was reading the paper Understanding Blockchain Consensus Models written by Dr. Arati Baliga and I couldn't agree more with the statement that “A blockchain based system is as secure and robust as its consensus model.” Having a PhD in formal verification of distributed systems I have been constantly thinking about the importance of correctness in such protocols.
Since I started engaging myself in learning Blockchain I was deeply interested in consensus protocols. Leslie Lamport’s Byzantine Generals Problem and the various formalizations of it using different logic systems, for example, TLA or CLT occupied part of my PhD years.
Tanenbaum and Steen define a distributed system as “a collection of independent computers that appears to its users as a coherent system”. Blockchain platforms have been proposed as distributed computation systems, where the consensus algorithm is the foundation. The big difference between blockchain algorithms and other distributed system is the lack of a central authority able to change the algorithm. In blockchain such change is called a hard fork, i.e. "a radical change to the protocol that makes previously invalid blocks/transactions valid (or vice-versa), and as such requires all nodes or users to upgrade to the latest version of the protocol software" (Investopedia). This poses a risk since if no consensus is reached between the users then it will create two blockchains, each with its own set of coins. Consequently, having a faulty or incomplete blockchain consensus algorithm in the 800-billion-dollar cryptocurrency industry is not acceptable.
Formal verification offers a variety of techniques to model and verify properties such as liveness, safety, and fault tolerance, as well as, blockchain consensus specific properties, for example to answer the fundamental question: “Can we design consensus protocols which are resilient assuming only that a majority of the online players are honest?” (The Sleepy Model of Consensus - IACR Cryptology)
A formal proof of the consensus algorithms gives credibility to Blockchain companies using these approaches and help investors to make decisions. I predict that this field of study will gain more importance in the near future.