The last decade witnessed an ever-increasing stream of successes in MachineLearning (ML). These successes offer clear evidence that ML is bound to becomepervasive in a wide range of practical uses, including many that directlyaffect humans. Unfortunately, the operation of the most successful ML models isincomprehensible for human decision makers. As a result, the use of ML models,especially in high-risk and safety-critical settings is not without concern. Inrecent years, there have been efforts on devising approaches for explaining MLmodels. Most of these efforts have focused on so-called model-agnosticapproaches. However, all model-agnostic and related approaches offer noguarantees of rigor, hence being referred to as non-formal. For example, suchnon-formal explanations can be consistent with different predictions, whichrenders them useless in practice. This paper overviews the ongoing researchefforts on computing rigorous model-based explanations of ML models; thesebeing referred to as formal explanations. These efforts encompass a variety oftopics, that include the actual definitions of explanations, thecharacterization of the complexity of computing explanations, the currentlybest logical encodings for reasoning about different ML models, and also how tomake explanations interpretable for human decision makers, among others.