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.
I thought I read that somewhere, but now I can't find the claim