[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
"Raft" : A new consensus algorithm with a TLA+ spec
The main motivation seems to have been to find a consensus algorithm that is easier to understand than Paxos.
They do give some statistical results of quizzing a group of students on both algorithms. They don't give defect-rates from any implementations.
The authors say they have a formal TLAPS proof of some parts.
I could not find that proof online, in a few minutes of searching.
The safety proof shows invariants that hold in every
state of every execution that the speciﬁcation allows. Its
main lemma states that a leader only marks a log entry
committed if every subsequent leader must also have this
entry. (Safety follows easily from this lemma.) We have
an informal proof  for Raft which is relatively precise and complete (about 9 pages or 3500 words long).
We also have a mechanically-checked version of the main
lemma and other portions of the proof using the TLA
proof system . However, this version relies on invariants whose proofs have not been mechanically checked
(for example, we have not proven the type safety of the