I will present the Simple Language of Communicating Objects (\SLCO) framework, which has resulted from our research on applying formal methods for correct and efficient model-driven development of multi-component software. At the core is a domain specific language called SLCO that can be used to specify software behaviour. One of the features of the framework is the formal verification of SLCO models, which is provided via a translation to mCRL2. In this talk, I will discuss the language SLCO, give an overview of the features of the framework, and discuss our roadmap for the future.