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.

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.