Formal methods are a collection of techniques, with mathematical foundations, that aide the specification, development and verification of computer systems and programs. Formal verification has the advantage over traditional verification techniques should as testing in that it can be automated and is exhaustive. These advantages make formal verification particularly suited to safety critical systems where the systems failure can be extremely expensive in terms of both lives lost and money. The talk will introduce formal methods and then describe how they have been applied to automatically check the correctness of real world train control systems.Siemens believe that these formal methods will make the railways safer in the long run and reduce the cost of verification.