Nice write-up. It's good they use Raft given the formal methodists are doing a ton of work on verified implementations. Recent example using Verdi where it's verified plus performance-competitive:
Likewise with 2 phase. Lots of analysis out there. Building on such proven protocol designs will help them out in long run to get where they want to be.
http://verdi.uwplse.org/raft-proof.pdf
Likewise with 2 phase. Lots of analysis out there. Building on such proven protocol designs will help them out in long run to get where they want to be.