[dwohnitmok]

In theory (no pun intended) yes.

In practice this is not done. Perhaps never done. I know of only one toy example that you could maybe extend to do this. TLA+ is meant to double-check design level questions and intuitions rather than code level or implementation level ones. That is it attempts to give guidance on whether a design is flawed rather than whether an implementation successfully follows a specified design.

This may sound limiting, but the fact that this is an artifact completely separate from code makes TLA+ much more attractive from a business risk perspective in my opinion.