Live modeling is the ability to change an executable model at run-time, and without having to restart its execution. Even though sometimes this ‘breaks’ the ongoing execution, in many cases, it does not have to. In earlier work, we reduced this problem to detecting fine-grained read-write conflicts between edit operations (created by the user) and execution steps (created by the interpreter). In this paper, we extend our approach by adding the the ability to perform model checking during live modeling sessions. We motivate that this further enhances the live modeling experience, producing counter-examples or ‘witness traces’ relative to the current execution state, as a possible `future’, integrated with the execution and edit history, minimizing the mental gap. The model checker itself is generic, and uses (via an adapter) the language’s existing interpreter. This way, we could implement this paper’s running example in a working prototype with relatively little effort.