I don't remember the details, but I remember some people where comparing traces of execution between the program and the TLA+ code.

If the traces don't match, you've got a problem.