FR

RESEARCH NOTE

What our proofs do not prove

A verification verdict is only as strong as the question it was asked. Here is what ours guarantee, what holds only within bounds, and what is still open.

Ironproof Research · 16 October 2026

Every result cited here is one already published on this site; this note adds its limits, not new figures.

“Proven” is the most dangerous word in our field. It is true of a model, under a property, within a scope — and it travels alone, without any of the three.

Our line is we prove what can be proven, and say so when we cannot. A line under a headline is a promise. This note is the part where we keep it: for each thing Ironproof checks, the exact edge of what the result means.

It is written for the person who has to sign off on a verification result — a risk committee, an auditor, an engineer inheriting a migration — and who needs to know what they are signing.

01

Three verdicts, never two

A pass/fail system has a hidden third state. When a tool cannot decide, it has to put the case somewhere, and “pass” is usually where it lands. That is how a check that never ran becomes a green light.

Every Ironproof result is one of three, always stated within the declared model:

  1. 01Proven. The property holds in every case the model allows. Not the cases we tried: every case.
  2. 02Refuted. The property fails, and the result carries the exact case that breaks it, so you can replay it yourself.
  3. 03Not demonstrated. We could not conclude, or the rule could not be modelled. It is reported as such, never folded into proven.

A result that cannot say “I don’t know” cannot be trusted when it says “yes”.

02

Five places a proof is weaker than its word

None of these is specific to us. They hold for any formal verification result, from anyone. We list them because they are the questions to ask of ours.

1. The model is not the system

A solver reasons about a model: a precise description of the policy, the program or the translation. A proof says nothing about behaviour the model leaves out. That is why every verdict we return is stated within the model you define, and why the model ships with the result.

2. The encoding is not the text

Your policy is written in words. The solver needs logic. Turning one into the other is a step no solver can check, because the solver only ever sees the logic. If the encoding misreads a clause, the proof is a proof of the misreading.

We test this step in our labs by encoding a policy blind: one side writes the rules without seeing the test cases, another writes the cases from the policy text without seeing the rules, and every disagreement is examined. That measures the step on the policies we tried. It is not attached to every result we seal, and it is not a proof.

3. A bound is a bound

Some checks explore a program only up to a stated limit: so many loop iterations, so much input. Within the bound, the answer is exhaustive. Beyond it, the check says nothing. A bounded result that is reported without its bound is a different, larger claim than the one that was checked.

4. The original program has more than one meaning

To show a translation preserves behaviour, you need the behaviour of the original. For COBOL, that depends on the compiler and its options: the same source can store an overflowing number differently under different settings. An equivalence result holds for the semantics our model implements, not for every way the original could have been compiled.

5. A seal proves integrity, not truth

Every result we return is sealed with Ed25519 and the post-quantum ML-DSA-65 signature. Change one figure and the seal breaks. What the seal shows is that the record is intact and which keys signed it. It does not show that what the record says is true. That is what the proof, and the limits above, are for.

03

Application by application

The same engine answers three questions. Here is the edge of each, in the terms of what is already published.

May this action run?

Does this C fix really close the hole?

Does the migrated COBOL do what the old one did?

04

What “without trusting us” covers

Your auditor can check the seal in a browser and re-run the proof in their own solver, from the obligations we ship. Our word is not part of that check.

What that check cannot tell them is whether the obligations were the right ones to prove. That is places 1, 2 and 4 again: the model, the encoding, the meaning of the original. Re-running a proof confirms the mathematics. Choosing what to prove is still a judgement, and it is ours until someone reviews it.

05

Four questions to ask of any verification result

Ours included. If a result cannot answer these, it is a verdict, not evidence.

  1. 01What was the model? What behaviour of the real system does it leave out?
  2. 02What were the bounds? Is the result exhaustive, or exhaustive up to a limit — and which limit?
  3. 03Who wrote the property, and when? Before the solver ran, or after the result was known?
  4. 04What happens when it cannot conclude? Is there a third verdict, or does “unknown” become “pass”?

We prove what can be proven, and say so when we cannot. This page is the “say so”.

RELATED

SOURCES

This note introduces no figure that is not already published. When a published result changes, this note changes with it.