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

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).