- Specification's authors: Murat Demirbas
- Original paper: TLA+/PlusCal modeling of Synchronized Round Consensus Algorithm
- Extended modules: FinSet, Int, Seq
- Computation models: crashes
- Some properties checked with TLC: agreement, Syncterm, Term
- TLA+ files