信标链协议|技术贴 | 形式化验证Gasper共识机制的终局性（finalization）( 三 )
b1和b2都被终局化了（因为b1和b2都不是对方的祖先区块）。这两个区块可以是在任意合理化高度的时候被任意长的链终局化的。
这些定义和结果组中被用来指出和证明可追责的安全性、似然活性以及可罚没下限三种定理。为清楚起见，我们还用下式重新定义了可追责安全性定理的表述：
这个定义很简单，只是说：如果安全性被打破（出现了任何被敲定的分叉），那必定意味着某个验证者集合会被罚没。这个证明机械化了 Gasper 给出的非正式论证，并展示了为什么分叉获得终局化就意味一定有两个绝对多数团体违反了其中一条罚没条件，因此其交集可被罚没。
我们的技术报告描述了形式化过程以及这些属性的证明，而我们的项目代码库提供了完整的详述。
继续前进 在本文中，我们讲解了 Runtime Verification 与以太坊基金会合作成就的第一部分。这第一部分乃是（在验证者集合会动态变化的条件下）形式化 Gasper 并证明其关键的三种属性：可追责的安全性、似然活性以及可罚没下限。我们成就的第二部分，在本文中还未涉及的，是展示如何将这些结果代入更加精细的模型（用 K 框架写就）中，给出一个信标链状态转换函数的抽象版本。我们后面会用另一篇文章来展示这一成果。
完成这个里程碑还意味着我们向这场合作的终极目标（形式化地证明信标链协议满足所有三种关键属性、并能清楚地声明一个非常接近于协议详述的抽象版本所需的所有假设）迈出了重要的一步。
我们期待在这项工作上与以太坊基金会继续合作。在这次接触中，我们对以太坊基金会的几位专家深为感激：Danny Ryan、Carl Beekhuizen、Martin Lundfall、Yan Zhang 以及 Aditya Asgaonkar。
（完）
推荐阅读
- 中华人民共和国商务部 中华人民共和国科学技术部公告
- 机器人|AI训练师让机器人更聪明
- Huawei|华为推出“二郎神”智能摄像机：加入手机技术 长焦广角全覆盖
- [央视]两部门发布中国禁止出口技术最新目录，涉53项技术条目央视2020-08-29 14:15:550阅
- 马斯克|马斯克用活猪演示脑机技术，他希望今年年底前能在人体内植入
- Mix|小米发布第三代屏下相机技术，或将在Mix 4上首秀？
- 东方文化|李安：数字技术是东方文化表达的新机会
- 新浪科技■马斯克在猪身上展示Neuralink脑机接口最新技术新浪科技2020-08-29 08:06:490阅
- 《中国禁止出口限制出口技术目录》调整内容
- 技术|商务部就调整发布的《中国禁止出口限制出口技术目录》答记者问