Model checking is a powerful automated proof technique based on temporal logics. Model checking has become widely used in the field of hardware verification, but has also recently attracted some interest in the multi-agent community. In this talk, I will outline the theory behind the model-checking technique and it's limitations, the popular model checking tools, and the application of model-checking to multi-agent systems.