conclusion.tex

\section{Discussion and Conclusion}

In summary, we've partially specified a family of consensus protocols and shown that every member of this family has asynchronous, Byzantine-fault-tolerant consensus safety. Furthermore, we've given examples of members of the family of increasing complexity to demonstrate the power and flexibility of our approach to correct-by-construction consensus protocol design.

Although the protocols given here are not fully enough defined to serve as production systems, we contend that the specifications given here make it easy to define many practical protocols. For example, we have been able to show that it's possible to do consensus with asynchronous Byzantine-fault-tolerant safety with the same network overhead as Nakamoto consensus. We strongly suspect that CBC Casper protocols are qualitatively different from traditional consensus protocols like Paxos\cite{paxos} or PBFT\cite{Castro_Liskov_1999_pbft}.

Notable related work that isn't discussed here includes work on fault attribution and classification, the detection of decisions in CBC Casper protocols, light client CBC Casper protocols, running CBC Casper with extra-protocol fault tolerance thresholds, doing validator set changes, guaranteeing the validity and availability of messages, and work on ensuring the existence of incentives in proof-of-stake.

Work on liveness, validator strategies for making consensus messages, and for preventing denial-of-service attacks is ongoing. Furthermore, work of parametrizing penalties and rewards for security-deposit based proof-of-stake is in relatively early stages. 

Exploration of the CBC Casper family of protocols (and their implementations) is in early stages, and we have relatively very little undertanding of what would make an ``ideal" estimator, or of what kind of estimators lead to the lowest latency or lowest overhead decisions. For example, Vitalik's discussion of latest message-based estimators vs ``immediate" message-driven fork choice rules\cite{vitalik-FFG-CBC-wars-tweet-thread}.

The work shared here is supposed to be the simplest formalization that will give the reader an understanding of the logic behind the proof of asynchronous Byzantine-fault-tolerant safety for the broadest family of CBC Casper consensus protocols. It isn't meant to be a complete specification of a consensus protocol, nor does the specification represent the best way to implement even this partial specification. We therefore primarily hope that readers find this work to be educational, and secondarily that it puts them in a position to contribute to ``CBC Casper research".