Model-Driven Software Engineering (MDSE) encompasses traditional areas of language design, tool engineering, and system validation and verification, following a unified conceptual and technical framework (metamodeling, declarative model transformations, model-based analysis). This work presents design cases of methodologies and tools for MDSE, where the state-of-the-art is advanced as a result of applying formal techniques. The contributions encompass (a) the application of metamodeling techniques to industrially relevant languages, capturing their static semantics in a machine-processable manner; (b) the formulation of a methodology for the design-time certification of transformation algorithms; (c) the design of algorithms for efficiently evaluating Object Constraint Language (OCL) invariants for both the secondary-storage and main-memory cases; and (d) several contributions focused on the generation of Integrated Development Environments (IDEs) derived from language definitions for Domain Specific Languages (DSLs). Venues for further progress and an appraisal of the impact of our research are also reported.