It's not exactly proof by exhaustion, as model checkers don't actually check all assignments, even explicit-state model checkers (because even in finite state c

It's not exactly proof by exhaustion, as model checkers don't actually check all assignments, even explicit-state model checkers (because even in finite state cases, verified propositions are about infinite behaviors; you often model-check propositions much more elaborate than "X never happens in any state"), and algorithms like DPLL for SAT model-checking don't even do explicit state visits. Rather, it is a proof in the model theory of the logic.