Cordis models are industrial, UML like models. There are some semantical differences compared to standard UML. We verify Cordis models using a translation to mCRL2. In order to verify such models, we have to over several obstacles. In this talk, I will discuss three main challenges that we face so far: (1) the accurate translation of Cordis models into mCRL2, (2) the specification of requirements about Cordis models using the mu-calculus, and (3) scalability of the verification. I show some examples of these challenges and discuss some solutions and results. This work is part of the MACHINAIDE project (ITEA3, No. 18030).