Modeling and Verification of Keeta's Consensus [pdf]

Modeling and Verification of Keeta’s Two-Phase Consensus Protocol xescure xescure@xescu.re 2026 Cross-border financial settlement remains slow and costly, with structural inefficiencies rooted in the correspondent banking sys- tem.

Keeta is a recently released blockchain network designed for high-volume global payments, employing a novel two-phase client-directed consensus algorithm. Despite its promise, the al- gorithm has only been described informally in a whitepaper and has not been subject to formal analysis. This paper presents the first formal specification of Keeta’s two-phase consensus algorithm, written in Quint and model-checked with TLC under a Byzantine fault model. It establishes that the algorithm preserves agreement under a fixed, equally weighted set of representatives, argues that this safety guarantee generalizes to any number of representatives, and exhibits conditions under which a contended account can be driven into a permanent lockout. Whether agreement survives Keeta’s live, stake-weighted voting is left open. The resulting model is machine-checkable and serves as a reusable artifact for future research.