Model checking is used to verify the correctness of digital circuits and code against their formal specification. In case of design or programming errors, it provides a counterexample evidence of erroneous behavior. We describe here model checking and two related techniques: black box checking and runtime verification. Black box checking is a variant of model checking where the description of the system is not given apriory, but we can interface with the system via experiments. Runtime verification checks a current execution against the specification. The common ground for the presentation of these methods is the use of automata theory for both modeling the system and representing the specification.