Featured Article: CBC Casper and formal verification

CBC Casper is a proposal of beautiful PoS consensus protocol which has various potential advantages and will possibly be adopted by ETH2.0 in the future. In this article, I describe the basics of CBC Casper and introduce our work.