Read the PDF Markdown Quint model
Cross-border financial settlement remains slow and costly, with structural inefficiencies rooted in the correspondent banking system. 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 algorithm 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.
f Byzantine
representatives, and does that guarantee extend beyond the checked configurations?Keeta, consensus algorithms, formal verification, Quint, TLA+, Byzantine fault tolerance, blockchain, DAG, distributed ledger technology
xescure. 2026. Modeling and Verification of Keeta’s Two-Phase Consensus Protocol. https://xescu.re/keeta-consensus/