我们很高兴地分享我们的团队已经形式化验证了 AleoBFT 共识协议！
我们现在有一个形式化证明，在 AleoBFT 中，不同验证者的区块链“永远不会分叉”。
这很重要，因为大多数协议使用固定或很少变化的委员会，而 AleoBFT 支持“动态委员会”。
形式化验证是用数学方法去证明系统是可行且无BUG的，用数学语言描述清楚要解决的问题。通过对问题建立数学模型，限定系统在不同时刻应该有的状态，以及不应该有的状态。然后用这些数学规则去限定系统的设计以及实现。形式化验证方法主要包括定理证明、模型检验和模型等价性验证。
https://provable.com/blog/creating-aleobft-formal-verification-milestone
AleoBFT 是 Aleo 区块链的拜占庭容错 (BFT) 共识协议，在snarkOS（大部分）和snarkVM（某些功能）中实现。AleoBFT 基于Narwhal和Bullshark，并扩展了带有权益的动态委员会。作为我们将形式化验证技术应用于 AleoBFT 的持续努力的一部分，我们很高兴地宣布完成了一个重要的里程碑：
我们现在有一个带有动态委员会的 AleoBFT 形式模型，以及一个形式化证明，即在该模型中，不同验证者的区块链永不分叉，即所有验证者都提交相同的数据。这个结果超越了具有静态委员会的 Bullshark 的类似属性；动态委员会是一个重要的扩展，其正确性乍一看并不明显。
但这到底有什么关系呢？接下来又该怎么做呢？
快速回顾：什么是 BFT 共识协议
BFT 共识协议旨在确保验证者网络在状态上达成共识，前提是足够数量的验证者正确遵循协议。例如，在 Bullshark 中，在 n = 3f+1 个验证者中，只要至少 2f+1 个验证者行为正确，许多期望的属性就会成立，例如区块链不会分叉。
我们在形式化验证工作中了解到的一个微妙之处是，上述 2f+1 界限主要依赖于 n 具有 3f+1 形式的假设。然而，这并不是一个完全普遍的假设，因为在实际系统中，n 可能并不总是具有这种形式，另外两种可能性是 3f+2 和 3f+3。对于一般数量的验证者 n，正确的最小正确验证者数量为 nf，其中 f 是严格小于 n/3 的最大整数。
动态委员会的必要性
Bullshark 最初的构建考虑了静态委员会。然而，直觉上，这听起来不太现实。组织和社会在变化，如果我们期望相同的实体永远负责维护加密货币网络的完整性，那注定会失败。一种解决方法是定期使用受信任的协调员，或依靠网络社区的善意，来决定“权力过渡”并确定新的验证者。然而，一旦这成为一个值得信赖的过程，我们就失去了分布式共识算法的真正魔力。一种更灵活的解决方案是在协议中构建动态更改验证者的能力。
如果您查看其他流行的共识算法，例如比特币的工作量证明、Chia 的空间和时间证明或以太坊的权益证明，就会发现动态验证器集是游戏的名称。考虑到这一点，AleoBFT 诞生了，这是一种共识算法，它提供了强大的一致性保证，同时支持动态委员会变更。
在 AleoBFT 中，委员会由一个或多个验证者组成，每个验证者都拥有一定数量的股份；在协议执行期间，某些决策取决于该股份。从Aleo 主网启动时已知的创始委员会开始，验证者通过特定类型的交易进行绑定和解除绑定，这些交易与其他类型的交易混合在一起，全部提交到区块链。这使得 AleoBFT 委员会非常动态，可能在每个区块上都发生变化，其中协议每两轮就会产生一个新区块。由于验证者不会同时提交所有区块（它们可能彼此领先或落后），因此验证者很难或导致无法容忍的延迟，因为总是就最新区块产生的委员会达成一致，并使用该委员会在下一轮达成共识。因此，AleoBFT 使用了一种创新的回顾方法，通过这种方法，负责下一轮的委员会不是来自上一个区块，而是来自过去固定数量的轮次（目前为 100 轮）。换句话说，验证者的绑定或解除绑定与其开始或结束参与达成共识之间存在“延迟”（100 轮）。（为了简洁起见，对回顾和动态委员会的解释略有简化，但给出了总体思路。）
ACL2 形式化
我们的 AleoBFT 形式化模型和证明是用 ACL2 定理证明器编写的；它们可作为ACL2 及其库的 GitHub 存储库的一部分使用。我们形式化将 AleoBFT 建模为标记状态转换系统，其状态由验证器和连接它们的网络组成，其转换描述了验证器内部状态和网络的变化，后者以验证器之间交换的消息的形式出现。我们通过系统可达状态上的许多不变量形式化证明了区块链的非分叉。这些不变量很复杂，其中一些是相互依赖的：
特别是，区块链的一致性（即非分叉）取决于区块链完全有序的部分有序证书的非歧义性，这些证书的非歧义性取决于验证器同意负责这些证书轮次的委员会，而委员会是根据区块链计算出来的，因此必须达成一致。我们的顶级归纳证明确保这些相互依赖关系在归纳上是格式良好的，并且不存在循环推理。
这种方法让我们确信，委员会在某一轮/某一区块完全可以改变：
只要在每一轮（签名者、选民和前任）使用正确的委员会做正确的事情，协议仍然可以正常工作，这是非常了不起的。
一些强制性的细则
和所有形式化验证的用途一样，强调哪些已经得到形式化证明，哪些尚未得到形式化证明非常重要。我们已经在 AleoBFT 形式化模型中形式化证明了非分叉性，该模型是我们在仔细检查 snarkOS 和 snarkVM 中 AleoBFT 实现的基础上构建的。我们尚未形式化证明 snarkOS 和 snarkVM 的正确性。即便如此，snarkOS 和 snarkVM 模型的形式化证明比仅仅测试和非形式化推理提供了更高的保证。
从回顾委员会到展望未来
我们将继续在各个方向开展形式化验证工作。一个直接的方向是将我们的模型和证明从使用验证者数量作为 n 和 f 推广到与验证者相关的质押。我们还计划形式化研究 AleoBFT 的其他属性，特别是与活性相关的属性。
我们正在撰写一篇学术论文，描述我们的形式化模型和区块链不分叉的证明。我们欢迎您关注我们的工作、提出问题，甚至可以说与我们合作，帮助使现代共识实现越来越强大。
ZKT Aleo ZPU 芯片机 ，现正式开启第一批头矿预售！
2024 年全球 ZK 峰会 Aleo-ASIC 最有竞争力品牌！
感兴趣请扫码联系，ZKT ASIC 仅对大客户和大渠道！
转载：ZKTo完成Aleo专用ZPU芯片FPGA与PooL联调测试
Aleo主网后PoSW数据全面分析汇总(10/28/2024)
什么是SNARK？什么是Varuna SNARK？与ZK-SNARK有什么区别？
ALEO 问答集锦 | 关于质押者、证明者和验证者官方最新解答
ALEO 问答集锦 | Aleo积分到底有什么用？区块奖励重大变化？
