Gnatprove vs Multics

the irresistible force meets the immovable object — and what happened to both of them

The coloured notes are from Tony's AI assistant, whose job is to keep people straight where he has missed something — a fact, a caveat, or an observation of its own. We have left them a different colour rather than blending them in.

I am not a formal methods person. I am the simpleton with the proofs who has chanced on a methodology he likes, and last week it found a bug in a banking program that has been running for decades. I want to explain why, because it took me a while to understand what each of these things is actually looking at.

There are four of them and they do not overlap as much as you would think.

I went in trying to fail

I wasn't trying to make it work. I was trying to break it.

I had a proved replacement for an old module, and the proof discharged, and I didn't believe it. Not because I doubt the prover. Because a green tick had started to feel like something I'd set up.

So I went at it looking for the crack. Numbers at the edges, inputs nobody would ever send, and every disagreement my fault until proven otherwise.

And boy did I learn.

note — this is the design of the experiment, not modesty, and it is why the harness will not print a success rate. Four hundred and three agreements out of four hundred and seven is ninety-nine percent if you are hoping to pass, and four things to explain if you are not. Same numbers.

Half of what broke was mine. I'd expected the old code to be the interesting one. It wasn't, or not only. And the proof was perfectly happy with my half.

Tests check the cases you thought of

You write a test, you pick some inputs, you say what the answer should be. If the answer comes back different, you have found something.

The problem is obvious once you say it out loud: a test only ever asks about the cases you were clever enough to imagine. Nobody writes a test for the input that never occurred to them, and that is precisely where the bug is.

note — and tests do not compose. Two components that each pass their own tests can still be wrong together, because nothing tested the join. That is why large tested systems get more frightening with age rather than less: every change might break something no test covers, so nobody dares touch anything.

Flow analysis checks the data goes where you said

This one reads the program and works out where every value actually comes from and goes to. It catches things like: you said this function only depends on these two inputs, but it is reading a third. Or: this variable is used before it is set.

It is very good and it is completely automatic. But notice what it is checking — it checks the program against itself. It has nothing to say about whether the program is doing the right thing.

Proof checks the code against its contract, for every input

This is the one people mean when they say formal verification. You write down what must be true — this function never returns a negative number, this balance is always zero afterwards — and a prover either demonstrates it for every possible input or tells you it cannot.

It is enormously stronger than testing. It is not a sample. When it discharges, there is no input left to worry about.

note, and this is the load-bearing bit — the proof checks the code against the contract you wrote. It cannot check the contract. If you wrote down the wrong thing — a wrong constant, a wrong assumption about what the original did — the prover will discharge it perfectly and you will have proved the wrong theorem, with a green tick next to it.

That is the gap. And I did not really feel it until I saw it happen.

The fourth one: run the old program next to the new one

When we take an old program — COBOL, PL/I, the sort of thing running in a bank — and produce a proved replacement, we now do one more thing. We run the original and the replacement on the same inputs and look at where they disagree.

We call it the Yang Technique.

note, on the name — after Chen-Ning Yang, who, describing how he came to see the CP violation, told his students that if they ever caught the tiniest glimpse of something they should investigate it. That is the whole discipline: the technique is worthless unless you chase the small divergence rather than rounding it off.

Here is the first time it earned its keep. We had a core that computes monthly interest. Proof: discharged. Flow: clean. Both green.

Ran it against the original COBOL over four hundred cases. Four hundred and three agreed. Four did not.

Ninety-nine percent. Every instinct in me said round it off.

The four were the original silently overflowing — a field too small for a result nobody had checked it against, quietly truncating, for decades.

And then it found a worse one

Last week we pointed it at a bill payment program. It pays your balance off in full: move the balance into the payment amount, subtract, done.

The balance field holds ten digits. The payment field holds nine.

note, completing this — ACCT-CURR-BAL is PIC S9(10)V99; TRAN-AMT is PIC S9(09)V99. Moving the wider into the narrower drops the high-order digit, and a COBOL MOVE has no size error clause available — not "nobody added one", it cannot be guarded at all.

So above a billion, it goes wrong. Here is what we measured:

balance	payment recorded	balance afterwards
£999,999,999.99	£999,999,999.99	0
£1,000,000,000.00	£0.00	£1,000,000,000.00
£1,234,567,890.00	£234,567,890.00	£1,000,000,000.00
£9,999,999,999.99	£999,999,999.99	£9,000,000,000.00

Look at the second row. At exactly a billion, you ask to pay the whole balance, the system records a payment of nothing, and your balance is untouched. No error. No warning.

And a much older one

Before the banking program we pointed it at Multics — the operating system, the one from the sixties that everything since borrowed from. We had converted and proved a module called valid_decimal_, which checks whether a string is a valid decimal number. The version we were working from dates to 1978.

Then we ran the original. Not a simulation of it — the actual module, on an emulated Multics, the real operating system booted up and answering.

It crashed.

Error: out_of_bounds at valid_decimal_$|362 — Attempt to reference beyond end of stack.

Feed it a number that is overpunched, signed, and has a precision of zero, and it asks for a piece of string with a negative length. Nothing checks. It runs off the end.

note — the sequence matters here. Our translation had already flagged that input as suspicious and recorded a note about it, but a note is a suspicion. Running the original turned it into a fact, on the real machine, with an error message. Forty-eight years in a system module and, as far as we can tell, nobody had put that input in.

The same run also found a bug in our version. We had written down a bound as 64; the real machine says 87. Four decimal types were invisible to our replacement.

I think that is the honest advertisement for this. One run, two defects, one theirs and one ours, and the technique does not care which is which. It just shows you where the two disagree.

The part that nearly fooled us

Of a hundred and twelve cases, a hundred and eight agreed.

Twenty-eight of those agreements were accidental. Right answer, wrong reason — our version reached the same result down a path that happened to coincide.

note, and this is the sharpest lesson in the whole exercise — a naive comparison reports 108 of 112 and calls it fidelity. It is not fidelity; it is a coin landing the same way twice. The rule we took from it: never count as agreement a case the original never actually reached, and audit the agreements as carefully as the disagreements. It is not enough to chase the small divergence — you have to distrust the large consensus too.

Why none of the other three could find that

Tests would not, unless someone had thought to test a billion-pound balance. Nobody did.

Flow analysis would not. Nothing flows anywhere it should not — the value goes exactly where the program says it goes. It just does not all fit.

And the proof would not, which is the part that took me a while. Our replacement proves that the balance afterwards is zero. That proof is correct. It is correct about our code. It is simply not true of the program we were replacing.

note, and worth being exact about — this is a fidelity gap, not an unsoundness. The prover did its job perfectly and the theorem it discharged is true. What was wrong was the assumption underneath — that the original always zeroed the balance — and no amount of proving would have questioned it, because a proof examines the artefact against its contract and never against the world the contract came from.

You need something that has actually run the old program. That is the only thing that knows.

What you get, when it works

Two things at once, and I did not expect the second one.

You get a replacement you can trust, because the proof discharges. And you get a list of the bugs in the original — the ones nobody knew about, in the code that has been quietly running the business for thirty years.

The proved version becomes a detector for the thing it replaces. Where the old code silently truncates, the new one raises. Every place they disagree is either a mistake in our translation or a defect that has been sitting there all along, and you have to work out which. Both are worth finding.

What it costs, and I should be straight about this

You cannot do this cheaply. You cannot take one suspicious function, prove that, and compare it. To run the comparison at all we had to convert and prove the whole application first, and only then run it alongside the original.

That is the real work. The comparison is the easy part — it is an afternoon once you have both halves. Getting to the point of having both halves is a migration.

note — which is why this is not really a testing tool you would buy on its own. It is what you get in addition, if you were replacing the system anyway. Nobody would convert and prove a decades-old program purely to find its bugs; but if you are converting it regardless, the bug list arrives free, and it arrives before you have switched anything over.

I think that is the honest way to sell it. Not: here is a clever way to find bugs. Rather: here is what replacing your system properly also tells you about the system you are replacing.

What it does not do

It needs the original to still run. If you cannot execute the old program you have nothing to compare against.

It needs a proved replacement in the first place, so it cannot go first.

note — the two are a chain rather than alternatives: the protocol produces the twin, and only then can the technique check it. It can never run ahead of the proof.

And it only sees what you drive it with. It is not exhaustive over the whole program — it is exhaustive over the inputs you gave it, which is a different and smaller claim.

The rule I would give anyone

Do not report a percentage.

The temptation is to say four hundred and three out of four hundred and seven and move on. If we had done that we would have thrown away both findings. Our harness will not print a success rate for exactly this reason: every divergence is listed, and each one has to be explained as our defect, the original's defect, or a fault in the comparison — and you have to say which.

If you get the tiniest glimpse of something, investigate it.

He was talking about particle physics. It turns out to work on COBOL.

So who won

I set this up as the irresistible force against the immovable object, which is the sort of thing you write in a title and then have to live with.

The prover is genuinely irresistible in the only sense that matters here: it does not sample. When it discharges a theorem there is no input left to try, no edge case waiting, nothing to get lucky about. And Multics is genuinely immovable — fifty years old, still runs, still answers, and nobody has needed to touch that module since 1978.

Neither of them won.

The immovable object had a crack in it. Give it a number that is overpunched and signed with a precision of zero and it falls over, and it has been able to do that since before I could read.

And the irresistible force was pointed at the wrong thing. Our replacement proved its theorem perfectly, and the theorem had a 64 in it where the world has an 87.

note — which is the argument of this whole piece in one line. A proof is irresistible within its contract, and completely powerless about whether the contract is the right one. The only thing that settles that is the old program, still running, being asked.

That is why we now run them against each other. Not because either one is the answer, but because the disagreement is the only place the truth shows up.