Keeta共识协议首次通过形式化验证
Modeling and Verification of Keeta's Consensus [pdf]
跨境金融结算长期受困于代理银行体系的低效与高成本。Keeta作为新兴的高性能区块链网络，采用创新的客户端导向两阶段共识算法，旨在解决这一痛点。然而，其协议此前仅停留在白皮书的非正式描述阶段，缺乏严谨的数学证明。本文首次利用Quint语言和TLC模型检查器，对Keeta的两阶段共识进行了形式化建模与验证。研究在拜占庭容错模型下证实了算法在特定条件下的安全性，同时揭示了在特定竞争场景下账户可能陷入永久锁定的风险。这一机器可验证的模型不仅填补了理论空白，也为未来金融基础设施的可靠性提供了关键参考。
共识算法构成了区块链系统的安全与可靠性基石——一个微小的缺陷就可能导致双重支付或交易永久停滞。
- rkeene2
Keeta 开发者在此。我认为我们在代码执行方面的处理方式将与 Sui 有显著不同，无论是针对有状态还是无状态的执行。
- dlahoda
> 客户端负责管理冲突，并在必要时重新提交交易。
“胖”客户端需要同时与多个“RPC”通信，并在其交易的“两阶段”提交中获得最终投票。
客户端类似于 Proposer Builder Separation 中的 Builder。
每个代表节点存储所有账户的所有数据。它们负责 DA。
- xescure
Keeta 是一个新的高吞吐量支付区块链。其起源可追溯至无费用的 DAG DLT Nano 以及 Facebook 的 FastPay，但它有许多值得正式审视的创新贡献。
在此，我提出了其共识协议的正式 Quint 规范，并在拜占庭容错模型下进行了模型检测。结果显示，在故障边界内及恒定权重模型下，安全性得以保持，且 FastPay 风格的锁定问题也如预期般被复现。
未来的研究方向取决于 Keeta 的走向；检查点和纪元（类似于 Sui）是那里需要关注的特性。
前置论文：https://keeta.com/whitepaper.pdf
Google 营销垃圾：https://cloud.google.com/blog/topics/financial-services/how-...