Correctness of Paxos with Replica-Set-Specific Views

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.