+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.
How do Coyote and P differ?
OK, but then not for generating production code?
I thought I read that somewhere, but now I can't find the claim