TLC has for years had a mode in which it checks that a
behavior satisfies the spec. (I expect that the states have to be
specified in the restricted subset of TLA+ that TLC uses to write out
traces.) However, I don't know of it actually being used by any
engineers, so I wonder how useful it is in practice. However, it
should make implementing what you want to do pretty straightforward.