Basing system designs on informal specifications and applying formal methods after system implementation greatly reduces the benefits that formal methods can provide. Systems of high quality and trustworthiness can be developed in a faster and much more efficient way by capturing system designs with formal executable specifications and subjecting them to automated formal verification from the earliest stages of system design. Even greater benefits can be gained by making such formal designs highly composable and reusable by means of formal patterns. The experience on using the rewriting-logic-based language Maude and its tool environment and formal patterns for all these purposes is presented and illustrated with concrete examples. The benefits of combining model-based design approaches with the one based on formal executable specifications is also discussed an illustrated with examples.