- Specification's authors: Thanh Hai Tran, Igor Konnov, Josef Widder
- Original paper: Raynal, Michel. A case study of agreement problems in distributed systems: non-blocking atomic commitment. High-Assurance Systems Engineering Workshop, 1997., Proceedings. IEEE, 1997.
- Extended modules: Nat, FinSet
- Computation models: clean crashes
- Some properties checked with TLC: validity, nontriviality, termination