  We formally introduce IsaVODEs (Isabelle verification with Ordinary
Differential Equations), a framework for the verification of cyber-physical
systems. We describe the semantic foundations of the framework's formalisation
in the Isabelle/HOL proof assistant. A user-friendly language specification
based on a robust state model makes our framework flexible and adaptable to
various engineering workflows. New additions to the framework increase both its
expressivity and proof automation. Specifically, formalisations related to
forward diamond correctness specifications, certification of unique solutions
to ordinary differential equations (ODEs) as flows, and invariant reasoning for
systems of ODEs contribute to the framework's scalability and usability.
Various examples and an evaluation validate the effectiveness of our framework.
