[colanderman]

Learn it on your own first before trying to foist it on others. I'm on the cusp of seriously introducing use of TLA+/PlusCal at the startup I'm at, and having worked through (and had success with) modeling a couple real-word concurrent systems I have designed here, I have a very different perspective how to use TLA and explain it to co-workers than when I first started using it.

(For example: it's tempting to think of variables as some sort of communication channel – they're not. And fairness can be hard to conceptualize until it's put to a real-world use.)

Definitely use PlusCal. It's a little more to learn, and a little more restrictive, than straight TLA+, but most TLA+ specs you write will end up looking like the output of PlusCal anyway, and the PlusCal version will be much more compact and easy-to-follow. Just remember that PlusCal is not like any other programming language; especially the "await" statement can throw newcomers off (it's not like "await" in other languages).