Formal Safety Verification – How to deliver 100% safe and compliant rail control systems without time delay

The challenge of verifying safety in complex rail systems

Imagine a train weighing thousands of tons, moving at 200 km/h – and hundreds operating simultaneously across a network, guided only by software and signals. When everything works as intended, operations are seamless. However, if something goes wrong, the consequences can be catastrophic, including lives at risk, infrastructure damage, and service disruption.

Over the past decades, railway control systems have grown increasingly complex. Testing and manual reviews remain essential, but they can no longer ensure full coverage. The number of possible system states is simply too vast. In many cases, billions of combinations that no test suite could ever exhaust. Traditional methods show the existence of bugs, not their absence.

A new era of railway safety verification

Formal Safety Verification (FSV) is a breakthrough approach that utilizes mathematical proof to ensure a system meets its safety requirements in every possible state. Instead of relying on selected test cases, engineers use models and automated verification tools to prove that no unsafe scenarios can occur exhaustively.

Prover’s Solution Formal Safety Verification makes this process industrially viable. It integrates proven formal methods with efficient tooling to verify complex rail control systems at scale, across all Safety Integrity Levels (SIL 0-4) and in compliance with CENELEC standards EN 50716, EN 50126, EN 50128, and EN 50129.

How safety is usually handled

In EN 50126, safety is an independent process that starts with the identification of all potential hazards that can affect your system. Then, provided the likelihood of these risks is high enough, some mitigation is added as an extra requirement to the development of the system, with a dedicated SIL level.

For instance, a function of the control system will be tagged as SIL4, and the means to address this criticality is to develop this function following the EN 50716 process, with testing and reviews, and even formal proof to verify that the requirements are correctly implemented. The safety case then collects evidence that the whole process covers these risks, by the book.

From traditional testing to formal proof

Traditional verification relies heavily on reviews and test campaigns that are both labor-intensive and prone to human error. Engineers spend valuable time ensuring coverage and tracking potential corner cases: test scenarios are based on the experience or imagination of the test team.

Formal Safety Verification changes the paradigm. Instead of ensuring that the requirements are implemented as they should be, the new process begins with the hazards themselves, utilizing a model of the system design in a formal language to create a digital twin of the control system. Automated model checkers then verify that the model fully satisfies all hazards, independently of their mitigation. If issues exist, they are presented as high-level scenarios, such as train movements or route conflicts, enabling engineers to pinpoint and resolve potential hazards early.

The result: complete coverage, faster verification cycles, and certified safety evidence generated automatically.

Introducing Prover Diagnostic

At the heart of Prover’s solution lies Prover Diagnostic – a packaged, hazard-based formal verification tool that identifies and eliminates potential safety risks before deployment.

Prover Diagnostic integrates:

• Safety properties, derived from system hazards (e.g., collision or derailment scenarios).
• Environment models define real-world constraints, such as the behavior of wayside components (e.g., switch machines), train movement logic, and operational procedures.
• Formal system models, automatically generated or imported from existing design data.

Together, these components form a rigorous verification process in which hazardous states are either proven impossible or clearly reported for review. Prover Diagnostic ensures 100% coverage, a feat no test-based approach can match.

Proven in leading railway projects

Formal Safety Verification isn’t theoretical – it’s field-proven for many years.

• Stockholm Metro uses Prover’s formal methods for both computerized and relay-based interlockings, supported by digital twins for system-level modeling. The approach enables competition among signaling suppliers, reduces lifecycle costs, and ensures consistent safety assurance across upgrades.
• RATP (Paris Metro) applies hazard-based formal verification using Prover tools to validate CBTC systems from multiple suppliers.
• Alstom, one of the world’s largest rail suppliers, integrates formal methods with Prover PSL and Prover Certifier in its global verification process, enabling exhaustive, automatic safety demonstrations from design through implementation.

These projects demonstrate the maturity and scalability of Formal Safety Verification in real-world railway environments. In many cases, the process reveals and allows for the correction of critical bugs missed by traditional testing.

Formal Safety Verification: a summary of the benefits

• 100% safety requirement coverage – mathematically proven, not sampled.
• Early detection of design issues – reducing rework and project delays.
• Certified safety evidence – supporting compliance with international standards.
• Reduced testing and review effort – accelerating delivery while improving reliability.
• Field-proven solution – trusted by leading metros, railways, and signaling suppliers worldwide.

Ready to prove safety with certainty?

Formal Safety Verification empowers rail engineers to deliver provably safe systems – faster and with complete confidence.

Watch the on-demand webinar to learn how Prover’s solution works, explore real-world case studies, and see how formal methods can transform your railway safety verification process.

Watch the webinar recording