The language I want is a specification language (a bit like Pluscal or P) which allows me to specify distributed system behavior, then ask both correctness (liv

The language I want is a specification language (a bit like Pluscal or P) which allows me to specify distributed system behavior, then ask both correctness (liveness/safety) questions and quantitative behavior questions. I wrote a bit about it here: https://brooker.co.za/blog/2022/06/02/formal.html https://brooker.co.za/blog/2022/06/02/formal.html