AI makes formal verification more important. Here is why.

The railway and metro signaling industry is under pressure to modernize faster, handle more software-driven systems, manage complex multi-supplier environments, and produce stronger safety evidence, all while maintaining the highest levels of safety and service continuity.

AI can help. It can accelerate engineering work that is often repetitive, document-heavy, and time-consuming: extracting requirements from legacy documentation, checking specifications for consistency, generating configuration candidates, drafting test scenarios, summarizing evidence packs, and exploring system behavior at scale.

For an industry facing long project timelines and shortages of experienced signaling engineers, this is a major opportunity.

But it also raises an important question:

If AI can generate code, review specifications, find edge cases, and simulate system behavior, does formal verification still matter? 

The answer is yes. In fact, AI makes formal verification more important, not less. Prover has spent more than twenty years building a formal verification methodology proven in revenue service on systems operated by infrastructure managers such as New York City Transit, Stockholm Metro, and Paris Metro, who have staked safety cases on it. If AI were making that work redundant, we would need to know. 

There are two reasons. First, AI is entering the engineering workflow itself, which means AI-generated outputs must be checked before they influence safety-critical behavior. Second, AI also lowers the cost of systematic attacks, probing, and manipulation, thereby changing the risk profile of increasingly connected and modular signaling systems. 

Formal verification does not compete with AI-assisted engineering. It is what makes AI-assisted engineering usable in a safety-critical context. 

AI in the engineering workflow: opportunity and obligation

AI tools can already support many parts of signaling engineering. It can help structure requirements, identify inconsistencies, generate configuration candidates, propose test cases, and summarize evidence. 

This can reduce manual effort and help teams move faster.  But speed is only valuable if the output can be trusted. 

AI systems can produce results that look fluent, structured, and plausible while still being wrong. In railway signaling, a subtly incorrect route table, a missing constraint, or a misconfigured protection area can lead to unsafe behavior that only manifests in specific operational scenarios. These errors may not be found through standard testing.

AI can help generate. Formal verification determines whether the generated output satisfies the requirements it must meet, including, but not limited to, those that carry safety significance.

This is where Prover’s methodology fits directly. Prover establishes precise specifications as primary engineering artifacts, and verifies every artifact built from them against those specifications, automatically and formally. The same verification boundary applies whether an artifact is produced by a human engineer, an automation tool, or an AI-assisted workflow.

The practical implication is clear: the organizations that benefit most from AI will not simply be those that adopt AI fastest. It will be those who can verify what AI produces. 

AI also lowers the cost of attack

The same AI capabilities that assist engineers can also assist adversaries.

Systematic probing of interfaces, generation of plausible but unsafe configuration inputs, automated search for edge cases, and manipulation of complex multi-component systems all become easier as AI tools mature. 

Four threat areas are especially relevant for railway signaling. 

1. Interface manipulation 

The move toward standardized and documented interfaces such as OPC UA, EULYNX, and RaSTA is positive for interoperability and long-term maintainability. But documented interfaces are also easier to study, test, and probe. 

AI tools can help identify malformed message sequences, timing-dependent vulnerabilities, and edge cases that cause unexpected behavior in receiving systems. 

A formally verified safety core may still be exposed if corrupted or malicious inputs reach it through an interface. The safety boundary must extend beyond the core logic and include interface behavior and assumptions.

2. Configuration and supply-chain attacks 

Signaling applications are highly sensitive to configuration inputs: route tables, track layout data, protection areas, signal charts, and other engineering data. 

These inputs are often produced and reviewed during engineering rather than formally verified during runtime behavior. AI makes it easier to craft changes that appear plausible to human reviewers yet lead to unsafe outcomes in specific scenarios.

As AI-assisted engineering enters supplier workflows, the risk of AI-generated or AI-manipulated configuration data reaching operational systems increases, especially in large projects with multiple suppliers and complex handovers. 

3. Maintenance and update pathways

Modern, software-defined signaling systems require updates, diagnostics, engineering access, and maintenance workflows that older relay-based systems did not.

Each of these pathways can become an entry point. AI-assisted social engineering or supply-chain compromise can target engineering tools, deployment pipelines, or update processes without directly attacking the operational system.

This makes verification and controlled change management increasingly important. 

4. Unverified components in modular systems 

In modular signaling architectures, a verified safety core is often surrounded by components whose correctness is demonstrated mainly through testing and review: gateways, object controllers, traffic management integrations, interface adapters, and engineering tools. 

AI-assisted adversaries will target the weakest link. In a multi-supplier system, the number of possible component interactions is too large to be covered by traditional testing alone. 

This is where formal assurance of interfaces, configuration properties, and interaction assumptions becomes increasingly valuable. 

Why AI-based testing is not enough

A reasonable response is to ask whether AI itself can handle the verification problem. Can AI-based simulation and testing find problems faster and more thoroughly than before?

It can help. But it does not close the gap. 

Testing, including AI-enhanced testing, reveals problems. It does not prove their absence. 

An adversary with AI tools can search the same behavioral space as AI-based testing and is motivated to find exactly the cases that testing missed. Formal verification addresses this differently. It proves that specified properties hold under all reachable conditions in the model. 

An adversary with AI tools can search the same behavioral space as AI-based testing and is motivated to find exactly the cases that testing missed. Formal verification addresses this differently. Formal verification is a mathematical proof that a system satisfies all specified safety requirements under all reachable conditions. It is the only technique that closes this gap. A component with a valid formal safety proof cannot exhibit the class of unsafe behaviors that proof rules out, regardless of how inputs are crafted. Testing, including AI-enhanced testing, can help discover problems. It cannot prove their absence.

That difference matters.

For AI-assisted engineering, formally verified artifacts are more trustworthy than merely tested artifacts. For security and resilience, formal proof can rule out entire classes of unsafe behavior rather than relying on the hope that testing found the relevant cases. 

What this means in practice 

The response does not need to be a dramatic redesign of the entire engineering process. It can be built step by step.

1. Automated verification in delivery and release pipelines 

Today, formal verification is often applied on a per-project basis to support a specific safety case. The natural next step is continuous verification pipelines, where releases of signaling software, configuration, or related components are automatically checked against formally stated safety and interface properties before deployment.

This can reduce manual effort, strengthen evidence for assessors, and give infrastructure managers a more continuous assurance record. 

Prover already applies automated verification pipelines in project delivery. Extending this approach as a recognized compliance and assurance pathway is an important direction for the industry.

2. Extending verification to interfaces and configuration 

Prover’s formal verification has been proven at the level of core safety logic. The same methodology, precise specification, executable models, and automated proof can be extended to interface and configuration properties. 

This matters because AI-assisted risks are likely to appear not only in the safety core, but also in the data, interfaces, and assumptions surrounding it. 

Formally specifying and verifying interface behavior can help prove that no valid or invalid input sequence can drive a component into an unsafe state under the defined assumptions. 

3. Treating safety and cybersecurity as connected assurance problems 

Railway cybersecurity and safety assurance are still often handled through separate frameworks. But as signaling systems become more modular, connected, and software-defined, the boundary between safety and security becomes harder to separate.  

Prover is working toward safety and security assurance handled together.  Formal verification that rules out unsafe behavior does so whether the cause is an engineering error or a manipulated interface.

A cyber event can create a safety-relevant condition. Configuration manipulation can create a safety hazard. A compromised engineering pipeline can affect operational behavior. 

Formal verification cannot replace cybersecurity processes. But when security-relevant properties can be specified, it can help provide machine-checkable assurance at critical boundaries. 

Summary 

AI changes the signaling engineering environment in two important ways.

It accelerates engineering work, which means AI-generated specifications, configuration, models, and evidence must be verified before they can influence safety-critical behavior. 

It also lowers the cost of systematic probing and manipulation, which increases the need for stronger assurance around interfaces, configuration, update pathways, and multi-supplier systems. 

AI-based testing will help find more problems. But it cannot prove that specified unsafe behaviors are absent.

Formal verification remains essential because it provides mathematical proof that defined safety properties hold under all reachable conditions in the model. In an AI-assisted engineering environment, this becomes the trust boundary. 

The conclusion is straightforward: AI makes formal verification more important.