Verification of Low-Dimensional Neural Network Control

We verify safety of a nonlinear continuous-time system controlled by a neural network controller. The system is decomposed into low-dimensional subsystems connected in a feedback loop. Our application is a rocket landing, and open-loop properties of the two-dimensional altitude subsystem are verified using worst-case simulations. Closed-loop safety properties (crash-avoidance) of the full system are obtained from composition of contracts for open-loop safety properties of subsystems in a fashion analogous to the small-gain theorem.