PaxosStore is a highly available distributed storage system developed by Tencent Inc. to support the comprehensive business of WeChat. PaxosStore employs a variant of Paxos which is a classic protocol for solving distributed consensus. It is called as TPaxos in this study. The originality of TPaxos lies in its “uniformity”: it maintains a unified state type for each participant and adopts a universal message format for communication. However, this design choice brings various differences between TPaxos and Paxos, rendering TPaxos hard to understand. Moreover, although the core code (including both pseudocode and source code in C++) for TPaxos is publicly available, there still lacks a formal specification of TPaxos. Finally, as far as literature demonstrates, TPaxos has not yet been manually proven or formally checked. To address these issues, three main contributions are expounded in this paper. First, it is demonstrated that how to derive TPaxos from classic Paxos step by step. Based on this derivation, TPaxos can be regarded as a natural variant of Paxos and is much easier to understand. Second, TPaxos in TLA+, a formal specification language, is described. In the course of developing the TLA+ specification for TPaxos, a crucial but subtle detail is uncovered in TPaxos which is not fully clarified. That is, upon messages, do the participants (as acceptors) make promise that no proposals with smaller proposal numbers will be accepted before accepting proposals or vice versa? This leads to two different interpretations of TPaxos and motivates authors to propose a variant of TPaxos, called TPaxosAP. In TPaxosAP, the participants accept proposals first, and then make promise. Third, the correctness of both TPaxos and TPaxosAP is verified by refinement. Particularly, since the known voting mechanism called Voting cannot capture all the behaviors of TPaxosAP, EagerVoting for TPaxosAP is first proposed and then the refinement mappings are established from TPaxosAP to EagerVoting and from EagerVoting to consensus. They are also verified using the TLC model checker.