使用 TLA+ 对 CBC Casper 共识算法进行形式化分析

摘要

一位 Trail of Bits 实习生用 PlusCal 和 TLA+ 形式化建模了以太坊 CBC Casper 二进制共识协议，验证其活性属性要求拜占庭容错阈值低于验证者总权重的三分之一，与 Lamport 的拜占庭将军问题结论一致。