Comment by jackdaniels4me

Lamport didn't design TLA+ for model checking or for practicing developers to use. He did purely for publishing papers where the researchers express their proofs as math (his new TLA+) instead of free form text.