[inaseer]

This is a good callout. P language evolved into the P# framework (as opposed to a language) which then evolved into Coyote (https://microsoft.github.io/coyote/)

Coyote allows developers to systematically test concurrency expressed through .NET async/await tasks. I encouraged my team to embrace Coyote based concurrency testing right from the start as we set out to build a new Azure service from the ground up. The results have been encouraging. The unification of the programming and modeling language is actually _quite_ useful in practice. For one, developers who aren't experts in formal methods are able to write concurrency tests fairly easily with minimal guidance. Secondly, the model and code never go out of sync as they are one and the same. The trick through which we are able to scale out these techniques to large scale software-in-the-wild is to have numerous tests, each test exercising concurrency in one set of APIs. This approach has scaled out in a decent manner. We run our entire distributed system in one process with various tests exercising concurrency and faults triggered through a focused set of APIs. We'll blog more about our usage of Coyote in the coming months.

While TLA+ is very powerful and useful, we've also found language integrated tools like Coyote to be quite effective in testing and catching concurrency bugs in real world code in Azure.