paxosstore-tla TLA model checking and TLAPS theorem proving for the Paxos implementation in PaxosStore by WeChat See the PaxosStore@VLDB2017 paper and the open-source Tencent/paxosstore.