# Verification of Autonomous Neural Car Control with KeYmaera X

arXiv: https://arxiv.org/abs/2504.03272 · HTML: https://mlsanity.com/paper/2504.03272/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 35 references that are in the map.
- First posted on arXiv 4 Apr 2025.

## Builds on (most cited first, 9 of 9)

- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Verifiably Safe Off-Model Reinforcement Learning](https://mlsanity.com/paper/1902.05632/) (2019)
- [Correct-by-Construction Runtime Enforcement in AI -- A Survey](https://mlsanity.com/paper/2208.14426/) (2022)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [CESAR: Control Envelope Synthesis via Angelic Refinements](https://mlsanity.com/paper/2311.02833/) (2023)
- [A Complete Uniform Substitution Calculus for Differential Dynamic Logic](https://mlsanity.com/paper/1601.06183/) (2016)
- [Verified Runtime Validation for Partially Observable Hybrid Systems](https://mlsanity.com/paper/1811.06502/) (2018)
- [Uniform Substitution for Differential Refinement Logic](https://mlsanity.com/paper/2404.16734/) (2024)
- [HyPLC: Hybrid Programmable Logic Controller Program Translation for Verification](https://mlsanity.com/paper/1902.05205/) (2019)

## Built on by (most cited first, 1 of 1)

- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)

## Abstract (arXiv)

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.