First Formal Proof of Keeta's Consensus: Safety Holds, But Lockout Looms
Modeling and Verification of Keeta's Consensus [pdf]
Keeta's two-phase consensus algorithm, described informally in its whitepaper, has now been formally specified in Quint and model-checked with TLC under Byzantine faults. The model proves agreement is preserved for a fixed set of equally weighted representatives, and argues the guarantee generalizes. However, it also reveals conditions where a contended account can be permanently locked out. The live, stake-weighted voting remains unverified.
Without such an analysis, the correctness of the protocol cannot be established beyond reasonable doubt, and any deployment of Keeta in real financial infrastructure is based on unverified assumptions.