Synthesizing controllers that enforce both safety and actuator constraints is a central challenge in the design of cyber-physical systems. While zonotope-based reachability methods deliver impressive scalability, only parts of these methods have been formalized. Consequently, no practical tool provides a fully verified end-to-end pipeline, leaving an assurance gap for safety-critical systems. Deductive verification with the hybrid system prover KeYmaera X could, in principle, resolve this assurance gap, but the high-dimensional set representations required for reachability analysis overwhelm its reasoning based on quantifier elimination. To close this gap, we develop a verification pipeline that combines scalability with formal rigor by computing control-invariant sets using high-performance reachability algorithms and verifying them using novel logical proof rules. Computationally intensive zonotope containment tasks are offloaded to efficient numerical backends, which return compact witnesses that KeYmaera X can validate rapidly. We show the practical utility of our approach through representative case studies.