I present our work on modeling an autonomous driving controller system using Stark. We explore a range of traffic scenarios, from a simple case with two cars on a single lane to complex multi-lane environments with multiple vehicles. Throughout these scenarios, we specify robustness properties and formally verify safety guarantees. Finally, we leverage Stark to assess the safety of an AI agent controlling a vehicle in a congested highway setting. Valentina and I submitted this work in response to the case study proposal of the ABZ 2025 conference.