Formal Verification of Neural Network-Controlled Systems via Proof Certificates

Neural Network-Controlled Systems (NNCSs), which embed deep neural networks into feedback control loops, are increasingly used in safety-critical domains such as autonomous driving, robotics, and industrial automation. Despite their impressive performance in complex environments, guaranteeing robustness and safety remains a fundamental challenge, largely due to the black-box nature of neural controllers and their sensitivity to uncertainties. This tutorial presents a proof certificate-based framework for the formal verification of NNCSs. A proof certificate is a mathematical object whose existence alone ensures that a system satisfies a desired property. We highlight two representative classes: reward martingales, which provide a rigorous foundation for reasoning about how state perturbations influence cumulative rewards and thus system robustness, and barrier certificates, which partition the state space to ensure that trajectories starting from safe regions cannot reach unsafe ones, thereby formally certifying system safety either qualitatively or quantitatively. Together, these certificates provide a principled and reproducible foundation for establishing trustworthy guarantees in learning-enabled control systems.