> we also sought a language that would allow us to model check (and later prove) key aspects of systems designs while being more approachable to programmers.

I find it a bit surprising that TLA+ with PlusCal can be challenging to learn for your average software engineer, could anyone with experience in P show an example of something that can be difficult to express in TLA+ which is significantly easier in P?