Correct-by-construction Casper | A Visualization for the Future of Blockchain Consensus

This is what the third generation blockchain platform, RChain’s current model of consensus looks like in action:

It’s mesmerizing to watch, but what is this animation all about? It shows continued progress in the development of the Casper consensus algorithm for use on the RChain platform. Here, we discuss a little background of Correct-By-Construction Casper, how it is being applied to RChain, and how to interpret the image above. This article is written for those who have some familiarity with distributed consensus as it applies to blockchains; some background material which readers not too familiar with that work may consider looking over can be found in the links below:

With that out of the way, let’s get started.


Introduction to Correct-by-Construction (CBC) Casper

The correct-by-construction design philosophy follows these steps:

  1. lay out an abstract (mathematical) framework for the thing that you want to create;
  2. prove that all instances of things following that framework have certain desirable properties (i.e. prove it is correct);
  3. create a concrete thing, matching your use case, within that proven correct framework.

The main advantage of this approach is being certain the outcome has the properties you need. Moreover, working in an abstract setting means that steps 1 and 2 can actually solve many problems at once if they have sufficient similarities. For example, an abstract consensus framework does not necessarily need to reference the specifics of what we are looking for consensus on; thus a single framework could give rise to proven correct protocols for many different blockchain-like systems (regardless of architecture) or indeed anything at all we might want multiple parties to agree on.

Much of the work for the first two steps of the CBC process have already been done for the case of a distributed, asynchronous, trustless consensus algorithm (details have been uploaded to GitHub). This work was done by Vlad Zamfir in collaboration with Vitalik Buterin, Greg Meredith, and others in a research group initiated by the Ethereum Foundation. In short, the abstract framework represents the protocol itself as a category where the objects are the protocol states and the morphisms are the protocol executions, and defines a function called the “estimator” which maps protocol states onto satisfiable logical propositions about the consensus.

One of the properties this framework has is “consensus safety.” This means that as long as two protocol states have a common future (i.e. there is a pair of protocol executions which bring the two states to the same state), then any propositions that each state is certain of must not be contradictory. Phrased another way, consensus is always possible.

Vlad and others have also done work to apply their framework to the case where we want consensus on a blockchain (the paper is uploaded to GitHub). A key insight in that work is that if “justifications” are required as part of the protocol, then certain Byzantine Faults (non-protocol behaviors) can be easily detected, thus providing further safety to the protocol. From this, the main achievement of the work is to specify an asynchronous and Byzantine fault tolerant protocol with very low message passing overhead. The paper also makes use of the Greedy Heaviest Observed Sub-Tree (GHOST) fork choice rule (which, yes, is a pun that is 100% on purpose), originally developed by Aviv Zohar and Yonatan Sompolinsky. GHOST tells validators how to decide what branch of the chain to build on, based on the information they have received so far. The details of GHOST itself can be found in Vlad’s paper, but these details are not strictly necessary for the present article. The main idea is that “scores” are calculated for each block at the top of the chain based on some “weights” that are related to the validators. The block with the highest score is the one which is chosen as the parent for new blocks.


RChain’s CBC Casper

The development team for The RChain Cooperative is building on the above foundational work in two important and related ways:

  1. consensus is happening on a directed acyclic graph of blocks (blockDAG), rather than a blockchain;
  2. introducing agency of the validators through block acknowledgement and political capital (PC).

The first point simply means that a block may have multiple parents and multiple children. The DAG structure allows for the acknowledgement (as per the second point) of multiple blocks. This in turn serves as a “join” operation and allows independent branches can be merged into a single branch, thus reducing the time to reach consensus.

The second point, validator agency, is the key departure from previous CBC Casper work. The amount of PC a validator spends on a block corresponds to its weight in the GHOST fork choice rule. Therefore, a block with more PC is more likely to remain a part of the main blockDAG. The amount of PC a validator chooses to attach to a block can be thought of as a “bet” on the success of that block. The other aspect of validator agency is the ability to acknowledge blocks. Acknowledgements, unlike new block proposals, are not subject to the GHOST fork choice rule, thus validators have more influence over which branch of the blockDAG continues. Acknowledgements of blocks serve both as a vote of support, and the only mechanism of earning PC. Earning PC exclusively through acknowledgements is important because it means that the only way to contribute to new blocks which have a significant amount of PC attached (and thus will be more likely to remain part of the main DAG) is to participate in the consensus for an extended period of time.

A more detailed description of the protocol can be found on RChain’s wiki.


Understanding the Impact of Agency

Once agency is allowed into a protocol, it essentially becomes a game. For a validator on a Proof-of-Stake distributed computing platform such as RChain, the goal of the game is to maximize the fees earned from running smart contracts. Infinitely many strategies exist for this game, not all of which may be good for the network. It is therefore critical to try to ensure that only strategies which embody desired behaviors are successful. To this end, a simulation engine for RChain’s Casper has been written to allow experimenting with different strategies. In the end, bad actors are necessarily identified and discharged from the network, but it is important to systematically disincentivize such behaviour in the first place in order to make the network safer for everyone. The purpose of the simulation is to help us ensure bad behaviour is indeed disadvantageous compared to behaviour which improves the network.

A simulation is only as good as the data it produces. The post-simulation data allows us to draw conclusions about the behaviours the protocol promotes. Quantitative data can put numbers behind statements like some strategy is advantageous, telling us precisely how much better it might be than some other strategy. Visualizations, on the other hand, can provide intuitions and deeper explanations of the quantitative data — both are important. And, as it turns out, RChain’s Casper implementation looks really cool too!

The image at the beginning of the article was generated by the simulation and shows Casper at work with three validators. The nodes (circles) correspond to blocks in the DAG and are coloured according to which validator created them. The single orange node at the beginning is the genesis block. The size of the nodes is proportional to the number of contracts run in that block (the smallest nodes have no contracts and are acknowledgements). The arrows are parent block pointers. Red arrows correspond to the connections in the main DAG, as determined by the GHOST fork choice rule, while black arrows are discarded, or yet to be decided upon, branches.

As simulation and other foundational work continues, future pictures like this will aid understanding and therefore help ensure that we develop the safest, most efficient (technically and in terms of power consumption) consensus algorithm for RChain as a third generation blockchain platform: formally verified, fast, and scalable.


For a deeper dive into the CBC Casper approach of RChain, visit the developers wiki and join as a member through member.rchain.coop.

*Special thanks to the RChain Cooperative members who contributed to the curation and editing of this post (Vlad Zamfir, Greg Meredith, Lawrence Lerner, Leah McKelvie, and Patrick Maguire.)