Articles Practice
What people actually ask
Nobody opens with "we would like to adopt formal verification". They open with a question about something that already happened. Here are the eight we hear most, and what each one gets back.
Nobody arrives saying “we would like to adopt formal verification”. They arrive with a question about something that already happened. If one of these is yours, that one question is enough to start from.
These are the eight we hear most.
It never showed up in simulation, but we deadlocked on the floor
You get the exact event sequence that makes the deadlock reachable. What simulation cannot cover is the interleaving — the order in which the parts interrupt each other.
I want to know two axes will not collide before we assemble the machine
This is the question a counterexample answers directly. The search includes the cases where the other axis interleaves between a check and the motion it authorised. For the object itself, see What a counterexample is and the trace on the front page.
What if the value changes in the instant between reading the sensor and acting?
That is a defect class in its own right: the gap between read and act is not atomic. We find the orderings that fit inside that gap.
Can maintenance accidents be shut off by the procedure itself?
We move the maintenance procedure into states and guards, then check whether any path still reaches start-up while a person is inside.
Can we stop the line running normally while a bypass is still active?
The bypass gets a lifecycle of its own in the model, and we look for paths that reach production — or shipment — without it being cleared.
If we enlarge the buffer, does the starvation go away?
We sweep the parameter and re-run the same check. If the design does not recover no matter how large it gets, we show you that as a counterexample.
On a retrofit, can you point at the defects that came from the original design?
We formalise the sequences and interlocks from the design documents. Recovering a model automatically from existing source code is not something we offer today.
Could it reproduce the real bug we spent days debugging?
We move the design conditions that made that bug possible into a model and check whether the same counterexample comes back. We think this is the fastest way to decide whether the method is worth anything to you.
Whichever question is yours, the same thing comes back
What you receive is the event sequence that makes the problem reachable, or confirmation that within the scope we agreed, it cannot be. Either way it arrives in a form you can carry straight into your next design review.
If one of the above is your question, start from that one question. It is fine if you have not yet decided what to ask for.
Read next
How “confirmation that it cannot happen” differs from testing’s “we tried it and it did not” is covered in What is the difference between testing and formal methods?.
Why this way of checking is a requirement in the standards rather than a hobbyist’s concern is in Why safety standards ask for formal methods.