Yes I misspoke, but, for the purposes of the article, the GP's question, and the use to which most readers here will put TLA+, it's tied at the hip to TLC and i

Yes I misspoke, but, for the purposes of the article, the GP's question, and the use to which most readers here will put TLA+, it's tied at the hip to TLC and is used primarily for model checking.