Formal methods bring the rigour of mathematics to the analysis, development and verification of software.  They provide the means to demonstrate that a design fulfills its specifications and are particularly helpful for the developement of high integrity software.

In this talk, I will reflect back on 20 years of experience of practicing formal methods for railway signalling software.  I will firstly present a brief overview of some of the techniques available and where to apply them.  I will then insist on the need for appropriate tooling. Finally, I will present how these techniques have been put into practice in an industrial safety-critical project of substantial size and will give some of the lessons learned during the last decade.