I use PlusCal and TLA+ for different things. TLA+ shines in almost every area, with one huge hole: sequential algorithms (or communicating sequential processes) are a PAIN to specify - you have to keep track of which "instruction" you're executing in each process, and it's a ton of boilerplate. TLA+ works best when the interacting state machines you're specifying are individually small but emergently generate extremely complicated behavior. PlusCal patches this hole perfectly by letting you write the logic in pseudocode and transpiling it to TLA+, taking care of all the boilerplate.
I think Hillel has said people find PlusCal easier to understand off the bat, but I don't recall exactly where he said that. In the Amazon TLA+ whitepaper (https://lamport.azurewebsites.net/tla/formal-methods-amazon....) different engineers found TLA+ or PlusCal easier to learn.
> different engineers found TLA+ or PlusCal easier to learn
That continues to be my experience. It varies both by engineer, and (as you point out) domain. Also, as I said in a sibling comment, it’s also important to think about what people want to read, because models are extremely useful formal documentation of protocols and interactions.
Source: I’m one of the authors of that Amazon paper.
I think Hillel has said people find PlusCal easier to understand off the bat, but I don't recall exactly where he said that. In the Amazon TLA+ whitepaper (https://lamport.azurewebsites.net/tla/formal-methods-amazon....) different engineers found TLA+ or PlusCal easier to learn.