uwplse/verdi-raft

Transfer-based correctness theorem for Raft is missing

Opened this issue · 0 comments

palmskog commented

From @wilcoxjay on September 22, 2015 16:51

We should prove something like "If P is an invariant of the underlying state machine, then P is an invariant of every state machine in Raft". This should follow directly from StateMachineCorrectness.

Thanks to UPenn folks for reporting!

Copied from original issue: uwplse/verdi#23