We present our return of experience in using Simulink Design Verifier for the verification and validation of a safety-critical function. The case study concerns the train tracking function for an automatic train protection system (ATP). We basically show how this function is formalized in Simulink and present the various proof strategies devised to prove the correctness of the model w.r.t. high-level safety properties. These strategies have for purpose to provide a certain harness over time/memory consumption during proof construction, thus avoiding the state space explosion problem.