Re: Why Amazon Chose TLA+

[ernie...@xxxxxxxxx]

With (interesting program) = Paxos, I intended "specification of (interesting program)" to mean consensus. You can use TLC to check that any model - even Liskov-Paxos - implements consensus without having to invent a refinement map. What you can't do is check that it implements Paxos (except for those cases where it does so fairly directly). 

It makes sense for someone trying to prove the correctness of Liskov-Paxos to prove that it implements Paxos. It doesn't make sense for someone who wants to check Liskov-Paxos to check that it implements Paxos, when you could instead just check that it implements consensus.