Verification of critical software
Proving a rule holds for every input, when testing is not enough
A test suite tells you about the inputs somebody thought to try. For most software that is enough. But some rules (a credit limit, an exposure cap, an eligibility check, a safety interlock) have to hold for every input there could ever be, and the one that breaks the rule is by definition the one nobody thought to try. For those rules a machine-checked proof is stronger evidence than any number of passing tests. It is also more expensive, so the first job is deciding whether you need one.
The decision
The question a proof answers
Tests give you confidence in proportion to how much of the input space they cover. A proof gives you a guarantee over the whole of it, for one stated property. So the question for any given rule is which of those standards it needs, and whether the property can be stated precisely enough for a proof to reach it.
-
Can this rule be trusted for every admissible input?
For a constraint that must never be violated, sampling is not enough. The case that breaks it is precisely the one a test suite did not happen to draw.
-
Where do formal methods help?
When a property is stated precisely and must hold universally, a capacity never exceeded, a bound always respected, a proof closes the space that testing only samples.
-
Where do they not?
Formal methods verify the specification as written. If the spec is wrong, or the property is inherently statistical, a proof is the wrong tool, and the audit says which tool is right.
-
What is the cost of a silent failure here?
The value of proof scales with the consequence of being quietly wrong. Where that consequence is severe and rare, tests are the weakest link.
Why it matters
Why the dangerous failure is the quiet one
Coverage has a ceiling
A test suite exercises the inputs you thought of. For a rule over a large or continuous input space, the untested region is unbounded, and the input that breaks the rule lives there, waiting for a customer to find it.
Numerical soundness is quiet
Floating-point rounding can turn a satisfied constraint into a violated one with no error, no warning and no failing test. The output looks right. It is wrong by a fraction of a cent, and then by more.
Audit needs more than green
When a regulator or a counterparty asks about a decision rule, "our tests pass" is a statement about how hard you tried. A machine-checked certificate is a statement about the rule itself, and they can weigh it as one.
How we approach it
What we do about it
Where a proof earns its cost, we write one: a machine-checked demonstration that the rule respects its specification over every admissible input. The prover we use is our own, and it is built so that the part you have to trust is about 1,200 lines. An engine you do not have to trust searches for the proof, and the small kernel checks every step of it.
For the owner
- A clear statement of which property is proved, over which inputs, and, just as important, which are out of scope.
- A machine-checked certificate a small trusted kernel can re-verify, and never a report you have to take on faith.
- An honest map of where a proof adds value over testing for your rule, and where testing remains the right and cheaper tool.
For the technical reader
- Dependent-type proof: properties are expressed in the type system and checked, never merely asserted in tests.
- Proof-carrying certificates. An untrusted engine proposes a proof term, and a small trusted kernel (about 1,200 lines in Rainbow) checks it. The trusted base stays small on purpose.
- Parametric verification, so a family of instances is covered by one proof instead of case by case.
- Exact-rational and interval arithmetic for numerical soundness, so a constraint proved satisfied cannot be quietly broken by floating-point rounding.
- Scope is published with the result. Rainbow proves all 222 catalogued operations-research algorithms today, and the covered set and the gap are reported together.
Where formal methods do not help
A proof verifies the specification you wrote. If the spec is wrong, the proof is faithfully wrong. It cannot make a claim about an unstated property, an inherently statistical one, or the messy boundary where your code meets the physical world. And a proof of a mathematical algorithm is not yet a proof that a given implementation matches it. Rainbow, for instance, does not currently claim a proved correspondence between its checked terms and their Clojure code, nor infinite-horizon convergence or Bellman fixed-point uniqueness. So where testing, monitoring or a design change is the right answer, we recommend that instead, and the audit fee is the same either way.
What we need to see
The decision logic itself, a precise statement of the property that must hold, and the set of admissible inputs it must hold over. Where the property has never been written down, articulating it precisely is the first deliverable. You cannot prove a specification that does not yet exist.
Where to start
Where to start
A Decision Opportunity Audit scopes one rule you run today: what property must hold, over which inputs, and whether a proof is the right instrument or testing already suffices. Rainbow is the evidence that we can do this: a Clojure-native dependent-type prover with a 1,200-line trusted kernel, proving all 222 catalogued operations-research algorithms, with its boundaries stated beside it.
The loop
- 1. State the property & the admissible inputs
- 2. Decide: proof, testing, or a design change
- 3. Proof-carrying certificate, checked by a small kernel
- 4. Scope and boundaries published with the result
The research behind it
The method and its limits, published
When this fits
- A decision rule whose silent failure carries a severe or regulated consequence.
- A property that can be stated precisely and must hold over every admissible input.
- An algorithm within, or close to, the class a prover like Rainbow can reach today.
When it does not
- The property is inherently statistical, or lives at the messy boundary with the physical world.
- The specification cannot be pinned down, so there is nothing precise to prove.
- Testing or monitoring already gives evidence in proportion to the risk.
FAQ
Questions about verification
When do formal methods pay off?
When a property can be stated precisely, must hold over every admissible input, and the consequence of a silent failure is severe or regulated. Where testing or monitoring already gives evidence in proportion to the risk, testing is the right tool and the cheaper one, and the audit will recommend it.
What exactly is proved, and what is left outside the proof?
We prove a stated property over a defined set of admissible inputs. A proof verifies the specification you wrote. If the spec is wrong, the proof is faithfully wrong. It cannot make a claim about an unstated property, an inherently statistical one, or the boundary where code meets the physical world. And a proof of a mathematical algorithm is not yet a proof that a given implementation matches it.
What is Rainbow?
Rainbow is our open-source, Clojure-native dependent-type prover, past v1.0. An untrusted engine proposes a proof term and a small trusted kernel of roughly 1,200 lines checks it. It proves all 222 catalogued operations-research algorithms; the covered set and the gap are always reported together.
How much do we have to take on trust?
Deliberately little. The trust rests on a small kernel, about 1,200 lines in Rainbow, so what you have to believe is small enough to read in an afternoon. The engine that searches for a proof does not have to be trusted, because the kernel re-checks its result.
What about floating-point rounding errors?
We use exact-rational and interval arithmetic for numerical soundness, so a constraint proved satisfied cannot be quietly broken by floating-point rounding. That failure mode, an output that looks right and is wrong, is the one a proof exists to close.
How do we start?
With a Decision Opportunity Audit that scopes one rule you run today: what property must hold, over which inputs, and whether a proof is the right instrument or testing already suffices. The scope and boundaries are published with the result.
Start with the decision
Bring us one rule
One piece of decision logic that has to hold for every input. A short audit run by a partner will say whether a machine-checked proof is the right instrument for it, or whether testing already earns the trust you need. About half the time it is the second.