Proving It, Not Just Testing It

There is an old observation in software engineering, usually credited to Edsger Dijkstra, that testing can show the presence of bugs but never their absence. It is the kind of remark that sounds like a pedantic quibble until you sit down and think about what it actually means for a system that steers itself around other ships.

Testing works by trying things. You run the system through the scenarios you thought of, and if it behaves, you gain confidence. But the scenarios you thought of are, by definition, the ones you thought of. An attacker’s entire job is to find the ones you didn’t. For most of a system this is a trade-off you simply accept, because exhaustive testing is impossible — the number of possible sequences of events in a real system is astronomically large.

For a small number of really important properties, though, there is another option.

Describing a system as mathematics

Formal methods take a different route. Instead of running the system and watching, you describe the essential behaviour of the system as a precise mathematical model, state the property you want to hold as a precise mathematical claim, and then hand both to a tool that checks the claim against every possible behaviour of the model — not a sample, not the interesting cases, all of them.
If the property holds, you have something stronger than confidence: you have a machine-checked proof that, for the behaviour you modelled, the thing you were worried about cannot happen. If it doesn’t hold, the tool hands you a counter-example — a specific sequence of events that breaks it. Both outcomes are useful. The second is often more useful, because it shows you a flaw you would probably never have tested for.
This is a demanding technique and it is not applied to everything. You use it where the stakes justify the effort: on the handful of properties whose failure would be genuinely serious.

A worked example: commands must arrive in order

Consider the link between a shore control centre and a vessel. The centre issues a sequence of commands — change heading, adjust speed, hold position. The vessel must act on them in the order they were sent. If two commands are swapped, the vessel follows a trajectory nobody asked for. If one is silently dropped, the vessel is doing something other than what the operator believes.
Now add an attacker who cannot forge a command — the cryptography from Post 2 has taken that option away — but who can interfere with the channel itself: dropping messages, delaying them, replaying an earlier one, or reordering two. Every message the vessel receives is authentic. The sequence is a lie.
The standard defence is to number the messages, so that the vessel can tell if it is about to act on something out of order. That is a sound idea. But “sound idea” is a long way from “works under every possible pattern of interference”, and this is precisely the kind of property where testing gives limited comfort.

What the proof showed

Within CertifAI, this exact scenario was modelled formally and checked by machine. The model included the control centre, the vessel, the communication channel, and an adversary able to drop and reorder messages at will. Two properties were stated: that the vessel receives every command the centre sent, and that it never acts on them out of order.
The results were clean and, importantly, not uniformly flattering — which is what makes them worth something. With the sequence-numbering mechanism in place, out-of-order execution was proven impossible, even against a channel under active attack. Dropped messages remain possible, as they must: no protocol can conjure back a message an attacker has destroyed. What it can do is guarantee the vessel notices, rather than quietly carrying on with a gap in its instructions. Remove the sequence-numbering mechanism from the model, and reordering becomes possible again — confirming that the mechanism is doing the work, and not merely present.

Why a customer should care

Two reasons. The first is the property itself: the command channel between an operator and an Artificial Captain vessel is protected against a class of attack that requires no forgery and leaves no obviously bad message behind — and that protection has been demonstrated by proof, not by assertion.
The second is what the exercise says about the evidence behind our claims. Assurance is usually a matter of documents, test reports and professional judgement, all of which depend on trusting the people who produced them. A machine-checked proof is a different kind of artefact. An assessor does not have to take our word for it; they can examine the model, the property and the result, and check the reasoning themselves.
It is worth being precise about what this does and doesn’t give you. A proof covers the property you stated, about the model you built. It does not certify that the entire vessel is correct, and it does not replace testing, code review or threat modelling. What it does is take one important question and remove doubt from it entirely — which, in a field where certainty is rare, is not a small thing