Abstract: We describe some ongoing work in developing a formal approach for codesign based on Interval Temporal Logic. Our approach is inspired by existing codesign systems but our focus is on correctness by design and support for proof-based methods. To achieve this, we bring together a number of tools and techniques from the formal methods community. Support for refinement is provided within the HOL system and the Tempura system is used for simulation and testing.