Thanks to Carl Beekhuizen for review

Any blockchain must provide two basic guarantees to its users: finality of blocks, and liveness of the blockchain. The underlying consensus mechanism of the blockchain is responsible for providing these guarantees. In Eth2.0, the consensus process happens only in the beacon chain, and the Casper Friendly Finality Gadget (FFG) mechanism is utilized for this purpose. This blog post aims to describe the basic Casper FFG mechanism and provide proofs of the guarantees it provides.

Casper FFG is a "finality gadget", meaning that it describes the rules for finality of blocks, and detects the finalization of blocks after the fact. The FFG mechanism is de-coupled from the chain growth process, and can be set up as an independent overlay over any live blockchain protocol to provide finality of blocks. In this regard, Casper FFG is not a full-fledged consensus protocol, since there is no description of a strategy to achieve liveness of the chain in the mechanism itself. (Maybe I'll write a post about the liveness considerations of the Eth2.0 Beacon Chain at some point!)

Let's start by taking a look at the structures that Casper FFG defines, then dive into the rules of the mechanism, and finally understand the proofs of its safety & liveness guarantees!

Votes

Validators vote for blocks in the chain by attesting to "valid transitions" between blocks. Votes are of the format (S, T), and contain the following two pieces of information:

• Source block (S)
• Target block (T), which must be a descendant of S

In practice, a vote includes information such as a digital signature of the validator, and block hash & block height to identify the block.

Justification & Finalization

Justification and finalization are phases of the consensus process in Casper FFG. These can be compared to the "prepare" and "commit" stages of the more traditional BFT consensus protocols.

Justification: A block B is justified if:

• it is the genesis block, or
• more than 2/3rd validators have made votes (A, B), where A is some ancestor of B and A is a justified block

Finalization: A block B is finalized if:

• it is the genesis block, or
• B is justified and more than 2/3rd validators have made votes (B, C), where C is the direct child of B (i.e., height(C) = height(B) + 1)

Note: There is a more general definition of finalization in Casper FFG which is used in Eth2.0. More information about it can be found in this paper. The specific definition above was chosen to keep this post simple.

Casper FFG Rules

There are only two simple Casper FFG rules. A validator cannot make two votes (S1, T1) and (S2, T2) such that either of these conditions hold:
1.Double Vote: height(T1) = height(T2), or
2.Surround Vote: height(S1) < height(S2) < height(T2) < height(T1)

Safety & Liveness

The purpose of Casper FFG is to provide consensus safety and liveness over the finalization of blocks. In particular, Casper FFG provides the following guarantees:

• Accountable Safety: If two conflicting blocks are finalized, then at least 1/3rd validators have broken the Casper FFG rules, and these validators can be identified.
• Plausible Liveness: In any state of the protocol, there is some set of votes that validators can make to finalize a new block without violating any Casper FFG rules.

While these are unorthodox definitions of safety and liveness as compared to traditional BFT literature, these interpretations are well-suited for a blockchain finality gadget!

In fact, readers familiar with BFT literature will find the definition of plausible liveness very absurd. However, since Casper FFG is only a finality gadget, the only liveness guarantees it needs to make is that the mechanism will never be stuck in a situation where honest validators need to violate FFG rules in order to make progress.

In regards to the safety definition, we want accountability (i.e., violators of the rules can be identified) so that we can pass this information along to the proof-of-stake mechanism, which will then penalize the dishonest validators. The goal is to provide information to the proof-of-stake mechanism that allows it to incentivize an equilibrium that is the intended protocol.

Safety Proof

Let two conflicting block (neither of them is a descendant of the other) A and B be finalized. There are two cases:

• height(A) = height(B)

  • Since A &B both need to be justified in order to be finalized, at least 2/3rd validators each made votes where the targets were A and B respectively. This means that at least 1/3rd validators broke the first Casper FFG rule.

• height(A) < height(B) (without loss of generality)

  • For A to be finalized, at least 2/3rd validators made the vote (A, C), where C is the direct child of A.
  • For B to be justified, there must be some sequence of blocks in the increasing order of height [genesis, B_0, B_1, ... , B_n, B], where each block justifies the next block in sequence, i.e., at least 2/3rd validators made the votes (G, B_0), (B_0, B_1), and so on. Let B_m be the first block in this sequence that has height(A) < height(B_m).
  • Note that if any block in this sequence has the same height as A or C, then by similar reasoning as the previous case, we have our proof.
  • Now consider the votes for (B_n, B_m) (where n = m-1) which lead to the justification of B_m. Since neither height(B_n) or height(B_m) are equal to height(A) or height(C), it must be the case that height(B_n) < height(A) < height(C) < height(B_m).
  • Therefore, 2/3rd validators must have violated the second Casper FFG rule.

Also note that it is easy to identify the validators who violated the Casper FFG rules simply by inspecting the set of all votes, finding the conflicting votes, and checking the validator siganture on those votes.

Liveness Proof

• Let P_0 be the justified block with the greatest height, and Q be the block with the greatest height that any validator has made a vote for.
• Consider any block P_1 which is a descendant of P_0 with height(Q) < height(P_1). This block can be justified by 2/3rd validators voting for (P_0, P_1) without violating any Casper FFG rules.
• P_1 can also be finalized by 2/3rd validators voting for (P_1, P_2), where P_2 is some descendant of P_1. This can also be done without violating any Casper FFG rules.

Hence, it's always possible for a set of at least 2/3rd honest validators to finalize a new block.

Additional Reading Material

1. The original Casper FFG paper - Casper the Friendly Finality Gadget
2. An analysis of Casper FFG in Eth2.0 - Combining GHOST and Casper