“与其不断同步整个状态，状态机复制让排序层先提供共同命令前缀，再由各副本在本地重放同一计算。它由此把“多台副本如何保持一致”分成两层：共识或原子广播负责决定顺序，执行层让确定性状态机从相同初态…”
形式陈述
共识先规定共同的单次任务接口，再由执行模型决定进程怎样交换信息。固定参与进程集合
- 完整性：每个进程至多决定一次；
- 统一一致性：任何两个已经决定的进程，即使其中一个稍后崩溃，也决定相同值；
- 提议有效性：若某进程决定
- 终止性：按已声明的进展条件完成决定；本页主消息模型要求每个正确进程最终决定。
有些文献只约束正确进程的决定，称 non-uniform agreement；有些有效性只要求全体输入相同时决定该值，或要求决定通过外部验证谓词。拜占庭模型还要决定是否只采信正确进程提议。引用“共识”结论时，必须同时给出这些版本与
完整性、一致性与有效性属于安全性：有限前缀即可见证违例。终止性是活性；在主消息模型中，证明它须使用已声明的正确进程持续取步、消息最终交付及故障预算条件。
共享内存的wait-free 共识保留上述完整性、统一一致性与提议有效性，但允许其他进程任意暂停。每个尚未决定的进程只要继续取得自己的步骤，就须在有限个自身步骤后决定；不能要求其他线程也持续运行来证明这一点。其可用原子对象与故障容忍量词应单独规定，消息网络的多数、信道可靠性或领导者条件不自动迁移过去。
直觉
每个进程只有局部消息前缀，却要作出全局唯一且不可撤销的决定。决定不要求每个节点都已知道结果：一个值可以已经获得足够证据，而另一个正确节点还在等待消息。协议必须保证后者迟到时只能学到同一值，同时证明它在允许的执行中最终能学到。
早决定可能漏掉相反提议，永久等待又违背终止。协议把安全证据做成跨轮次可继承的投票记录，并把活性押在某种最终协调条件上。轮次编号只区分尝试，不是重新开始一次独立共识；同一实例中换了领导者，旧决定仍不可撤销。
多数相交只提供证据相遇的机会。交点进程若可以在两个轮次无条件支持不同值，两个多数仍可能分别批准冲突结果；ballot、任期、锁定或继承规则才决定交点携带什么。
例子与边界
二值共识中，“总决定
三个投票者
即使
两阶段提交决定分布式事务提交或中止，prepared 参与者在协调者故障后可能阻塞。用共识复制提交决定可消除单协调者这一故障点，但 2PC 本身没有在异步 crash 模型中提供 nonblocking consensus。
FLP 不可能性说明完全异步、确定性、可靠消息且允许一次 crash 时，某个可容许调度可以永不决定。Paxos与Raft仍能在所有这类时序下保持安全；它们的终止证明另加稳定领导、可达多数与部分同步条件。拜占庭共识又需更大交集与认证假设，不能把 crash 多数公式直接搬过去。
两阶段随机共识在严格多数正确、固定不看内容的调度器下，逐步证明所有执行安全、概率一终止，并算出逻辑轮数的几何尾界；它明确区分输出决定与停止服务。
推论与应用
消息传递中，最终领导者检测器
本页消息传递实例中的 uniform 共识与原子广播的统一前缀版本，在固定成员、普通可靠广播及相同 crash/终止假设下相互归约。原子广播到共识：广播各自提议并决定第一条全序交付消息。共识到原子广播：可靠传播带唯一 ID 的完整 payload，持续参加各编号共识实例，本地无待排消息时也提议空集；决定直接给出整批内容，按固定顺序去重交付，不另等本地可靠交付。持续重提所有 pending 消息排除饥饿。详见完整归约；等价指可解性相互归约，不表示一个 one-shot 实例自动提供无限日志。
协议验证常把 agreement 化为配置上的归纳不变式，把 termination 写成对公平无限执行的性质。模型检查可以找出双决定或永不进展的调度，却不能替规格补入遗漏的公平性与故障上界。
参考资料
- Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996, Chapter 6.
- Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004，Chs. 5–6。
- Tushar D. Chandra and Sam Toueg, “Unreliable Failure Detectors for Reliable Distributed Systems,” Journal of the ACM 43(2), 1996, pp. 225–267。