- Specification's authors: Xiaosong Gu, Hengfeng Wei, Yu Huang
- Original paper: Wei Cao, Zhenjun Liu, Peng Wang, Sen Chen, Caifeng Zhu, Song Zheng, Yuhui Wang, and Guoqing Ma. 2018. PolarFS: an ultra-low latency and failure resilient distributed file system for shared storage cloud database. Proc. VLDB Endow. 11, 12 (August 2018), 1849–1862.
- Extended modules: Integers, FiniteSets, Sequences, Naturals
- Computational models: crashes, lost/duplicated messages
- Some properties checked with TLC: Consistency, refinement mapping to Multi-Paxos
- TLAPS proofs: currently unavailable
- TLA+ files