Abstract
Abstract
Neural controllers are increasingly used in safety-critical control systems. However, certifying their behavior remains difficult when reference tracking, disturbance rejection, and hard state and input constraints must be handled simultaneously. This paper presents a formal verification approach for neural tracking controllers with such operating conditions. Tracking with piecewise-affine dynamics is reformulated as a disturbance-preview problem, so robust controlled invariant sets or candidate operating domains define state-preview pairs on which closed-loop safety can be checked. The learned controller is checked against the induced one-step invariant safety property by encoding violations of input admissibility and guarded successor invariance as neural-network verification queries. The framework is modular with respect to invariant-set computation and to any verifier capable of soundly handling the generated network-linear constraint queries. Case studies on ground- and aerial-vehicle tracking systems certify or falsify controllers, with replay-validated counterexamples, verifier-instantiation agreement, and ablations over preview horizon and uncertainty scaling. The guarantees are conditional on the specified system model, verification domain, and tolerances.