TLA+ is a formal specification language, not a model checker. There exists a mod...

ahelwer on Aug 6, 2015 | parent | context | favorite | on: Prove Raft Correct

TLA+ is a formal specification language, not a model checker. There exists a model checker called TLC which works with TLA+. There also exists an associated proof system called TLAPS; TLAPS has been used to formally prove correctness of Byzantine Paxos.

r0naa on Aug 6, 2015 [–]

Right, I have edited my original comment.