When nobody can check, the cost lands on someone
There are two worlds of software. In one, failure kills people quickly, so behaviour is written down and checked by a prover before anything is allowed to run. That world is mature and well served, by people who have been doing it carefully for decades. This page is about the other one, where failure is slower and lands on whoever is least able to argue back.
The areas we are going into, and how we choose them
The software that pays a benefit, issues a licence, records a title, calculates a bill or holds a case file mostly does not get that treatment. It is written, tested for a while, released, and then defended for thirty years. When it turns out to be wrong, the wrongness is absorbed rather than fixed: a workaround here, a manual check there, a team whose job is partly to know which answers not to trust.
What is striking is not that this happens. It is that nobody is surprised when it does. A system that miscalculates for years before anyone notices is treated as bad luck. A replacement abandoned after a great deal of public money is treated as the normal weather of large projects. The standard has drifted so far that meeting it says almost nothing.
So we are going into those areas deliberately rather than waiting to be invited, and we choose them on two conditions together. The software serves the public badly, and the public cannot see in to know that it does. Either one on its own is somebody else's problem: poor work that everyone can see is ordinary competition, and good work behind a closed door is a question about governance rather than about software. It is the combination we are equipped for, because the whole of our method is producing evidence that a third party can re-check.
That is a market, not a fact of life. The difference between the two worlds is not that one has cleverer people or easier problems. It is that in one of them somebody has to produce evidence, and in the other nobody ever asks.
Why we think this is worth saying out loud
Our trade is the quality of software, so this is our subject rather than someone else's. And the clearest lesson available to anyone in it is what happens when a system that decides things about people cannot be examined by the people it decides about.
In the Post Office cases, the accounting software reported money missing. The sub-postmasters accused of taking it could not examine the system that accused them. The organisation that owned the software also brought the prosecutions and supplied the evidence for them. Convictions followed, and some of the people convicted died before they were cleared.
We are not going to tell you what anyone intended by that, which is a question for a court and not for us. What we can speak about is the structure, because it is made of the things we work on every day. There was no independent check. There was no artefact an accused person could take to their own expert and run. And the record could only ever be added to, never corrected downward, which is the condition under which a system stops being able to tell the truth about itself.
Each of those three is avoidable, and none of them is expensive compared with the cost of getting it wrong. That is the whole argument of this page.
Why now, and why not before
Proving that software behaves as intended used to be affordable only where the alternative was a fatality, because it took specialists and a great deal of time. That is why it settled in the places it did and stayed there.
Our whole business is that this is no longer true. If producing the evidence is part of the ordinary cost of the work rather than a special project, then the argument for leaving ordinary systems unproved falls away. A benefits calculation being wrong is not a footnote to someone whose rent depends on it.
What we could actually do
Three things, in the order they usually matter.
Write down what a system really does. For most long-lived government software this is the missing document, and it is often worth more than the code. Not what the specification said in 1994, and not what the manual claims, but the behaviour as it stands, including the parts nobody remembers deciding on.
Carry it across, with evidence. Move it to a language that can still be run and hired for, and hand over the demonstration that the new one behaves as the old one did, so the migration is something you can check rather than something you have to believe.
Change it on the way through, which is the cheapest moment there will ever be. Policy changes; the software usually cannot follow. A conversion is the point at which it can.
Our test cases
We would rather be judged on work already in the open than on a proposal. These are the ones we point at, including the one that does not work.
-
A fifty-year-old accounting system, still in service
A complete COBOL accounting system, written from 1976 and maintained by its author ever since. We converted it and put a machine-checked twin beside the original, then published both, running, free, with his name on it. It is the closest thing we have to the shape of a government engagement: real, old, in use, and nobody's idea of a demo.
See it running → -
An operating system we will never finish
We took one of the hardest bodies of legacy code in existence and ran it through the same process, knowing we could not complete it. We publish the counts as they are, we publish what failed and why, and when the number moved the wrong way we said so. It is on the site because a supplier who only shows you their successes has told you nothing.
Read the honest version → -
Money arithmetic that has to be exact
Tax, national insurance, value added tax, stamp duty and the rest: the small calculations that sit underneath a great deal of public administration, built as components with their proofs attached rather than as code you are asked to trust.
See the components → -
Our own measurements, including when they were wrong
We benchmark the tooling we depend on and publish what we find, which has more than once meant withdrawing something we had announced that morning. Any supplier can show a good number. What tells you more is whether they show you the retraction.
See the results →
What a sensible first step looks like
Not a pilot chosen because it is safe. One real system, small enough to finish, that somebody actually depends on and that everybody is slightly afraid of. If the result is a written account of what it does and a converted version you can check, that is worth having whatever you decide next. If it does not work, you will know that quickly and cheaply, which is more than the usual arrangement offers.
Where we stand
We operate under the King’s law. We are a company incorporated in England and Wales, and the Crown is the source of the law we work under rather than a customer whose conduct is ours to set conditions on. Where we do place conditions on what our work may be used for, those are terms of trade with commercial customers, and they are published where those customers will read them.
If you work in or around government and this describes something on your desk, we would like to hear about it. There is nothing to sign and no obligation to proceed.
Start a conversation →