Comment by hwayne

The universal problem is "generating code from a formal spec" is extremely, maddeningly, pull-your-hair-outingly hard. A slightly easier thing, as you said, generating test cases, which is what the Mongo people have been advancing: https://arxiv.org/abs/2006.00915

(Another interesting approach in this space is P, which is lower-level than TLA+ but also can compile to C#: https://github.com/p-org/P)