I've actually built something like this for TLA+ and C#, which I call Kayfabe. I'll hopefully present it this October at the next TLA+ conference. High-level,

I've actually built something like this for TLA+ and C#, which I call Kayfabe. I'll hopefully present it this October at the next TLA+ conference. High-level, there are two modes: 1. Checking execution traces from running code against the model (see notpron's work for this idea) 2. Outputting every state visited by the model checker in a finite instantiation, then computing paths to step the real C# through so it'll visit every state or transition at least once. This is very, extremely computationally expensive, but I'm running real code in prod that I've tested this way. Hopefully I can get my algorithms to be efficient and if so I'll try to open-source my efforts.