Correctness and Fairness of Tendermint-core Blockchains
Yackolley Amoussou-Guenou (CEA, NPA, LIP6), Antonella Del Pozzo (CEA),, Maria Potop-Butucaru (NPA, LIP6, LINCS), Sara Tucci-Piergiovanni (DILS, CEA)

TL;DR
This paper formally analyzes the correctness and fairness of Tendermint-core blockchains, characterizing their system model, proving their consensus properties under certain conditions, and establishing the link between system synchrony and fair reward distribution.
Contribution
It provides the first formal system model and correctness proof for Tendermint, and establishes the conditions for fair reward mechanisms based on system synchrony.
Findings
Tendermint solves one-shot and repeated consensus under eventual synchrony with Byzantine faults.
A fair rewarding mechanism exists if and only if the system is (eventually) synchronous.
Formal analysis clarifies the assumptions and guarantees of Tendermint's consensus and reward fairness.
Abstract
Tendermint-core blockchains (e.g. Cosmos) are considered today one of the most viable alternatives for the highly energy consuming proof-of-work blockchains such as Bitcoin and Ethereum. Their particularity is that they aim at offering strong consistency (no forks) in an open system combining two ingredients (i) a set of validators that generate blocks via a variant of Practical Byzantine Fault Tolerant (PBFT) consensus protocol and (ii) a selection strategy that dynamically selects nodes to be validators for the next block via a proof-of-stake mechanism. However,the exact assumptions on the system model under which Tendermint underlying algorithms are correct and the exact properties Tendermint verifies have never been formally analyzed. The contribution of this paper is two-fold. First, while formalizing Tendermint algorithms we precisely characterize the system model and the exact…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBlockchain Technology Applications and Security · Distributed systems and fault tolerance · Optimization and Search Problems
