Summary: This paper concerns a formal encoding of the Object Management Group’s Complete Meta-Object Facility (CMOF) in order to provide a more trustworthy software development lifecycle for Model Driven Architecture (MDA). We show how a form of constructive logic can be used to provide a uniform semantics of metamodels, model transformation specifications, model transformations and black-box transformation tests. A model’s instantiation of a metamodel within the MOF is treated using the logic’s realizability relationship, a kind of type inhabitation relationship that is expressive enough to characterize constraint conformance between terms and types. These notions enable us to formalize the notion of a correct model instantiation of a metamodel with constraints. We then adapt previous work on snapshot generation to generate input models from source metamodel specification with the purpose of testing model transformations.