- Specification's authors: Diego Ongaro
- Original paper: Ongaro, Diego, and John K. Ousterhout. In search of an understandable consensus algorithm. USENIX Annual Technical Conference. 2014.
- Extended modules: FinSet, Nat, Seq
- Computation models: crashes, lost/duplicated messages
- Some properties checked with TLC: deadlock
- TLA+ files