📝 SummarXiv

Abstract

Synthesizing controllers that enforce both safety and actuator constraints is a central challenge in the design of cyber-physical systems. State-of-the-art reachability methods based on zonotopes deliver impressive scalability, yet no zonotope reachability tool has been formally verified and the lack of end-to-end correctness undermines the confidence in their use for safety-critical systems. Although deductive verification with the hybrid system prover KeYmaera X could, in principle, resolve this assurance gap, the high-dimensional set representations required for realistic control envelopes overwhelm its reasoning based on quantifier elimination. To address this gap, we formalize how control-invariant sets serve as sound safety certificates. Building on that foundation, we develop a verification pipeline for control envelopes that unites scalability and formal rigor. First, we compute control envelopes with high-performance reachability algorithms. Second, we certify every intermediate result using provably correct logical principles. To accelerate this certification, we offload computationally intensive zonotope containment tasks to efficient numerical backends, which return compact witnesses that KeYmaera X validates rapidly. We show the practical utility of our approach through representative case studies.