Just a tiny nitpick: there is no need to qualify TLA+ with anything (especially "raw", as "raw TLA" is already used for something else). There's TLA+ and there'

Just a tiny nitpick: there is no need to qualify TLA+ with anything (especially "raw", as "raw TLA" is already used for something else). There's TLA+ and there's PlusCal, a language that compiles to TLA+. True, TLA+ also refers to the gestalt of the TLA+ toolbox, but whether you're referring to the tools or to the language is often clear from context. E.g: "At my company we use TLA+, but we prefer writing specifications in PlusCal." "At my company we also use TLA+, but we write the specifications in TLA+."