- Specification's authors: Michael J. Cahill, Uwe Röhm, Alan D. Fekete
- Original paper: Cahill, Michael J., Uwe Röhm, and Alan D. Fekete. Serializable isolation for snapshot databases. ACM Transactions on Database Systems (TODS) 34.4 (2009): 20.
- Extended modules: FinSet, Int, Seq
- Computation models: Write-rejection
- Some properties checked with TLC: termination, correctness
- TLA+ files