Hybrid systems, which combine continuous and discrete dynamics, pose analytical challenges due to their complex nature. Critical systems like automobiles, aircraft, and robotics require high levels of assurance. Theorem proving is a potential method to attain this assurance. In this thesis, I explore how integrating symbolic and numerical computation can lead to the development of automated techniques that are scalable, providing innovative pathways to enhance system reliability.