Correctness proofs of classic Paxos and Fast Paxos I am reading the "Fast Paxos" paper by Leslie Lamport and get stuck with the correctness proofs of both classic Paxos and Fast Paxos.

For consistency, the value $v$ picked by the coordinator in phase $2a$ in round $i$ should satisfy


  $CP(v,i):$ For any round $j &lt; i$, no value other than $v$ has been or might yet be chosen in round $j$.




For classic Paxos, the proof (Page 8) is split into three cases: $k &lt; j &lt; i$, $j = k$, and $j &lt; k$, where $k$ is largest round number in which some acceptor has reported to the coordinator by phase $1b$ message. I failed to understand the argument for the third case:


  Case $j &lt; k$. We can assume by induction that property $CP$ held when acceptor $a_0$ voted for $v$ in round $k$. This implies that no value other than $v$ has been or might yet be chosen in round $j$. 


My question is:


  
  Why can we assume that property $CP$ held when acceptor $a_0$ voted for $v$ in round $k$? 
  
  
  It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?




For Fast Paxos, the same argument (Page 18) goes on. It says,


  Case $j &lt; k$. For any $v$ in $V$, no value other than $v$ has been or might yet be chosen in round $j$. 


My question is:


  
  How is this obtained? In particular, why is "For any $v$ in $V$" here?
  
  
  In my opinion, the correctness proof of the case $j &lt; k$ relies (recursively) on those of cases of $k &lt; j &lt; i$ and $j = k$.   
  
  Therefore, how can we conclude the case $j &lt; k$ without first proving $j = k$ completely (namely, missing the subcase of $j = k$ where $V$ contains more than one value)?
Why can we assume that property CP held when acceptor a0 voted for v in round k? It seems that we are using mathematical induction, therefore, what are the basis, inductive hypothesis, and inductive steps?


You're looking at an instance of strong induction. In simple induction you assume the property holds for $n=m$ and prove it holds for $n=m+1$. In strong induction you assume the property holds for $\forall n: n&lt;m$ and prove it holds for $n=m+1$.

Basis (I believe): $j = 0$. That is, the null round (since rounds start at 1). This is trivially true, which is probably why it was not stated explicitly.

Inductive step: Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j &lt; i$.

Believe it or not, this is only a proof sketch. The real proof is in the Part Time Parliament paper. (Some consider the paper cryptic, others consider it humorous.)




  How is this obtained?
  
  In my opinion, the correctness proof of the case $j&lt;k$ relies (recursively) on those of cases of $k&lt;j&lt;i$ and $j=k$.
  
  Therefore, how can we conclude the case $j&lt;k$ without first proving $j=k$ completely (namely, missing the subcase of $j=k$ where $V$ contains more than one value)? 


This is again strong induction, so the case $j&lt;k$ does rely on the cases of $k&lt;j$ and $j=k$, but through the induction hypothesis, namely from the previous Paxos round.



General tips for Lamport's proofs.

Lamport uses a technique of hierarchical proofs. For example, the structure of the proof on pages 7-8 looks somewhat like this:


Assume $\forall n, n \le j : CP(v; n)$; prove $CP(v; j+1)$ where $j &lt; i$.

Observation 1
Observation 2
Observation 3
$k = argmax (...)$
case k = 0
case k > 0

case k &lt; j
case k = j
case j &lt; k




Lamport tends to use another type of hierarchy. He'll prove a simpler algorithm, and then prove that a more complex algorithm maps onto (or "extends") the simpler algorithm. This doesn't seem to be happening on page 18, but it is something to look out for. (The proof on page 18 appears to be a modification of the proof a pages 7-8; not an extension of it.)

Lamport relies heavily on strong induction; he also tends to think in terms of sets instead of numbers. So you may get empty sets where others would have zeros or nulls; or set unions where others would have addition.

Proving correctness of asynchronous message-passing systems needs an omniscient view of the system with respect to time. For example, when considering actions in round $i$, keep in mind that the actions for some round $j &lt; i$ may not have happened temporally!. And yet Lamport states these potentially future events in past tense.

Lamports systems and proofs tend to have a variable or set of variables that are only allowed to go in one direction; only incrementing numbers and only adding to sets. This is used extensively in his proofs. For example, on page 8 Lamport shows how he neutered the future ability of $a$ to cast another vote:


  ...Since it set $rnd[a]$ to $i$ upon sending a message, $a$ could not subsequently have cast a vote in any round numbered less than $i$....


It's definitely a brain-stretcher to prove these kinds of systems.

(update): List out the invariants; Lamport uses a lot of invariants when developing and his proofs. They are sometimes scattered throughout the proofs; sometimes they are only present in the machine-checked proof. Reason about each invariant; why is it there? How does it interact with the other invariants? How does each step in the system keep this invariant?



Full disclosure: I hadn't read Fast Paxos until I was asked to answer this question; and only looked at the pages cited. I'm an engineer and not a mathematician; my brush with Lamport's work is based purely on the need to correctly invent and maintain large-scale distributed systems.

My answer relies heavily on my experience with Lamport's work. I have read several of Lamport's protocols and proofs; I professionally maintain a paxos-based system; I have written and proven a high-throughput consensus protocol, and again professionally maintain a system based on it (I'm trying to get my company to allow me to publish a paper). I have collaborated on an insignificant paper with Lamport, in which I met with him thrice (the paper is still pending peer review.)