Right. In addition, you miss out on the notion of refinement (ordinary implication in TLA+) which is the most powerful (and most foundational) idea of the forma

Right. In addition, you miss out on the notion of refinement (ordinary implication in TLA+) which is the most powerful (and most foundational) idea of the formalism. But I think many developers may be threatened by the unfamiliarity of TLA+, and PlusCal serves as a gateway drug, as it's often useful enough on its own (you're right that you need to know at least a bit of TLA+ to understand some of the tooling's output). If "PlusCal first" makes TLA+ less threatening and hopefully more approachable to many developers, then the approach is doing its job. (BTW, I wouldn't call it "raw TLA+" as "raw TLA" is a particular logic that Lamport uses to introduce TLA, so the term may be confusing.)