It looks like Coyote[0], which is used in azure, was an evolution of P# which was an evolution of P
[0]https://www.microsoft.com/en-us/research/wp-content/uploads/...
+1.
We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.