AI-arkiv - Prover - Engineering a Safer World

Engineering in the age of AI and executable specifications

Mats Boman — Tue, 24 Mar 2026 11:45:20 +0000

Artificial intelligence is transforming engineering. Systems are designed faster, code is generated automatically, and prototypes can be produced in hours instead of months. Across industries, development cycles are compressing while system complexity continues to grow.

But acceleration creates a new challenge: understanding and control.

When systems are generated rapidly, whether by humans or AI, the limiting factor is no longer production capability. It is the ability to ensure that what has been built is correct, aligned with intent, and robust under all relevant conditions.

This is not only a safety issue. It is a systems engineering issue.

The real bottleneck: Clarity of intent

Many engineering failures do not originate in code. They originate in ambiguity:

Requirements that are open to interpretation
Assumptions that are not made explicit
Incomplete descriptions of system behavior

AI amplifies this problem. It can generate implementations quickly, but it cannot resolve intent ambiguities. If the requirement is unclear, the generated result will faithfully encode that uncertainty.

The solution is not slower development. It is stronger specification.

Precise, structured, machine-verifiable specifications create a stable foundation for accelerated engineering. They turn intent into something analyzable, testable, and enforceable.

Executable models as a tool for understanding

One of the most powerful shifts in modern engineering is the transformation of specifications into executable models.

When specifications are expressed in a formal, structured way, they can be transformed into digital representations of system behavior, executable models that simulate how the system should act.

This fundamentally changes the early phases of development.

Instead of validating understanding through review alone, teams can:

Execute scenarios against the intended behavior
Detect inconsistencies before implementation
Prototype system logic before committing to architecture
Align stakeholders around observable behavior

Executable models are not merely simulation tools. They are instruments for shared understanding. They reduce ambiguity at the source.

Conformance and validation in an automated world

As automation increases, so must verification rigor.
Whether logic is handwritten, configured, or AI-generated, it must conform to the original intent. Formalized specifications allow automated conformance checking between:

Requirements
Design
Implementations

This creates a closed loop in which generated artifacts can be systematically validated against defined behavior.

Verification and validation no longer depend solely on late-phase testing. They become continuous activities embedded in the development process.

The role of formal proof

Testing remains essential. But testing is inherently selective. It demonstrates that a system behaves correctly in tested scenarios, not that it behaves correctly in all scenarios.

Formal verification adds a fundamentally different dimension. Proving that defined properties always hold provides exhaustive logical coverage of the specified behavior.

This has two major effects:

It reduces reliance on extensive test campaigns for certain defect classes.
It strengthens the evidence base for safety, reliability, and correctness claims.

Formal proof does not replace engineering judgments. It augments it with mathematical certainty where it matters most.

In complex systems, particularly those developed with AI assistance, this level of rigor becomes a strategic advantage.

Engineering for both speed and confidence

The perceived tension between speed and rigor is a false dichotomy.

Strong specifications enable acceleration. Executable models enable early validation. Automated conformance checking maintains alignment. Formal proofs provide deep assurance. Together, they create a development process that is both faster and more controlled.

Prover’s methods support this paradigm by:

Transforming specifications into executable system models
Enabling early validation and prototyping
Providing automated conformance checking
Supporting formal verification to strengthen evidence and reduce excessive testing

The result is not only improved safety. It is improved understanding, improved predictability, and improved control over increasingly complex systems.

In the age of AI-driven engineering, the competitive edge will not belong to those who generate the most artifacts but to those who can demonstrate, with clarity and rigor, that their systems behave as intended.

Acceleration is inevitable. Assurance must be engineered.

Inlägget Engineering in the age of AI and executable specifications dök först upp på Prover - Engineering a Safer World.

Succeed with migrations of old signaling and traffic management systems

Jesper Carlström — Wed, 29 Jan 2025 07:50:34 +0000

Ondemand WEBINAR

AI

Recorded on February 19, 2025

Much of the traffic management and signaling solutions in the railway industry relies on old technology, and the need for modernization and digitalization is growing. Migrating these systems that are highly dependent on each other is not easy. Many have failed due to over-exceeding costs and time plans.

In this recorded webinar, we presented a solution for overcoming the challenges by modernizing rather than replacing existing solutions. It offers a more sustainable and cost-effective alternative. It allows you to unlock the benefits of a new system more quickly, with minimal disruption to daily operations. By choosing modernization, you can extend the lifespan of your infrastructure while leveraging the advantages of advanced technology sooner.

This approach, based on a structured, proven process in steps and the use of digital twins, is suitable for both rail and metro control systems.

Agenda:

The challenges with migrating old signaling and traffic management systems
Based on real-world migration projects and decades of experience, we will present:

A proven process of migration based on modernization

A modern architecture for signaling and traffic management solutions

A complete traffic management solution

How to migrate a signaling solution based on digital twins and formal methods
Interactive Q&A with experts from Prover and Cactus Rail

Yes please, send me the recording!

Speakers

Jesper Carlström
Chief Product Officer at Prover

Fredrik Bergström
CEO at Cactus Rail

Inlägget Succeed with migrations of old signaling and traffic management systems dök först upp på Prover - Engineering a Safer World.

AI-driven railway signaling is now available via Prover Labs

Fei Niu — Mon, 02 Dec 2024 07:00:55 +0000

There is huge potential to leverage AI in the railway signaling domain. Prover is an expert in developing railway control solutions. We’re continuously pushing the limits of what’s possible in automating signaling design. Our approach, built on formal methods and digital twins, has already set a new standard for automation and efficiency with guaranteed safety. Now, we’re taking these innovations even further by incorporating AI to accelerate and enhance these efforts.

Prover Labs is a space and community where innovation thrives. Through Prover Labs, we invite the railway signaling industry and our customers to explore and shape future AI-driven applications. Here, you can engage with our latest developments and test early versions of our AI-driven applications. It’s more than just a showcase; it’s an interactive environment where your feedback directly influences the future of our solutions and contributes to advancements in automation, efficiency, and safety.

The synergy between formal methods and AI is key to our approach. Formal methods ensure that AI-generated content, such as specifications, models, and code, is rigorously validated against strict rules and properties, guaranteeing accuracy and safety. In turn, AI, particularly large language models (LLMs), makes formal methods more accessible and scalable.

By combining AI, formal methods, and automation tools, we aim to deliver unprecedented efficiency and precision to railway signaling. Tasks that are currently manual—such as input document analysis, requirements engineering (including formalization), and compliance reporting—can be automated, reducing errors and accelerating project timelines.

At Prover Labs, we are exploring these possibilities and more. Starting with simpler applications, such as chatbots for Q&A, we are progressing toward advanced solutions capable of addressing complex challenges, including requirements formalization, compliance analysis, and verification—all powered by the combination of AI and formal methods.

This is just the beginning. Our early prototypes are now available for exploration, and we encourage you to join us on this journey. Try Prover Labs here. Your insights will help refine these tools and drive the next wave of innovation in the railway industry.

Inlägget AI-driven railway signaling is now available via Prover Labs dök först upp på Prover - Engineering a Safer World.

How AI can take automation and safety to a new level in railway signaling

Fei Niu — Fri, 25 Oct 2024 09:43:03 +0000

RECORDED WEBINAR

AI

Recorded on December 18, 2024

At Prover, we’re continuously pushing the limits of what’s possible in automating signaling design for railway control solutions. Our approach, built on formal methods and digital twins, has already set a new standard for automation and efficiency with guaranteed safety.

Now, we’re taking these innovations even further by incorporating AI to accelerate and enhance these efforts. In this webinar, we will explore how AI, together with formal methods and automation tools, can elevate signaling design automation and discuss the future possibilities it brings to the industry.

Agenda:

How AI will bring new levels of automation and safety
How formal methods powered with AI benefit from each other
The most relevant AI use cases in rail control solutions today
How to connect with our ongoing AI innovation via Prover Labs
Interactive Q&A with Prover AI experts

Speaker

Fei Niu
AI Innovation Lead

Yes please, send me the recording!

Inlägget How AI can take automation and safety to a new level in railway signaling dök först upp på Prover - Engineering a Safer World.

Discover next-level rail engineering: Prover Station, COTS Solutions, and AI at InnoTrans 2024

Amanda Öberg — Mon, 09 Sep 2024 08:04:36 +0000

The demand for safer, more efficient, and reliable signaling systems is at an all-time high. At InnoTrans 2024, Prover is thrilled to present our latest innovations that are poised to transform the future of railway signaling. From the powerful Prover Station platform to the seamless integration of COTS technology and AI-driven automation, our solutions are designed to meet today’s challenges and unlock new opportunities.

Discover Prover Station

Prover Station is a web-based platform specifically designed to meet the rigorous verification and validation needs of the rail and metro signaling industry. With decades of expertise behind it, Prover Station streamlines the creation, management, and verification of formal proof projects while integrating digital twins for comprehensive testing and training.

What Prover Station offers:

Formal verification: Prover Station organizes formal verification tasks into Proof Projects, guiding you from initial specifications to final validation. By identifying and correcting logical errors early, it reduces the risk of costly mistakes. The process is fully customizable to meet your safety and performance standards, ensuring compliance with all regulatory requirements.
Digital twin aggregates: Prover Station enables the creation and management of digital twins, which is essential for real-time system monitoring, analysis, and optimization. It aggregates multiple digital twins into a unified model, providing a comprehensive overview for design, testing, and decision-making.
Integration and flexibility: Whether you prefer a cloud-based or on-premises solution, Prover Station adapts to your needs. It integrates seamlessly with external simulators and hardware via MQTT or OPC-UA protocols, offering flexible web interfaces and automation through APIs.

Prover Station is built to enhance the safety, efficiency, and reliability of signaling systems in the railway and metro sectors. From proof projects to ongoing operations, it provides the essential tools you need for success.

Join us on Wednesday, September 25th, from 12:00 to 14:00, for a live demonstration during our mingle event. See Prover Station in action and connect with our team.

The transformation into open and interoperable signaling solutions via COTS

COTS (Commercial Off-The-Shelf) technology is playing a vital role in the modernization of railway signaling systems. Unlike traditional, custom-built systems that are costly to maintain and difficult to upgrade, COTS offers ready-made solutions that are easier and more affordable to integrate. This flexibility allows for faster deployment and better adaptation to new technologies.

The transition to COTS is crucial for updating outdated signaling systems. With COTS, railway operators can quickly adopt new technologies, reduce reliance on single vendors, and achieve higher safety standards more efficiently.

While challenges such as legacy systems, slow standardization, and integration complexities remain, COTS provides dynamic, cost-effective solutions that simplify management and updates. By adopting COTS, you can reduce costs, accelerate development, improve maintenance, and enhance system reliability—key factors in maintaining the highest safety standards in modern rail systems.

We will demonstrate how Prover’s products seamlessly integrate with COTS systems using a Schneider PLC at our booth. Stop by and see it in action!

Advancing railway signaling with AI

We are pushing the boundaries of railway signaling design automation by integrating AI with Formal Methods and Digital Twins, solidifying our commitment to “Engineering a Safer World”. Current industry practices are outdated, and our approach has already delivered significant improvements in efficiency and automation. By incorporating AI, particularly Large Language Models (LLMs), we aim to make complex tasks like requirements engineering, design, verification, and safety more intuitive and efficient.

At InnoTrans, we will showcase how AI is transforming railway signaling. Engage with our AI tools and discover how our innovations are bringing new levels of automation and safety to the industry. Check out Prover Labs, our space and community where you can try out AI-driven innovation and be part of shaping the future.

Join us at InnoTrans 2024

We will be at booth 130 in hall 3.2 from September 24 to 27. Don’t miss the opportunity to see firsthand how Prover is revolutionizing railway signaling. Want to schedule a meeting? Click here to fill out the form, and we will suggest a time slot.

We look forward to welcoming you to our booth at InnoTrans 2024. See you in Berlin!

Inlägget Discover next-level rail engineering: Prover Station, COTS Solutions, and AI at InnoTrans 2024 dök först upp på Prover - Engineering a Safer World.

Prover takes railway Signaling Design Automation to the next level with AI and formal methods

Fei Niu — Mon, 26 Aug 2024 12:00:58 +0000

Prover is dedicated to “Engineering a Safer World,” focusing on providing railway Signaling Design Automation with formal methods and digital twins. We are now taking the next step in accelerating this effort by using AI. As in so many other industries, AI has a huge potential to increase automation and efficiency.

The industry needs to be modernized, standardized, and digitized. The current process for developing and maintaining signaling solutions is slow and inefficient. Prover’s approach to Signaling Design Automation, based on formal methods and digital twins, has taken automation and efficiency to a new level. Our AI investments will continue that development and take this even further by leveraging the synergy between AI and formal methods.

Formal methods is a systematic approach that uses mathematical models to specify, develop, and verify software and hardware systems. They enable precise analysis and verification of system properties such as correctness, safety, and reliability. By applying these methods, developers can ensure their systems meet specified requirements, offering confidence in both system behavior and performance.

The relationship between formal methods and AI is mutually beneficial. Formal methods help ensure AI-generated content is accurate and safe by rigorously checking it against strict rules and properties. Simultaneously, AI, especially large language models (LLMs), can make formal methods more accessible and easier to use. LLMs can simplify the use of complex tools and the creation of necessary artifacts like formalized requirements and models. Additionally, AI can enhance the efficiency of formal verification tools, such as using AI-tuned tactics to guide the model checker during proof searches (read our blog for more information). This synergy enhances AI reliability while expanding the practical application of formal methods, driving innovation and safety in areas like railway signaling.

At Prover, we are working on how AI can bring new levels of automation and safety to railway signaling. By upgrading our existing offerings and developing new products that integrate LLMs, we aim to make complex processes like requirement engineering, design, V&V (verification and validation), and safety more intuitive and efficient.

AI technologies can help generate data and models, automate manual tasks (such as reviews and checks), and improve the usability and efficiency of formal verification tools, all while maintaining the highest safety standards.

Prover will attend InnoTrans 2024 in Berlin from September 24 to 27.

Visit us at booth 130 in hall 3.2.

At InnoTrans, we will demonstrate how AI can bring new levels of automation and safety to railway signaling.

We will demonstrate cases where AI can be used already today.
All the visitors will get access to Prover Labs and be able to use our AI tools themselves.
Book a meeting with us for a deep-dive session on how AI can take automation and efficiency to the next level!

Inlägget Prover takes railway Signaling Design Automation to the next level with AI and formal methods dök först upp på Prover - Engineering a Safer World.

Using AI to unlock the next breakthrough in rail control system performance

Fei Niu — Wed, 15 Nov 2023 08:39:38 +0000

Railway systems have been in use for over two centuries, and they only continue to grow more complex with every year. Today’s infrastructure managers and signaling suppliers are faced with the formidable task of balancing ever-increasing demands for greater speed, frequency, capacity, and smarter features with higher requirements on safety and efficiency.

There is a clear need for technology that can help make sense of the complexity and remove the safety concerns involved in developing and operating rail control systems. Luckily, this is an area where a lot of progress is already being made.

As experts in signaling design automation here at Prover, we always have our eyes open for the technological puzzle piece that can help deliver even safer and more efficient systems. Right now, we are especially excited about the prospect of combining the generative abilities of AI with the precision and rigor offered by formal methods.

Here we will explore how rail control and signaling systems can potentially benefit from AI, with a particular focus on generative AI such as Large Language Models (LLMs).

Why LLM and Formal Methods make a promising match

At Prover, we are currently exploring how AI can be used to assist at different phases of the rail control system development process, especially working in conjunction with our existing tools. In particular, we see great potential in Large Language Models where there have been rapid advancements in recent years.

A large language model (LLM) is a type of artificial intelligence (AI) program with the ability to achieve general-purpose language understanding and generation by being trained on massive amounts of data. We see an opportunity to use LLMs to, for example, help generate data to use in our safety tools, build models for automation, and generally make our tools even easier to use.

If applied correctly, LLMs could very well revolutionize requirement management, development, and V&V processes in the railway signaling industry. Let’s explore further.

Potential applications of LLM in rail control projects

Here are some of the ways LLM-based technologies could be used to benefit the different development phases of rail control and signaling systems, as well as other safety-critical systems.

1. The requirement engineering phase
During the requirement engineering phase, a LLM-based assistant could intelligently answer questions about a collection of requirement documents written in natural languages. It could also extract structured information (from the requirements), and offer suggestions and identify issues aimed at improving the quality of requirement specifications.

2. The design and implementation phase
During the design and implementation phase, including activities such as configuration data creation, model-based software design, and code production, a LLM-based modeling tool could be used to create initial versions of data, software logic models, and formalized requirements (as logic formulas), from given requirements and high-level instructions.

3. The integration, verification, and validation phase
During the integration, verification, and validation phase, a LLM could be used to improve the usability of formal verification tools that have complex user interfaces. For instance, an intelligent formal verification assistant could autonomously perform complex and advanced verification tasks based on the high-level instructions and goals it receives from users.

In addition to the above, we are also interested in exploring how AI could assist the non-safety critical parts of signaling systems, such as traffic management systems. The AI could, for instance, create timetables and scheduling automatically based on user requirements and other constraints.

What’s next?

Based on our initial exploration, it is clear that AI, namely the LLM, has a ton of potential for use in combination with our tools to achieve much higher automation and enhanced safety in rail control signaling systems. All while helping infrastructure managers and signaling system suppliers to more easily balance and meet demands for greater safety, efficiency, innovation, and cost-effectiveness.

At Prover, we have already started prototyping and experimenting, and plan to apply for research funds to study and implement the proposed approaches in the near future.

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

Inlägget Using AI to unlock the next breakthrough in rail control system performance dök först upp på Prover - Engineering a Safer World.

Time to start offering AI-tuned proof tactics to the world!

Amanda Öberg — Thu, 03 Dec 2020 13:18:42 +0000

The time is ripe for “productifying” our work on AI-tuned proof tactics. A few weeks ago we made the first release of our AI-guided fine-tuning toolset, also known as PSL fine-tuner, for broader internal use. Our ambition is that fine-tuning of PSL proof tactics could be offered as part of Prover Cloud Apps in the near future. In fact, we have already contacted some customers to establish collaborations in order to shape this potential new service.

AI-tuned proof tactics are part of the R&D project on AI-powered formal verification that we started back in Spring 2019, and that is being generously partially funded by Vinnova (Sweden’s Innovation Agency). Make sure you read the first and second blog posts of these series.

Up to 100x faster induction proofs

Back in March we reported astonishing speed ups of up to 60x, but in the meantime we have found cases where induction proofs become even 100x faster after fine-tuning! An otherwise 4-day run becomes a 1-hour run using the right proof tactic.

We obtain such specialized proof tactics by learning from smaller versions of properties, and we then expect the tactics to generalize to the actual (larger) properties of interest. We have observed that these “smaller versions” can be obtained in different ways. In particular, for CBTC systems that are divided into multiple zone controllers (ZC), it is possible to train on the smaller ZC and the obtained proof tactics typically work well for the larger ones. We have also confirmed experimentally that proof tactics continue to work after successive iterations of the same system.

This may be of special interest to those of you developing CBTC systems. If you use our AI-tuning technology early in the development phase, you could benefit from significantly faster proving times for the years to come.

On-the-fly fine-tuning of BMC

For bounded model checking (BMC) we have managed to take this a step further, and we don’t require offline training on smaller versions of properties. We are able to fine-tune the BMC of a property on-the-fly. The BMC completes faster (up to 10x faster in our experience so far), and you also get the tuned proof tactic to use for subsequent regression runs.

Let us know if you have a hard verification problem that you would like us to try this technology on!

Inlägget Time to start offering AI-tuned proof tactics to the world! dök först upp på Prover - Engineering a Safer World.

Our model checker PSL up to 60 times faster using AI-tuned proof tactics

Amanda Öberg — Tue, 03 Mar 2020 07:55:07 +0000

From more than two months down to less than two weeks, or six times faster. From almost two weeks down to just five hours, or sixty times faster! These are the kind of speed ups that we are now obtaining in PSL (Prover SL CE) by boosting our turbo-threads technology using AI-optimized proof tactics. Make sure you read our previous blog post back in September, we have been working hard and made very good progress since then. Thanks again to Vinnova, Sweden’s Innovation Agency, for partially funding this R&D project!

The current state of AI-powered PSL

We have a research branch of PSL that has been modified to enable AI-tuned tactics to guide the model-checker during proof search. These proof tactics are obtained by a specialized AI-guided fine-tuning procedure, and they are designed to speed up specific sets of properties. Obtaining one such tactic could, in some cases, keep our servers busy for more than a week. Yet, the obtained tactic can mean saving months of CPU time and faster delivery times for our customers. These proof tactics do not only speed up verification for the HLL model that is used for training, but also boost verification for subsequent versions of the same model. We can fine-tune a proof tactic today and benefit from it for years.

This technology could already be highly valuable to some users of PSL who have very high demands for performance. And you may be able to benefit from it relatively soon! Initially we plan to offer this as a service, that is, you send us an HLL model and we send you back a set of customized proof tactics. For the future we are considering integrating our AI-guided fine-tuner into a special front-end for PSL, so that training happens automatically every time you solve a property.

What is coming next

We are currently experimenting with the computation of features that can characterize and relate a set of safety properties, that is, their “DNA” equivalent. Using this “DNA” will allow us to automatically discover properties that would benefit from known proof tactics, and also compute new proof tactics faster. At the same time, we have also started to explore prediction models, based on deep learning, that could automatically suggest the best proof tactic for a previously unseen property. All this put together would mean that, one day, all PSL users could automatically benefit from these AI-powered speed ups.

Let’s keep working on the future of formal verification!

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

Inlägget Our model checker PSL up to 60 times faster using AI-tuned proof tactics dök först upp på Prover - Engineering a Safer World.

AI-powered proof tactics pay off

Amanda Öberg — Mon, 30 Sep 2019 11:49:35 +0000

Our model checker Prover SL CE (PSL) is getting a lot faster thanks to artificial intelligence techniques (AI)! We are now able to solve some of the hardest benchmarks in our suite in half the time, and in some cases even 10 times faster! In fact, we are not only getting faster but also more efficient, using less computer resources, in some cases only 8% of the previous ones.

How do we do that?

Well, each system is unique and can benefit from a (sometimes radically) different proof tactic. In practice, though, finding the best proof tactic can be as hard as proving the property itself. So model checkers typically ship a few pre-cooked proof tactics that work reasonably well for most problems. Our “secret sauce” is rather to learn the best proof tactic for a specific system using AI, thereby making the search process much more efficient.

These are just the first results of a significant R&D project on AI that we started in the Spring. Of course, there is still much work to do. Our goal is to develop deep-learning models that automatically propose a good proof tactic by recognizing the high-level patterns in our customers’ HLL models.

We have been following the latest achievements in the AI field with great interest, and after having been awarded R&D funds by Vinnova, Sweden’s Innovation Agency, we finally took the decision to move forward with the future of formal verification. AI is playing an increasingly important role in our society and life. Soon AI may be driving our cars and who knows what more… perhaps proving our safety properties in the blink of an eye?

Inlägget AI-powered proof tactics pay off dök först upp på Prover - Engineering a Safer World.