[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

"Raft" : A new consensus algorithm with a TLA+ spec

Paper: https://ramcloud.stanford.edu/wiki/download/attachments/11370504/raft.pdf

TLA+ spec and informal proofs of safety : http://raftuserstudy.s3-website-us-west-1.amazonaws.com/proof.pdf

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[1].
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 specification 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 [19] 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 [3]. However, this version relies on invariants whose proofs have not been mechanically checked
(for example, we have not proven the type safety of the