This paper presents a case study in the design and formal verification of a safe controller for the generic two-element lumped-capacitance model of temperature regulation, using formal cyber-physical system (CPS) theorem proving. The coupled dynamics and the absence of a fallback state reflect the complexities of real-world control systems and make it a representative challenge for theorem proving. A controller is developed by a design-by-invariant methodology. Verification using the axiomatic theorem prover KeYmaera X revealed critical assumptions for safety and pushes the frontier of CPS theorem proving. The parametric, general and provably safe controller can be applied to a wide range of temperature regulation tasks and is validated by deploying an instance of the verified controller on a physical system, demonstrating its robustness under model inaccuracies and confirming its real-world usability.