
We’ve all been there, waiting for the theorem prover to answer. Getting up for a cup of coffee, bugging a colleague… still no answer. This can be standard behaviour when doing formal verification. The requirements are difficult to prove, the system manages to escape into some dark corner not easily approached by the theorem prover. If things are really bad, then the waiting might continue for hours, days, even weeks!
More is not better
The common remedy for this condition is to get more computers, more powerful computers, more memory, parallel computers, more, more… more usually helps to solve the current situation. But soon another larger system comes along and the condition returns. What I am saying is that, usually, perfomance issues when doing formal verification are a symptom of a more serious disease. And trying to cure it with more computer power is like treating cancer with stronger painkillers; it only addresses the symptom, not the cause.
System disharmony
In my experience, the cause of performance issues when doing formal verification is not lack of computer power. It is rather an indication that the requirements and the system verified are not in harmony. With this, I mean that the system might satisfy the requirements, but not in an obvious way. If the requirements are satisfied, then they are done so in some roundabout, tricky way, not by some straightforward checks, making them hard to prove.
The root cause of this disharmony is usually that the system was not developed for verification, causing the fulfillment of the requirements to be addressed late in the development process. The obvious cure is prophylax. Ideally, the requirements should be available at the beginning of the development of the system. Then the developers can design the system so that it satisfies the requirements in an obvious way. This will make the requirements easy to prove and all performance issues go away. Furthermore, formal verification should be introduced as early as possible in the process so the developers have a chance to confirm that they are on the right track.
In case you are wondering, this is how development is done in the Prover Trident process.
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 is partnering with Eiffage Énergie Systèmes on the Villeneuve Demain project, delivering railway signaling software for the PAVS system at SIL4 safety level.
Using Prover’s automation tools, the solution ensures EN 50716 compliance, facilitates future maintenance, and enables reuse across similar systems.
Prover will be at Train & Rail, meet us in our booth located at A06:31.
Learn how Prover’s Relay Signaling Migration enables safe, efficient modernization of legacy railway systems with formal verification and digital twin technology.