Mathematics of Consensus — Accidental Lecture

Alex from TigerBeetle is teaching his colleague Tobi, who understands set theory but not consensus algorithms, about the mathematics of consensus using set theory. They plan to construct a consensus algorithm from scratch, using trial and error to fix errors until it works. They define discrete systems evolving over time, using a state space S and behaviors as infinite sequences of states. They discuss specifying behaviors with initial state predicates and state transition predicates, and then move on to defining a correctness predicate to specify desired system behaviors. They then discuss the consensus theorem, and implement systems that hopefully obey the definition. They start with a simple consensus system and then make it distributed, discussing voting, autocracy, and combining the two. They address the issue of democratic voting getting stuck and propose a solution involving each person being a dictator for a day. They refine the approach to ensure a single value is chosen and introduce the concept of safe values to prevent contradictions, ultimately arriving at a consensus algorithm.