All software systems execute within an environment or context. Reasoning about the correct behavior of such systems is a ternary relation linking requirements, system and context models. Formal methods are concerned with providing tool (automated) support for the synthesis and analysis of such models. These methods have quite successfully focused on binary relationships: validation of a formal model against an informal one, verification of one formal model against another formal model, generation of code from a design, and generation of tests from requirements. The contexts of systems in these cases are treated as second-class concepts: in general, the modeling is implicit and usually distributed between the requirements and system models. This project is concerned with the explicit modeling of contexts as first-class concepts. Usually, "explicit" means clearly expressed or readily observable whilst "implicit" means implied or expressed indirectly. However, it should be noted that there is some inconsistency, within computer science and software engineering communities, regarding the precise meaning of these adjectives. The requirements engineering community use the terms to distinguish between declarative (descriptive) and operational (prescriptive) requirements where they acknowledge the need for “a formal method for generating explicit, declarative, type-level requirements from operational, instance-level scenarios in which such requirements are implicit”. A consequence of our research is a formal treatment of the adjectives implicit and explicit when engineering software. Nowadays, several research projects and approaches aim at formalizing mathematical theories applicable in the formal development of systems. These theories are helpful for building complex formalizations, expressing and reusing proof of properties. Usually, these theories are defined within contexts, imported and and/or instantiated. They usually represent the implicit semantics of the systems, by types, logics, algebras, etc. based approaches. To our knowledge, no work adequately addresses the formal and explicit description of domains expressing the semantics of the universe in which the developed systems run. For example, the context dependent properties (like weight which depends on gravity) are not expressed in the formal theory in which the formal developments are conducted. This domain information is usually expressed in an explicit semantics. Several relevant properties are checked by the formal methods. These properties are defined on the implicit semantics associated to the formal technique being used: type checking, proofs theory, logic based reasoning, rewriting, refinement, model checking, trace analysis, simulation, etc. When considering these properties in their context with the associated explicit semantics, these properties may be no longer respected. As a very simple example, take two formally developed systems that are composed to exchange currency data represented by a float. This system is no longer consistent if one system refers to Euros and the other to dollars. This is due to the absence of explicit semantics expression in the proof context of the system defining this composition. Therefore, the development activities need to be revisited according to the possibility to handle not only the implicit semantics, but also the explicit one. Without a more formal software engineering development approach, based on separation of implicit and explicit, the composition of software components in common contexts risks compromising correct operation of the resulting system. This is a significant problem if we wish to develop dynamic systems of heterogeneous components that are reliable (self-healing) in unreliable contexts. Thus, this project is about separation of intrinsic and extrinsic concerns by building explicit formal models of contextual semantics using proof based techniques and illustrated on two application domains.