Correct By Construction (CBC) Casper

Correct-by-Construction (CBC) Casper, is the second major Casper protocol development initiative, with a launch on the Ethereum mainnet planned for sometime in 2019. The first Casper implementation scheduled for launch is named Friendly Finality Gadget (FFG).

CBC Casper, aka “Vlad’s Casper” (Vlad Zamfir is CBC’s project lead), is the second and more complete approach to using Casper to move Ethereum to a fully Proof of Stake network. CBC is much more than simply a layering of PoS onto the Ethereum PoW network. It is a full implementation of the asynchronous Ethereum BFT PoS consensus algorithm.

CBC relies on a “safety oracle” (which the Ethereum Foundation labels an “ideal adversary”) to constantly fine-tune a partially built PoS protocol until the system has been completed. Whereas Ethereum protocols are typically fully-defined before testing, the CBC protocol is only partially specified at the start, with the protocol completing itself as it satisfies desired/requisite protocol properties. CBC starts with an initial partial specification for network “safety” and then derives safety proofs “by construction” from first principles, enabling it to construct itself.

The full protocol is derived through the implementation of the safety oracle, which either raises exceptions of a fault of a justified estimate or enumerates the potential future faulty estimates. Local views of a node’s estimate of safety can be extended to achieve consensus safety.

CBC’s Validator Slashing Trilemma solution is designed to force a reasonable compromise among these Zamfir’s Triangle tradeoffs:
a. Finality Latency: how long it take the network to finalize a proposed block.
b. Resource Overhead: how many blocks per second must validators verify.
c. Decentralisation: how many validators can exist in the network.

The goal of the solution is to create the optimal balance (a “You can’t have it all” comprimise) between three competing desired outcomes:
a. High Cost of Attack (defense)
b. High Valuation Yield (maximum rewards)
c. Low ETH Issuance (inflation control)

In order for a block to be finalised, at least 2/3 of the validator pool in the network must validate it, with any one node only able to choose at most two of the three properties in Zamfir’s Triangle. CBC Casper’s tradeoffs fall somewhere in the middle of the tradeoff triangle, with a reasonably low latency to finality, reasonably low overhead, and reasonably large number of validators.

CBC will make each node “safe”, i.e., impossible for two protocol-following nodes to make different decisions, since:
a. An attacker can’t know which safety thresholds are set locally.
b. Individual nodes are given greater flexibility in choosing between tradeoffs in Zamfir’s Triangle.

The CBC process will unfold in two steps:
1. Specifying data types and definitions that the protocol must satisfy to benefit from the implied results.
2. “Filling in the blanks” — defining implementations of data structures that satisfy the types and definitions required by the proof.

CBC Casper “derives” consensus protocols. Benefits include:

    • A relatively simple and shared consensus safety proof.
    • The absence of an “in-protocol” finality threshold.
    • The ability to make tradeoffs between number of nodes, network overhead, and latency to finality.
    • Theoretically optimal network overhead in the certain cases.