Implemented Is Not the Same as True
Three industries moved from testing to proving. A practical guide to doing the same on the questions supervisors now ask.
You can evidence that a control was implemented. Can it evidence that the control still does what it was built to do?
Those are two different questions. Only one of them is now being asked, and the answer increasingly shapes how much capital a supervisor requires the institution to hold.
There is an answer available. It was developed over two decades, in three industries with no connection to financial services.
Three industries that moved from testing to proving
Compilers, the software that turns human code into machine code. Every application an institution runs, from a customer-facing app to an overnight batch job, was translated by a compiler before it ran. If the compiler is wrong, every program it produces is quietly wrong too, in ways the original developer never wrote.
A group of researchers built a compiler called CompCert with a mathematical proof attached. For any legal input program, the machine code it produces will behave the way the source code says it should. Other researchers then spent years trying to break it, running a tool that generates random programs and hunts for miscompilation. In the other production compilers they tested, GCC, LLVM and others, the tool found real bugs. In the parts of CompCert covered by the proof, it found none.
Not fewer. None.
Flight-control software. In an aircraft, a runtime error means the software met a situation it did not know how to handle and stopped. On the ground that produces an error message. In the air it does not. Airbus adopted a tool called Astrée, which analyses the whole control program and produces a mathematical guarantee that a defined class of runtime errors cannot occur in any state the code can reach. It has been used across a range of Airbus aircraft, including the A380.
Cloud infrastructure at scale. When a storage system serves millions of customers at once, the number of possible interactions between concurrent operations runs far beyond what a conventional test suite can cover. AWS engineers built a lighter-weight approach for one of their storage systems, checking its behaviour against a simple reference model across an enormous space of input sequences and system states. It is a deliberate trade. Less complete than a full mathematical proof, far cheaper to build and maintain, and strong enough to surface classes of bug that ordinary testing leaves sitting there.
That trade matters, because these three are not one technique. They are a family, running from full mathematical proof at the expensive end to lightweight modelling at the practical end. The choice between them is an engineering judgement about cost and consequence, not a purity contest.
Three organisations with almost nothing in common. Each moved from testing to proving at the point where the cost of being wrong stopped being proportionate to the cost of finding out.
Why this now matters to a regulated institution
The FCA has been reshaping its supervisory approach since the Consumer Duty came into force in 2023, and 2026 has brought its clearest form yet. The regulator has moved from asking whether a firm implemented a rule to asking whether it can evidence the outcome that rule was written to produce. A firm can deliver every required disclosure on schedule and still fall short, if the data on customer understanding tells a different story.
DORA has moved through a parallel shift on a shorter timeline. It came into force in January 2025, and supervisors spent that first year testing readiness largely on paper. That phase closed in early 2026. Supervisors now examine how an institution manages a real incident, oversees an actual third party, and holds up under realistic testing.
Where those examinations raise concerns, they feed into the prudential review. That review looks at each institution and decides how much capital it must hold against its risks. Alongside the baseline requirement, supervisors can set an additional institution-specific layer, known as a Pillar 2 add-on, where they judge the risk profile warrants one. Persistent distance between what an institution has documented and how it is actually running now sits inside the picture that shapes that judgement.
So the line runs directly from how a leader answers a supervisor to how much capital the institution carries.
Both regulators are asking the same underlying question. Can you still explain why this control exists, and can you show that it is holding?
That is the proving standard, applied to leadership.
Two places to apply it
Example one. Interest calculation.
Interest calculations are typically assured through sampling. Choose a set of accounts each month, recompute what the interest should be, check the two figures agree. This works well for the cases the sample includes, and it has been the standard approach for years for sound reasons. Cost, feasibility, and a shared understanding across industry of what reasonable assurance has meant in practice.
The cases a sample tends to miss sit on the edges. An account crossing a rate-tier boundary mid-cycle. A leap-day accrual on a product that posts interest monthly. A negative-rate period on a deposit product designed before negative rates were plausible. A customer who moved between two products on a day when the calendar rule and the posting rule interact awkwardly.
Each of those is a single line in policy. Each is easy to miss in a sample of ten thousand accounts, because perhaps two hundred customers are exposed to it. Too few to surface reliably. Enough to matter when a supervisor asks.
Applying the proving standard here is narrower than it may sound. Proving that every account is correct forever would require the input data to be correct too, and data quality is a separate discipline with its own controls. What can be proved is the calculation engine itself. Given any legal input, it produces the answer the policy specifies. Every rate, every balance, every day-count convention, every combination of corner cases, considered exhaustively rather than sampled.
The value to a leader is concrete. When a supervisor asks whether the calculation holds for the customer on a product transition, in a leap year, at a negative rate, at a tier boundary, there is an answer that does not depend on whether that customer happened to fall into last month’s sample.
Example two. Access when someone leaves.
Every institution has a policy for revoking access when a person leaves. The literal question a supervisor asks is whether that policy exists. The substantive question is whether the person actually loses access to everything, on the day they go.
This is harder than it looks because access is not granted in one place. The identity system controls the front door and is usually clean. Beyond it sit the systems that cache credentials for performance, the service accounts a team created three years ago and never documented, a vendor portal a small group reaches through a shared password held in a team notebook, and a legacy application where access flows from membership of a group refreshed overnight from a source list. Remove the leaver from the identity system and the front door closes cleanly. Every other path depends on a different system doing something specific, in the right order, inside the right window.
Applying the proving standard here means building an explicit model of that whole flow. Every system that grants access, every path a credential can travel, every point where a cache might still hold a valid session. Then demonstrating that no reachable state in the model lets a leaver back in.
One caveat belongs here, and it is the same caveat that applies to CompCert and Astrée. A proof covers the model, not the world. If a system was left out of the model, the proof says nothing about it, and the discipline of building the model is often where the real value sits, because that is the point at which the forgotten vendor portal surfaces.
The value to a leader is again concrete. When a supervisor asks a DORA-style substantive question about joiner-mover-leaver control, there is a modelled answer covering every path, and a documented boundary showing what the model includes.
What a leader does with this
The full techniques behind CompCert, Airbus and AWS are formal methods, and they need specialist skill. A leader does not have to bring that. A leader brings the standard, and the discipline of applying it in miniature to the questions that carry the most consequence.
The discipline has three parts. Ask a control, periodically, why it still exists. Ask what it would fail to prevent if it stopped working tomorrow. Ask what would show up first if that had already happened. A control that can answer all three in language a board member follows is a control the institution still understands.
Applied over time, that discipline builds something specific. A stock of substantive answers, held live across the controls that carry the most weight, ready without preparation because they were never allowed to go quiet.
It is also what supervisors are now inviting us to bring. The FCA’s outcome test and DORA’s substantive review are both, at heart, requests for that stock of live answers. Where they are already in place, the prudential review that sets any Pillar 2 add-on has one less reason to reach for one. The leader gains clearer running command of their own estate. The supervisor gains the evidence they were looking for, in the form they were looking for it in.
A proof is not something you file once. It is something you have to keep being able to give.
If you found this useful, the likelihood is someone you know is asking the same question. Pass it on.