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!
Share this article
Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Prover uses formal methods to make railway signaling provably safe. Our solutions build safe, reliable, and cost-efficient systems that move and protect millions of passengers every day. Through our Open Signaling Initiative, we're reshaping how the industry builds and maintains signaling systems across Europe and beyond. Now we're looking for someone to join us and bring AI, LLMs, and agentic workflows into the heart of how we work and what we build.
Meet Prover at RailTech Europe in Utrecht, March 4–5. Visit Booth 2.509 and join our workshop on migration of signaling systems to PLC-based SIL 4 solutions.
We are seeking an Office Coordinator to our Stockholm office.
The Office Coordinator plays a key role in ensuring that our office operates efficiently and in line with Prover’s standards of professionalism and quality. The role combines office management with broad administrative support to management and staff.
