Embedded software for train control is safety-critical because errors can have disastrous consequences. To ensure the safety of controllers, formal verification with computer-checked, repeatable mathematical proofs presents a particularly trustworthy method for controller design. The Federal Railroad Administration contracted a research team from Carnegie Mellon University to develop a provably safe, machine-learning based, predictive train control algorithm to control acceleration and braking along rail tracks. This research was conducted from January 2021 to December 2023. The team used formal verification as a tool to design and verify a symbolic train controller, and a testing-based approach to fill in appropriate values for the symbolic parameters of the formal model. The formalization addresses complex dynamics with transcendental arithmetic, competing forces with subtle interaction, and effects whose exact magnitude is unknown at proof time.