ERTMS aims to facilitate train traffic in Europe by providing a single, interoperable framework. ERTMS represents a set of several thousand pages of specification, covering both high-level and (very) low-level aspects. Since its creation in the 1990 s, it has evolved regularly, with baseline 4 being published in 2023. However, it is proving rather difficult to implement and deploy. It has little feedback compared with the history of the railway world in general, particularly for the highest levels of supervision. The specification, expressed in the form of thematic SUBSETS, give direction but leave a great deal of freedom to manufacturers. The verification work being carried out today relates to the compliance of on-board and trackside equipment with the SUBSETS of the standard, mainly by means of simulation and test benches. This article presents some of the formal verification and validation methods, including formal modelling, automatic proof and model-checking, that are being used today to improve the confidence level of actual deployments.