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.
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-...