Abstract

We present a specification and proof of correctness for the Paxos replicated state machine consensus protocol in which replica-set-change is implemented with replica-set-specific views.

‚Äč