/paxosstore-tla

TLA+ model checking and TLAPS theorem proving for the Paxos implementation in PaxosStore by WeChat

Primary LanguageTLAMIT LicenseMIT

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.