This article presents an approach for model checking of UML class diagrams in combination with OCL constraints. UML/OCL models are automatically transformed into Formula models and then model checked. This kind of model checking can be seamlessly integrated with standard object-oriented analysis and design workflows, without the need of manual transformation to and from existing model checking systems.