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

[Chris Newcombe <chris.n...@xxxxxxxxx>]

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.

Chris

[1]

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

specification).