I love P and have used it for personal projects (like OSWALD^1) and at work (for some Redpanda components).
I find it very approachable. If you know some basic theory of distributed systems and have been exposed to actors and state machines before, you should be able to have some non trivial models in a few days at days.
Things get slightly more complicated when you begin to ask yourself whether or not you have validated enough of the state space to have confidence in the design. The verifier has a much of options who care poorly documented.
Recently, P was extended to support exploring the entire state space (PEX mode) as well as a prover. These have only rudimentary documentation. I learned about them more by looking at code.
According to public information, AWS uses both and not only. AWS wrote a paper on the topic with some details about their applications of
formal methods^1. AWS is a large org though, it would be hard to generalise or reduce their approach to any single method.
I love P and have used it for personal projects (like OSWALD^1) and at work (for some Redpanda components).
I find it very approachable. If you know some basic theory of distributed systems and have been exposed to actors and state machines before, you should be able to have some non trivial models in a few days at days.
Things get slightly more complicated when you begin to ask yourself whether or not you have validated enough of the state space to have confidence in the design. The verifier has a much of options who care poorly documented.
Recently, P was extended to support exploring the entire state space (PEX mode) as well as a prover. These have only rudimentary documentation. I learned about them more by looking at code.
1: https://nvartolomei.com/oswald/
Wasn't TLA+ used by AWS previously?
According to public information, AWS uses both and not only. AWS wrote a paper on the topic with some details about their applications of formal methods^1. AWS is a large org though, it would be hard to generalise or reduce their approach to any single method.
1: https://www.amazon.science/publications/using-lightweight-fo...
Later add: I believe P creator is employed by AWS at this moment.
Ankush has moved on to Snowflake now, but he was previously at AWS.
This P is, contrary to popular belief, stored on GitHub.