Formal methods history is paved with industry successes towards the improvement of railway systems safety: - L14 Paris driverless metro without accident after 20 years of exploitation, now historic line 1, then line 4 in the near future; - more than 30% worldwide CBTC-based metros embed a formal method; - formal techniques to prove configuration parameters and system level specification correctness; - safety computer programmed with formal method for SIL4 sensor-based C&C systems...