The Constraint Reasoning and Optimization group, with Matti Järvisalo as the project PI, has been awarded a new 360kEUR project grant by the Academy of Finland for a four-year period during 2019-2023 under the ICT 2023 funding instrument. The project develops new fundamental insights into and practical systems implementing scalable symbolic reasoning techniques for formally verifying and explaining AI models.