My team at AWS has been using P heavily for modelling and reasoning about distributed storage and database protocols and designs. I'm a big fan. The sweet spot for P in my mind comes from the fact that it's a much more approachable language, and mental model, than TLA+ (or Pluscal) for most programmers. That means that folks can pick up formal verification more easily, and then expand into tools like TLA+ or Dafny as their needs change.
I find myself reaching for P when, in the past, I would have reached for Pluscal. TLA+ is still my go-to for more "conceptual" problems, but I find the state machine model in P perfect for cloud systems work.
Ankush Desai did a great talk at HPTS'22 about P, and finding critical distributed systems bugs early: http://hpts.ws/papers/2022/HPTS2022.pdf He's also been working on some very interesting new directions for the verifier, and for closing the gap between specification and implementation for systems that are specified using P.
They've also developed a library that plugs into their actual Rust code to verify it (rather than writing a secondary model in TLA+ or P, it's easier to verify the actual system source code).
I find myself reaching for P when, in the past, I would have reached for Pluscal. TLA+ is still my go-to for more "conceptual" problems, but I find the state machine model in P perfect for cloud systems work.
Ankush Desai did a great talk at HPTS'22 about P, and finding critical distributed systems bugs early: http://hpts.ws/papers/2022/HPTS2022.pdf He's also been working on some very interesting new directions for the verifier, and for closing the gap between specification and implementation for systems that are specified using P.