Keeta共识协议首次通过形式化验证

Modeling and Verification of Keeta's Consensus [pdf]

跨境金融结算长期受困于代理银行体系的低效与高成本。Keeta作为新兴的高性能区块链网络，采用创新的客户端导向两阶段共识算法，旨在解决这一痛点。然而，其协议此前仅停留在白皮书的非正式描述阶段，缺乏严谨的数学证明。本文首次利用Quint语言和TLC模型检查器，对Keeta的两阶段共识进行了形式化建模与验证。研究在拜占庭容错模型下证实了算法在特定条件下的安全性，同时揭示了在特定竞争场景下账户可能陷入永久锁定的风险。这一机器可验证的模型不仅填补了理论空白，也为未来金融基础设施的可靠性提供了关键参考。