Abstract: A Formal Proof Environment for UML/OCL Achim D. Brucker and Burkhart Wolff We present the theorem proving environment HOL-OCL that is integrated in a MDE framework. HOL-OCL allows to reason over acsuml class models annotated with acsocl specifications. Thus, HOL-OCL strengthens a crucial part of the UML to an object-oriented formal method. holocl provides several derived proof calculi that allow for formal derivations establishing the validity of UML/OCL formulae. These formulae arise naturally when checking the consistency of class models, when formally refining abstract models to more concrete ones or when discharging side-conditions from model-transformations.