The programme
Question
Systems that make decisions are increasingly asked to account for them. A model grades an answer; an agent commits an action above a limit; a training run produces a number; a protocol advertises a set of tools. In each case someone later asks a question that sounds simple, is this right, did this happen as recorded, can this be checked by someone who does not trust the producer, and the answer turns out to depend on whether the check that was run measures what it appears to.
An assurance claim is a claim about an AI system that purports to establish a property: correctness, safety, reproducibility, provenance, authorisation.
This programme asks whether such claims can be independently checked, and finds that they often cannot, usually for structural rather than malicious reasons. A proof can be valid and prove the wrong theorem. A test suite can pass and measure only its own coverage. Two methods can agree and be wrong the same way. A record can be intact and untied to what produced it. None of these is dishonesty; each is a specific way a check comes apart from the property a reader takes it to establish.
That structure is set out on the failure taxonomy: nine recurring mechanisms, grouped into failures of the instrument (it does not measure what it appears to) and failures of inference (the instrument works, the result is read wrongly). The taxonomy is a claim about mechanism, not a measured base rate, the systems here were studied by one researcher looking for these failures, which is a selection effect.
Themes
The work sorts into five themes. Each names the object a claim is made about and the instrument used to check it.
| Theme | Object of the claim | Instrument |
|---|---|---|
| Formal verification | code and protocols | machine-checked proof |
| Agent control | agent authority, resource use, static-roster multi-agent constraints | machine-checked bounds |
| Evaluation integrity | model and agent behaviour | reproduction and reliability |
| Security engineering | protocol boundaries | differential and boundary audit |
| Assurance architecture | decisions and evidence | sealed records, evidence grading |
The mechanisms cut across all five, which is why the taxonomy is kept separate from the themes. A hidden trusted base is as much a formal-verification failure as an assurance-architecture one; a coverage illusion appears in a test suite and in a negative-control set for a proof alike. What each theme contributes is a different instrument for the same underlying question, and the findings are graded by how far that instrument actually reaches: proved inside a named frame, measured with a stated sample, observed in a single instance, or left open. What each grade permits, and the fields every finding carries with it, are set out in how claims are graded.
Where an analysis was fixed before the data existed, the ordering is carried by the commit history rather than asserted in the write-up. The pre-registration record for the agreement and accuracy study holds the registration, its two amendments and a deviations log that includes the departures weakening a result.
A distinction the findings hold to: a theorem about an artifact built to have a property is a demonstration of what is constructible, not a discovery about an existing system. Both are worth stating; they are not the same kind of claim, and the findings index keeps them apart.
Open problems
The programme's boundaries are as much a part of it as its results. Four problems are open and named here rather than papered over.
- Dynamic rosters in compositional proofs. The compositional safety results hold for a fixed, finite set of agents. A membership that changes during operation, agents joining and leaving under the same invariant, is not covered, and the composition argument would have to be rebuilt to carry it.
- Human labelling for attribution honesty. The judge-disagreement results rest on ground-truth labels that were assistant-adjudicated, not produced by human annotators. Whether the opposite-direction failure survives against human labels, and at what sample size the agreement interval stops being degenerate, needs human labelling to settle.
- GPU-nondeterministic provenance re-derivation. Bit-for-bit re-derivation of a training run was shown on one machine and one numeric environment; cross-hardware re-derivation is untested and reported UNKNOWN. Whether provenance by re-derivation can hold across the nondeterminism of different accelerators is unresolved, and detection power degrades exactly where reproducibility does.
- Specification faithfulness measurement. The sharpest failure in the taxonomy is a proof that is valid and proves the wrong theorem. There is no general way to measure how faithfully a formalised property tracks the intended one; a positive control catches a broken instrument, but measuring the gap itself, across domains, remains open, and its cross-domain form has been examined and set aside as occupied by existing per-domain work.
Warren Smith. Independent, solo. UK. The artifacts are on github.com/repowazdogz-droid.