Verification of Autonomous Neural Car Control with KeYmaera X

Abstract

This article presents a formal model and formal safety proofs for the ABZ'25 case study in differential dynamic logic (dL). The case study considers an autonomous car driving on a highway avoiding collisions with neighbouring cars. Using KeYmaera X's dL implementation, we prove absence of collision on an infinite time horizon which ensures that safety is preserved independently of trip length. The safety guarantees hold for time-varying reaction time and brake force. Our dL model considers the single lane scenario with cars ahead or behind. We demonstrate that dL with its tools is a rigorous foundation for runtime monitoring, shielding, and neural network verification. Doing so sheds light on inconsistencies between the provided specification and simulation environment highway-env of the ABZ'25 study. We attempt to fix these inconsistencies and uncover numerous counterexamples which also indicate issues in the provided reinforcement learning environment.

21 pages, 6 figures; Accepted at the 11th International Conference on Rigorous State Based Methods (ABZ'25)

References in corpus (5)

• First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)
• Verifiably Safe Off-Model Reinforcement Learning
• HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification
• CESAR: Control Envelope Synthesis via Angelic Refinements
• Uniform Substitution for Differential Refinement Logic