Provably Safe Neural Network Controllers via Differential Dynamic Logic

Verifying neural-network controllers for cyber-physical systems is hard, especially over unbounded time horizons. This talk introduces VerSAILLE and Mosaic: derive NN specifications from provably safe control envelopes in differential dynamic logic, discharge them with NN verification, and lift the result to an infinite-time safety proof of the closed-loop system. Demonstrated on the Vertical Airborne Collision Avoidance benchmark.