本文是对论文Combining GHOST and Casper的解读。 本文分为3部分WHAT、WHY、PRACTICE, 大致对应论文的结构，分别讲Gasper协议的内容、协议有效性证明、beacon chain在实现Gasper时的一些tradeoff。
在本文中，我们希望介绍这一成就的第一部分：验证 Gasper 的属性。所以，什么是 Gasper？如何能形式化地验证其属性？这种形式化验证有何意义？
Bo101010
EthFans