Paxos Made Simpler
In Paxos Made Simple, Leslie Lamport presented the Paxos algorithm in an intuitive way by starting from intuitions and then trying to fulfill the requirements. While it reflects how Paxos is invented, things can be made simpler if we think in reverse when proving its correctness.
The correctness of Paxos consists of safety and liveness. Since liveness can be achieved by electing a distinguished proposer, we only focus on safety.
The Paxos Algorithm

Phase 1.

(a) A proposer selects a proposal number \(n\) and sends a prepare request with number \(n\) to a majority of acceptors.

(b) If an acceptor receives a prepare request with number \(n\) greater than that of any prepare request to which it has already responded, then it responds to the request with a promise not to accept any more proposals numbered less than \(n\) and with the highestnumbered proposal (if any) that it has accepted.


Phase 2.

(a) If the proposer receives a response to its prepare requests (numbered \(n\)) from a majority of acceptors, then it sends an accept request to each of those acceptors for a proposal numbered \(n\) with a value \(v\) , where \(v\) is the value of the highestnumbered proposal among the responses, or is any value if the responses reported no proposals.

(b) If an acceptor receives an accept request for a proposal numbered \(n\) , it accepts the proposal unless it has already responded to a prepare request having a number greater than \(n\).

Requirements
To prove safety, we prove requirement \(P2\). Other requirements are intermediate.

\(P1^a\). An acceptor can accept a proposal numbered \(n\) iff it has not responded to a prepare request having a number greater than \(n\).

\(P2^c\). For any \(v\) and \(n\), if a proposal with value \(v\) and number \(n\) is issued, then there is a set \(S\) consisting of a majority of acceptors such that either (a) no acceptor in \(S\) has accepted any proposal numbered less than \(n\) , or (b) \(v\) is the value of the highestnumbered proposal among all proposals numbered less than \(n\) accepted by the acceptors in \(S\).

\(P2^b\). If a proposal with value \(v\) is chosen, then every highernumbered proposal issued by any proposer has value \(v\).

\(P2^a\). If a proposal with value \(v\) is chosen, then every highernumbered proposal accepted by any acceptor has value \(v\).

\(P2\). If a proposal with value \(v\) is chosen, then every highernumbered proposal that is chosen has value \(v\).
Proof

Paxos > \(P1^a\).
Trivial from Phase 2(b).

Paxos > \(P2^c\).
Trivial from Phase 1(b) and Phase 2(a).

\(P2^c\) and \(P1^a\) > \(P2^b\).
Prove by induction. For any \(n > m\), assuming a proposal with number \(m\) and value \(v\) is chosen, and any proposal with number \(m, \cdots, n  1\) has value \(v\), we prove any proposal with number \(n\) has value \(v\).

For the proposal with number \(m\) to be chosen, there must be a quorum \(C\) of acceptors such that every acceptor in \(C\) accepted it. (This is the definition of chosen.)

For any proposal with number \(n\) to be proposed, there must be a quorum \(C\)’ of acceptors such that every acceptor in \(C\)’ responded with the highestnumbered proposal (or no proposal) to the prepare request. (The algorithm flow says the proposer must receive a majority of responses to prepare requests before proposing.)

Quorum \(C\) and \(C’\) have at least one acceptor in common. From above analysis, two events have happened to this acceptor: accept(m) and respond(prepare_n). Since \(m < n\), accept(m) must happen before respond(prepare_n) (due to \(P1^a\)). Therefore, the response to prepare_n must contain a proposal with number at least \(m\).

Now it’s guaranteed that the proposer of a proposal numbered \(n\) gets a response with a proposal numbered at least \(m\). So proposals numbered less than \(m\) in other responses will not be used (since the proposer uses the highestnumbered proposal in Phase 2(a)). The proposer may use values from proposals numbered \(m, \cdots, n  1\). But from the induction basis, they all have the same value \(v\).

Therefore, the proposal with number \(n\) has value \(v\). And by induction, any proposal with number \(n > m\) has value \(v\).


\(P2^b\) > \(P2^a\).
Trivial. A proposal must be proposed before accepted.

\(P2^a\) > \(P2\).
Trivial. A proposal must be accepted before chosen.