AI software – both symbolic and connectionist – pervasiveness in our societies is a fact. Its very dissemination raises important questions from the perspective of software engineering. As AI software malfunctions have dire consequences on individuals and societies, it is expected that AI software will aim for high software quality. The field of formal methods successfully transferred techniques and tools into some of the most critical industries. The goal of this course is to provide an accurate perspective of formal methods applied to AI software. Following real-world industrial examples, we will present how the use of formal methods can help AI developers assess the quality of their software, ranging from adversarial robustness to automated neural network fixing and explainable AI with guarantees.