Margaria and colleagues have emphasized a paradigm for system construction and assurance in which development is organized around building and refining one comprehensive model of the system (referred to as the “One Thing Approach” (OTA)). In this paper, we connect to several key OTA ideas by presenting an integrated collection of development artifacts for a simple safety-critical system (an Infant Incubator example called the Isolette). Our illustration uses AADL for defining system models, the HAMR model-driven development tool, the GUMBO model-based component contract language for specifying constraints, and the Slang/Logika framework for code-level automated property-based testing and verificationl. The artifacts illustrate a rigorous process, moving end-to-end from the concepts of operations and requirements to assurance cases and deployment on the formally verified seL4 microkernel. We describe pedagogical resources and tutorials that have been used to introduce both students and industry teams to formal-methods integrated with model based development.