A trace is basically a sequence of states. If you're using TLA+ or something built on it (quint in my case) then you can get it to dump out valid sequences that you can then compare to output produced by your implementation. You have to explicitly instrument where the implementation performs the updates, so it's not free and there's potential for error there, but it clearly signals "this bit of code is responsible for that bit of the model".