Modeling and Verification of Keeta's Consensus [pdf]
xescure
13 points
3 comments
August 15, 2026
Related Discussions
Found 5 related stories in 42.5ms across 4,128 title embeddings via pgvector HNSW
- The Case Against Formal Verification, 50 Years Later ghuntley · 86 pts · August 16, 2026 · 45% similar
- Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code permute · 108 pts · July 28, 2026 · 44% similar
- Show HN: Reproducibility Benchmark a Risk Quantitative Model mingshi_tz · 11 pts · July 26, 2026 · 43% similar
- Coordination Without Consolidation: On Systems of States [pdf] brandonlc · 20 pts · July 09, 2026 · 40% similar
- GulliBench: Measuring Skepticism in Frontier Models rigelbm · 18 pts · August 12, 2026 · 39% similar
Discussion Highlights (3 comments)
xescure
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-...
rkeene2
Keeta developer here. I think the way we handle execution of code will be significantly different from Sui, both for stateful and stateless executions.
dlahoda
> Clients are responsible for managing conflicts and resubmitting transactions if necessary. "Fat" clients need to talk to many "RPC"s at once and get final vote on "two phase" commit to their transaction. Client is like Builder in Proposer builder separation. Each representative stores all data for all accounts. They do DA.