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 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 different from Paxos in many aspects. This study provides a formal specification of TPaxos, establishes a refinement relation between TPaxos and Paxos, and verifies the correctness of TPaxos with the TLA+ proof system and the TLC model checker. (In Chinese.)