Empowering the Future of Indian Railways

India is undertaking one of the world’s largest railway modernization initiatives, with KAVACH — the nation’s indigenous Automatic Train Protection (ATP) system — at its core. Through this partnership, Prover and BHEPL will focus on automating data preparation and verification for KAVACH deployments, enabling suppliers to streamline engineering workflows, reduce manual errors and improve overall safety. 

Leveraging Prover iLock, BHEPL will customize and automate the generation of essential datasets such as RFID tag layouts, control tables, gradient plans and other key KAVACH project deliverables. These activities, traditionally performed manually over several weeks, can now be completed in a fraction of the time with higher accuracy and consistency. 

Extending Automation to Metros and Beyond

Our collaboration extends beyond KAVACH. Prover and BHEPL are actively working with metro operators, Indian Railways, and signaling suppliers to explore broader automation opportunities — ranging from interlocking design to CBTC (Communication-Based Train Control) software development. Together, we aim to accelerate the deployment of safe, efficient, and digitally–verified signaling systems across India. 

A Shared Commitment to Safety, Reliability, and Efficiency

“India’s railway modernization drive presents an incredible opportunity to showcase how automation and formal methods can enhance safety, reliability and cost efficiency,” says Gunnar Smith, Chief Product Officer at Prover. “BHEPL’s strong engineering expertise, combined with our globally proven automation tools, is a powerful combination for achieving these goals.” 

Sudhir Reddy, Director at BHEPL, adds: 
“By partnering with Prover, we aim to bring world-class automation and verification capabilities to Indian Railways and metro systems. This collaboration aligns perfectly with India’s vision for a digitally transformed rail ecosystem. The automation tools and products we are co-developing with Prover will be a significant technological advancement for Indian Railways.” 

Introducing Prover iLock for KAVACH: Generative-AI–Driven Design Document Automation for Indian Railways

Prover and BHEPL are launching a Generative AI-powered solution, based on Prover iLock, designed specifically for automating signaling and KAVACH engineering documentation. 

This solution, co-engineered with BHEPL, uses Generative AI, formal methods and rule-based validation to: 

• Generate, verify and standardize complex signaling documents 

• Interpret datasets such as SIPs, TOCs, gradient plans and RFID tag layouts 

• Produce RDSO-compliant outputs automatically 

• Reduce engineering cycle times from weeks to hours 

With adaptive learning models tailored to Indian Railways, Prover iLock understands and evolves with: 

• National railway standards 

• KAVACH-specific data structures 

• Interlocking principles 

• RFID-based control logic 

This enables Prover iLock to function not only as a documentation tool but also as a simulation, verification and validation environment capable of: 

• Virtual testing of KAVACH configurations 

• Simulating interlocking behavior 

• Verifying tag placement logic 

• Ensuring fail-safe operation before field implementation 

These capabilities significantly reduce on-site testing time and accelerate certification. 

Upcoming CBTC Automation Module

Prover and BHEPL are finalizing a CBTC design automation module, marking a major advancement for India’s metro signaling ecosystem. By integrating Prover’s proven formal verification technologies, the CBTC extension will automate the generation and verification of: 

• Zone Controller and ATS control logic, including routing rules, interlocking behavior and operational constraints 

• Movement authority and speed profile logic, consistent with moving block or quasi-moving block CBTC principles 

• Interface and communication message definitions, ensuring correctness of onboard-trackside and ATS-DCS interactions 

This automation significantly reduces manual engineering effort, enhances functional safety and accelerates delivery of highly reliable, digitally verified CBTC systems – supporting India’s transition toward a fully automated, safety-assured metro network. 

About Prover 

Prover is a global leader in signaling design automation and formal verification, helping rail operators and suppliers deliver safe, certifiable signaling systems faster and more efficiently. Our tools are deployed worldwide to automate the design, verification and validation of rail control systems. 
Learn more at www.prover.com. 

About BHEPL

BHEPL (Bharat Heavy Engineering Private Ltd) is an Indian engineering company specializing in railway signaling, electrification and automation. With a strong presence in national infrastructure projects, BHEPL delivers end-to-end solutions to Indian Railways and metro systems, contributing to India’s ongoing modernization efforts. 
Learn more at  www.bhepl.com. 

Inlägget Prover and BHEPL Partner to Bring Signaling Design Automation to India dök först upp på Prover - Engineering a Safer World.

Exploring the interlocking’s full lifecycle

Our goal was to help them explore the entire lifecycle of a railway interlocking system, from layout design and safety requirements to formal verification and testing, all supported by Prover Studio and Prover iLock. The challenge was to build a complete railway line with 7 interlockings, prove the safety of the line, and simulate the behaviour of the whole system.

We began by introducing the fundamentals of railway signalling and explaining what an interlocking is. Equipped with this knowledge, the students first debugged an existing interlocking system following fundamental signalling principles by using formal verification.
Once confident, they defined and verified new safety requirements, created test cases, and implemented a manual release feature, addressing design, safety, and testing aspects within a single, integrated workflow.

Impressive Progress and Collaboration

We extend our warmest thanks to the CentraleSupélec students for their commitment and enthusiasm throughout the week. They impressed us with how quickly they are handling our tools, modelling language, and dealing with the complexities of the railway domain. Special thanks also go to Idir Ait Sadoune and the teaching team for renewing their trust in us again this year.

At Prover, we firmly believe that introducing formal methods and signalling engineering to the next generation of engineers is essential for building safer and more reliable railway systems. We look forward to seeing these talented students again, in the railway industry or the field of formal verification, as they help engineer a safer world.

Inlägget CentraleSupélec students taste Signal Design Automation dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Safety

As rail control software gets more complex, the real challenge is to ensure that implementations meet safety and functional requirements efficiently and convincingly. EN 50716 (the successor to EN 50128/EN 50657) sets the software development and verification expectations for railway applications, clarifying how formal methods and tool qualification contribute to a robust safety case. This session takes a practitioner’s view of applying that framework to real systems and on‑board functions.

We’ll walk through a repeatable assurance workflow: capture requirements as verifiable properties, model behavior in HLL and its sequential extension sHLL, use model checking to explore relevant executions, and establish auditable conformity between specification and implementation. We’ll illustrate the approach using Prover’s toolchain (HLL/sHLL, Prover PSL, Prover Certifier) to make the approach concrete, while maintaining the emphasis on methods, evidence, and governance that can be adopted in any environment.

Agenda:

• EN 50716 in practice. What changed from EN 50128/EN 50657, specifically regarding the role of formal methods within the lifecycle, and what auditors expect in terms of tool classification and evidence.

• A pragmatic formal‑assurance workflow. From property‑driven requirements to HLL/sHLL models, Prover PSL model‑checking, traceability, and preparation of sign‑off evidence.

• Software conformity by proof. How proof‑producing sign‑off with a T2‑qualified engine (e.g., Prover Certifier) demonstrates alignment between specification and implementation for SIL‑classed applications.

• Quality & efficiency gains. Ways to shorten verification cycles, raise coverage beyond testing, and catch defects earlier—without disrupting your current development process.

Yes please, send me the recording!

Speakers

Benjamin Blanc
Solutions Manager at Prover

Inlägget Software formal verification in the context of CENELEC EN 50716: from model to sign-off verification dök först upp på Prover - Engineering a Safer World.

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

Inlägget Formal Safety Verification – How to deliver 100% safe and compliant rail control systems without time delay dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Safety

Recorded on November 5, 2025

At Prover, we address the demand for cost-efficient rail control delivery through Signaling Design Automation (SDA), based on Formal Methods. SDA is also central to the Open Signaling Initiative, promoting open, modular, and interoperable signaling systems. 

With recent advances in AI, we can make SDA more accessible to the rail control community. Adoption challenges often lie in digitizing data, managing requirements, and mastering the technologies. Our goal is to simplify SDA and Formal Methods. In this webinar, we demonstrate how AI enables us to achieve this. 

Agenda:

• The vision for how AI will change the development of safe rail control systems

• Introduction to Signaling Design Automation and Formal Methods

• AI use cases in Signaling Design Automation

• Demonstration: Requirement engineering with AI in Prover Studio

• Interactive Q&A with Prover’s AI and product experts

Yes please, send me the recording!

Speakers

Gunnar Smith
Chief Product Officer at Prover

Fei Niu
AI Innovation Lead at Prover

Inlägget AI, a key enabler for Signaling Design Automation dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Safety

Recorded on September 10, 2025

As digital rail control systems evolve, so do the challenges in validating their safety. Manual testing and reviews are no longer sufficient; they are expensive, slow, and can’t guarantee complete safety. Meanwhile, the cost of missed errors or late-stage discoveries can cause severe project delays or system failures.

Prover’s Formal Safety Verification solution enables a faster, more efficient, and more reliable way to ensure your system meets all safety requirements. It is mathematically proven, highly automated, and compliant with CENELEC standards.

Watch this webinar to learn how formal methods can help you avoid costly project delays, eliminate safety gaps, and streamline your certification process. 

What you will learn:

• Why traditional verification approaches struggle with today’s complex rail systems

• What formal safety verification is and how it works

• How to use model-based development and mathematical proof to ensure 100% requirement coverage

• How Prover’s new solution enables early issue detection, automation, and certified safety evidence

• Real-world results from leading metros, railways, and signaling suppliers.

Yes please, send me the recording!

Speakers

Gunnar Smith
Chief Product Officer at Prover

Daniel Fredholm
Senior Consultant at Prover

Inlägget How to deliver 100% safe and compliant rail control systems without time delay dök först upp på Prover - Engineering a Safer World.

Inlägget Reachability analysis as a way to validate requirements and constraints dök först upp på Prover - Engineering a Safer World.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Formal verification applications to ensure safety of CBTC systems dök först upp på Prover - Engineering a Safer World.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget 3 scenarios where formal verification caught errors missed by traditional rail control system tests dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Safety

An easier path to CENELEC EN50128 SIL4 compliance

In almost every rail control project the effort for achieving compliance with safety standards such as CENLEC EN50128 is a significant part of the project. Traditionally, this involves many manual steps such as reviewing verification documents, test plans, and test reports.

Much of this work can be replaced with automated formal verification, reducing effort, increasing quality, and reducing risk for project delays.

Formal verification is a technique based on mathematical proofs that gives 100 % coverage and can be fully automated. In this recorded webinar, we focus on how formal verification, implemented with a pre-qualified T2 SIL4 tool, Prover Certifier, can be used in a CENELEC EN50128 compliant process.

We also present a case study on how CASCO, a leading rail control supplier, benefits from formal verification in its safety process.

Agenda:

• What is formal verification and why do we need it
• Formal verification in a CENELEC EN50128 SIL4 process
• Introduction to Prover Certifier, a T2 SIL-4 qualified formal verification tool

• A case study: Formal safety verification at CASCO

• Recommendations and considerations for the implementation process

Yes please, send me the recording!

Hosts

Benjamin Blanc
Solutions Manager, Prover

Olav Bandmann
Chief Technology Officer, Prover

Daniel Fredholm
Senior Consultant, Prover

Inlägget Building a safety case for rail control software with formal verification dök först upp på Prover - Engineering a Safer World.