# Nero: A Deterministic Leaderless Consensus Algorithm for DAG-Based Cryptocurrencies
## 3 The Nero Algorithm
### Correctness  
In this section, we discuss the correctness of the Nero consensus algorithm.  
**Lemma 1**.: _There cannot be two or more valid commits with different values in a given round._  
Proof.: Since, per the consensus algorithm, a correct process never votes or commits more than one block hash in the same round in the same election, it is not possible to have two sets of \(2f+1\) of different values without at least one correct process voting for two different values, so we prove by contradiction.  
**Lemma 2**.: _If a correct process commits a value \(v\) in round \(r\) and it receives a valid commit of another value \(v^{\prime}\) in round \(r^{\prime}\), \(r^{\prime}>r\), no correct process could have decided \(v\) in round \(r\)._  
Proof.: If a correct process decides value \(v\) in round \(r\), it means that it has received at least \(2f+1\) commits with value \(v\) in round \(r-1\). Since at least \(f+1\) of those commits are from correct processes, they will not change its value and so the \(2f+1\) valid messages of value \(v^{\prime}\) of type VOTE needed to commit value \(v^{\prime}\) will not be produced. Inversely, if there was a commit of value \(v^{\prime}\), it means that value \(v\) was not decided in a previous round.  
**Lemma 3**.: _The Nero algorithm satisfies Termination._  
Proof.: We need to prove that all correct processes decide. For that, we have to prove that all correct processes eventually commit a value and then that all correct processes eventually decide a value. The proof follows from Lemmas 4 and 5.  
**Lemma 4**.: _All correct processes eventually commit a value._  
Proof.: First, we prove that at least one correct process eventually commits. Since a byzantine process can send different valid votes (with different values) to different correct processes in a given round, it is possible that no correct process commits during the non-GST phase.  
However, during the GST, all correct processes will eventually vote the same value in a given round \(r\) because they will all receive the same votes in round \(r-1\).  
**Lemma 5**.: _All correct processes eventually decide a value._  
Proof.: First, we prove that at least one correct process eventually decides, which happens because all correct processes will eventually commit the same value.  
During the GST, all correct processes will eventually decide as well since they will receive the valid commits in which the correct process based its decided value.  
**Lemma 6**.: _The Nero algorithm satisfies Agreement._  
Proof.: We need to prove that all correct processes decide the same value. Since we already proved in Lemma 5 that all correct processes eventually decide, we need to prove that they all decide the same value.  
Suppose that a correct process \(p\) decides value \(v\) in round \(r\). This means that it has received at least \(2f+1\) commits with value \(v\) in round \(r-1\). At most there are \(f\) byzantine processes, so at least \(f+1\) of those commits are from correct processes, which means that they will only change their commit if they receive a valid commit with value \(v^{\prime}\) in a round \(r^{\prime},r^{\prime}>r-1\).  
If \(r^{\prime}=r\), this cannot happen due to Lemma 1. If \(r^{\prime}>r\), for a valid commit with value \(v^{\prime}\) to happen, there needs to be at least \(2f+1\) valid votes in a previous round \(r^{\prime}-1\), which is not possible since at least \(f+1\) correct processes will not change their commit with value \(v\) in round \(r\) and vote with value \(v^{\prime}\) since \(r^{\prime}-1>=r\). Therefore, we prove by contradiction.  
Lemma 2 ensures that a correct process can change its commit to a subsequent valid commit while maintaining safety.  
**Lemma 7**: _The Nero algorithm satisfies Validity._  
Proof.: A correct process only sends messages with a valid value so only valid values can be decided.  
**Theorem 1**: _The Nero algorithm achieves a multi-valued consensus, i.e., Termination, Validation and Agreement._  
Proof.: Follows from Lemmas 3, 6 and 7.