- Specification's authors: Xingchen Yi, Hengfeng Wei
- Original paper: Zheng, Jianjun, et al. PaxosStore: high-availability storage made practical in WeChat. Proceedings of the VLDB Endowment. 2017.
- Extended modules: Integers, FiniteSets
- Computation models: crashes, lost/duplicated messages
- Some properties checked with TLC: Consistency
- TLA+ files