This is, incidentally, one of the kinds of use cases that informed part of our product functionality. 1. A way to write down fairly complicated system/behavior

This is, incidentally, one of the kinds of use cases that informed part of our product functionality. 1. A way to write down fairly complicated system/behavior-level specs for distributed systems. 2. A way to instrument implementations to get the necessary signal out of the system to verify it nominally. 3. A way to automatically explore adverse conditions to validate that the system keeps behaving as needed and specifically isolate contributing factors for when it doesn't. The very first prototype was leveraged (in-part, as there was much more too the system under test) in a consensus mechanism that was central to the correct, stable, and most importantly... safe... operation of some critical software infrastructure. It was necessary to try to explore where the model assumptions broke down in practice in a real system.