Switched systems (i.e. systems switching between a finite set of continuous systems) are an important subclass of hybrid systems, expressive enough for a wide range of systems. This paper introduces the first formalization of switched systems in the proof assistant Coq – a step towards building verified controllers in Coq. We define switched systems and the trajectories they induce while prioritizing verification. Moreover, we offer a specialized formalization for the efficient modeling of periodic controllers. Finally, we illustrate the formalization by modeling and verifying an air filter.