This approach is sometimes referred to in the literature as model-based trace checking or just trace checking (e.g., see
this paper), and could, indeed, be a relatively cheap way to verify a real implementation, even of a distributed system.
However, I think that disabling state-exploration completely may result in imprecision, as usually traces contain only a partial view of the system's state so there is some nondeterminism as to the current state. Checking whether every transition in isolation satisfies the next-state relation may miss entering unreachable states, or delay detecting them to the point that their source is hard to pin and so debug. Instead, the state exploration should be pruned to only those states that match the view in the trace (although, perhaps that's what you meant by "altering the formula for future steps").
I think that a feature that lets TLC process traces offline (whether with pruned state exploration or with the less-precise next-state checking) could be a worthy project, and should be tried before the online solution you propose. I also found
this paper, which seems to discuss the online approach.
Ron