Introduction
This article explains the leaderless consensus models as one algorithm family. It presents the progression from an intentionally naive protocol to stronger set- and prefix-based designs, with emphasis on the problem each variant addresses, the object it commits, and the safety and liveness properties established by the executable TLA++ models.
This work is a continuation of the earlier article Replicated object, part 7: masterless. The difference is that the earlier text described the ideas, while this effort carries them into checked finite models with explicit safety proofs and separate liveness checks.
The implementation is available at github.com/gridem/tlapp, and the detailed variant notes live at github.com/gridem/tlapp/tree/main/docs/leaderless-consensus.
