This article presents a formal model and formal safety proofs for the ABZ’25 case study in differential dynamic logic ( \(\textsf{dL}\) ). The case study considers an autonomous car driving on a highway with a neural network controller avoiding collisions with neighbouring cars. Using KeYmaera X ’s \(\textsf{dL}\,\) implementation we prove collision-freedom 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 \(\textsf{dL}\,\) model considers the single lane scenario with cars ahead or behind. We demonstrate \(\textsf{dL}\,\) and its tools are 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 indicative of issues in the provided reinforcement learning environment.