In model checking, systems are modeled by finite state machines, and this finite state model is checked against a given specification. The model checking verification procedure is done by an exhaustive search of the state space of the design.

In some cases, model checking might prove to be more cost-effective than verifying a program's correctness against a formal specification.

Model checking allows for verification of both positive and negative properties. With model-checking, it is possible to deduce if a particular system execution will lead to a certain system state, or if none of a system execution will lead to another state. This type of verification will be more difficult to deduce by verifying a program's correctness against a formal requirement, thus less cost-effective.

In model checking,the analysis can be fully automated as opposed to manual checking of formal requirements to validate correctness. The specification can be expressed in a suitable language, temporal logic being a prime example, describing the permitted behaviours of a given system. Model checking provides full coverage for verification; it can examine all the possible behaviours in a single execution. It is easy to see how this can be cost-effective in some cases.