- TPaxos.tla: the specification and proof of the TPaxos.
- Paxos.tla: the specification and proof of the Paxos.
- EagerVoting.tla: a specification wit h proof that is equivalent to Voting.
- Voting.tla: a specification introduced by Lamport in paper Byzantizing Paxos by Refinement.
- Consensus.tla: a specification that implemented by Voting.
We introduce a invariant that all actions of TPaxos will remain, which constarin all messages and the state of variables in TPaxos.
