I love this, and have similar feelings about PRISM. I hope recent work to add probabilistic properties to TLA+ and P provide a route towards doing this kind of

I love this, and have similar feelings about PRISM. I hope recent work to add probabilistic properties to TLA+ and P provide a route towards doing this kind of work with languages that are easier to use. While this example is a bit silly, the ability to check properties like availability, latency, etc alongside the traditional liveness and safety properties is super useful for distributed systems work.