This requirements document presents the case study for the ABZ conference 2025. The case study is about a safety controller for autonomous driving on a highway. The description contains two variations of the case study. First, in the simpler setting, we just consider a single-lane highway where each vehicle can accelerate and brake. The goal is to keep a safe distance to the preceding car. Second, we consider a multi-lane highway where each vehicle can also change lanes. The challenge is to model the system and its environment, derive assumptions, and model a controller that guarantees safety. The challenge is also to present the safety case in such a way that it is convincing to readers not entirely familiar with the formal method employed. The case study is designed so that the formal model can be used as a safety shield within a highway simulation environment. We provide pre-trained (unsafe) AI agents for experimental purposes. This part of the case study is optional.