Modeling and Verification of Keeta's Consensus [pdf]

Keeta is a new high-throughput payments blockchain. Its origins trace back to Nano, the feeless DAG DLT, and Facebook's FastPay, but it has plenty of novel contributions which warrant a formal look.

Here I present a formal Quint specification for its consensus protocol, model-checked under a Byzantine fault model. Safety was found to be preserved within the fault-bounds and under a constant weight model, and the possibility of FastPay style lockouts was reproduced as expected.

The direction for future research depends on the direction Keeta takes; checkpoints and epochs (similar to Sui) are the features to watch there.

Prerequisite paper: https://keeta.com/whitepaper.pdf

Google marketing slop: https://cloud.google.com/blog/topics/financial-services/how-...