Buterin 和 Griffith 在 [7] 中介绍了 Casper 友好最终性⼩⼯具 (FFG)。该⼯具定义了受实⽤拜占庭容错 (PBFT) ⽂献启发的证明和最终性（justification and finalization） 概念。Casper 旨在与各种具有树状结构的区块链协议配合使用。
- 每个区块都有⼀个⾼度，该⾼度由其与创世区块（⾼度为 0）的距离定义。等效地，B 的⾼度是 chain(B) 的⻓度 −1。
- 我们将检查点（checkpoint） 块定义为⾼度为常数 H 倍数的块（在 [7] 中，H = 100）。我们将检查点块 B 的检查点⾼度 h(B)定义为 B 的⾼度除以 H，H 始终为整数。因此，我们可以认为视图中的检查点作为⼦树，仅包含⾼度为 H 倍数的块。
- 证明（Attestations） 是包含“检查点边”A → B 的签名消息，其中 A 和 B 是检查点区块。我们可以将每个这样的证明视为从区块 A 移动到 B 的“投票”。A 和 B 的选择取决于底层区块链，⽽不是 Casper 的⼀部分。每个证明都有⼀个权重，即编写证明的验证者的权益。理想情况下，h(B) = h(A) + 1，但这不是必需的。例如，如果 H = 100，诚实的验证者可能会以某种⽅式错过区块 200，在这种情况下，其底层区块链可能希望他们从检查点区块 100 向检查点区块 300 发送证明。
备注。 请注意，我们以插槽为单位设置时间，这些插槽被分组为时期。这类似于（但不完全相同）区块⾼度和检查点区块。我们将在第 4.1 节中进⼀步讨论这⼀点。
Casper FFG 还引⼊了证明（justification） 和最终确定（finalization） 的概念，它们类似于 PBFT ⽂献中基于阶段的概念，如准备（prepare） 和提交（commit），例如参⻅[8]：
- 在每个视图 G 中，都有一组合理的（justified） 检查点块 J(G) 和最终（finalized） 检查点块的子集 F(G) ⊂ J(G)。创世区块始终是合理且最终确定的。
- 在视图 G 中，如果 A 是合理的，并且有证明投票⽀持 A → B，且总权重⾄少为总验证者权益的 2/3，则检查点区块 B 是合理的（由合理的检查点区块 A 证明）。同样，我们说存在一个绝对多数链接（supermajority link） A → B。这是⼀个依赖于视图的条件，因为所讨论的视图可能已经或尚未看到打破 2/3 阈值的所有相关证明（甚⾄可能已经看到区块 B 本⾝），这就是为什么合理区块集由 G 参数化的原因。
- 在视图 G 中，若 A ∈ J(G)（等价地，A 是合理的），且 A → B 是一个绝对多数链接，且 h(B) = h(A) + 1，则我们说 A ∈ F(G)（等价地，A 是最终确定的）。
最后，Casper 引⼊了削减条件，这是对诚实验证者的假设。当验证者 V 违反这些条件时，不同的验证者 W 可以通过提供 V 违反条件的证据来削减 V（销毁 V 的权益并可能获得某种“削减奖励”）。
定义 3.1。 以下削减条件⼀旦被破坏，将导致违反条件的验证者被削减其权益：
- (S1) 没有验证者做出两个不同的证明 α1 和 α2 ，分别对应检查点边 s1 → t1 和 s2 → t2 ，且 h(t1) = h(t2)。
- (S2) 没有验证者做出两个不同的证明 α1 和 α2 ，分别对应检查点边 s1 → t1 和 s2 → t2，使得 h(s1) < h(s2) < h(t2) < h(t1)。
由于 Casper 是⼀种确定性⼩⼯具，⽽不是完整的协议，因此它假设底层协议有⾃⼰的分叉选择规则，并且在每个时期，所有验证者都会在某个时间点运⾏分叉选择规则以进⾏⼀次（且仅⼀次）证明。假设遵循底层协议的诚实验证者永远不会被削减。例如，如果协议要求每个时期只进⾏⼀次证明，那么诚实的验证者永远不会违反 (S1)。
Casper 定理是（略作解释）：
定理 3.2（可追究的安全）。不同分⽀上的两个检查点不可能同时被最终确定，除⾮⼀组拥有超过⼀定总数的权益的验证者可证明违反了协议（因此可以被追究责任）。
定理 3.3 （可信活性）。只要底层区块链能够创建新的区块，新的检查点就始终有可能被最终确定。
备注。 Palmskog 等⼈[17]在 Coq Proof Assistant 中为 Casper FFG 的可信赖安全性和合理活性提供了机械证明助⼿。作者修改了 Coq 中的区块链模型 Toychain，以⽤于具有以太坊信标链规范的 Casper FFG，以了解 Casper FFG 的证明在实践中如何发挥作⽤。
最贪婪最重观察⼦树规则 (Greediest Heaviest Observed SubTree, GHOST) 是由 Som-polinsky 和 Zohar [20]引⼊的⼀种分叉选择规则。直观上看，GHOST 是⼀种贪婪算法，它在“最活跃”的⼦分⽀上增⻓区块链。Zamfir [22]在寻找“构造正确”的共识协议时，引⼊了 GHOST 的⾃然改编，恰好⾮常适合我们的设置。我们将这种变体称为 最新消息驱动的最贪婪最重观察⼦树 (Latest Message Driven Greediest Heaviest Observed SubTree, LMD GHOST)，我们可以在了解权重概念后对其进⾏定义：
定义 3.4。 给定⼀个视图 G，让 M 为最新证明集，每个验证者⼀个。权重 w(G, B, M) 定义为验证者 i 的权益之和，这些验证者在 M 中的最后⼀份证明是给 B 或 B 的后代的。
图 3：LMD-GHOST 分叉选择规则⽰例。每个区块 B 中的数字是权重（按权益计算），在我们的⽰例中，所有证明（圆圈）的权重均为 1。使⽤此视图的验证者将得出蓝⾊链为规范链的结论，并输出左侧最新的蓝⾊区块（权重为 3）作为链的头部。
LMD GHOST 的理念是，在任何分叉处，我们都使⽤该分叉所创建的⼦树的权重作为启发式⽅法，并假设权重最⼤的⼦树是“正确”的⼦树，这从算法的名称就可以看出来。我们最终总会到达⼀个叶块，它定义了⼀个规范链。参阅图 3 的图形可视化。在[22] 中， LMD GHOST 与特定协议绑定。我们在本⽂中的介绍将证明的具体内容视为协议需要填写的细节，就像 Casper 没有指定区块构造的细节⼀样。我们只需要存在区块和证明的概念，然后 LMD GHOST 定义⼀种算法来根据视图查找区块。在第 4 节中，我们将修改规则以满⾜我们的其他⽬的。