Parallel-Raft-TLA 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