Railway signalling systems are surprisingly expensive to produce. Formal methods have emerged as a way to cut costs and increase safety at the same time. Why did this happen, and what have been achieved so far?
Today, there are proof engines that can formally verify the safety requirements for a railway interlocking system in a few minutes using an average laptop computer. Time-consuming and incomplete safety testing can be replaced by mathematical proofs that, for a fraction of the previous cost, can provide 100 percent coverage. This approach requires good quality of the specifications. They must be formalized in a mathematically precise formal language, so that proof engines understand exactly what they are supposed to prove.