COMMONKADS is a well-known methodology for the development of knowledge-based systems. In this methodology one constructs so-called models of expertise as a basis for the development. A new feature with respect to older versions of the KADS methodology is a formal version of these models, whereby models of expertise are expressed in a special logical language called (ML)2 that is tailored to the needs of KBS methodology. Our paper presents TheME, an environment for constructing and manipulating these formal models of expertise. We consider the role of formal methods in conceptual knowledge modelling and briefly introduce the ingredients of the formal framework. Next, we discuss the rationale behind the TheME environment that supports the formalisation process. The functionality of the environment is described and illustrated in detail and experiences and future developments are discussed. TheME constitutes one of the tools of the COMMONKADS knowledge engineering workbench currently under construction.