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 pro

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.