verdi-raft icon indicating copy to clipboard operation
verdi-raft copied to clipboard

Published 20 hours ago • verified publisher icon uwplse

Transfer-based correctness theorem for Raft is missing

Open palmskog opened this issue 7 years ago • 0 comments

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

palmskog avatar May 21 '17 03:05 palmskog