Automated verification of discrete-state systems has been a hot topic in computer science for over 35 years. The idea found its way into AI and multi-agent systems in late 1990’s, and techniques for verification of such systems have been in constant development since then. Model checking of temporal, epistemic, and strategic properties is one of the most prominent and most successful approaches here. In this course, we present a brief introduction to the topic, and mention relevant properties that one might like to verify this way. Then, we describe some very recent results on incomplete model checking algorithms and model reductions, which can potentially lead to practical solutions for the notoriously hard problem. We conclude by a presentation of the experimental tool for verification of strategic ability, being developed by our research group at the Polish Academy of Sciences. [The course features advanced content presented with introductory attitude. If needed, we can change the proposal to a foundational course, focusing on formal semantics and fundamental theoretical results, as discussed with the organizers.