- Specification's authors: Siyuan Zhou
- 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: NeverRollbackCommitted
- TLA+ files