Chapter 16 · Part III — The platform
Assurance, evidence and audit
A guarantee is only as good as the thing enforcing it. What the trusted base is, how it is kept small, and why the evidence must not depend on trusting us.
Every claim in the preceding chapters reduces to the same question: what enforces it, and why should anyone believe that thing? This is the chapter that a serious accreditor, auditor or procurement function should read first, because it is where the argument either holds or does not.
Section 01The way assurance claims usually fail
A vendor states a guarantee. The guarantee is enforced by the vendor's own tooling. The tooling is large, proprietary, and unavailable for review. The evidence that the guarantee holds is produced by the same tooling.
That is a closed loop, and no amount of certification around the outside of it changes the fact that the assurance rests on trusting the vendor. The programme's position is that this is not good enough for the sectors in Part II, and that the constraints required to avoid it have to be adopted at specification stage — because they are effectively impossible to retrofit.
Section 02A trusted base that is small and nameable
The programme's binding constraint set fixes the trusted computing base at five enumerable items, sizes them, and treats keeping that list short as a first-order design pressure rather than an aspiration:
- Kernel checker
- The component that establishes the guaranteesDeliberately small and inference-free: inference proposes, the kernel re-checks. This split exists so the part that must be correct stays reviewable.
- Reference interpreter
- An executable specification, plus its conformance suiteThe definition of what the language means, in a form that can be run against an implementation rather than argued about.
- Oracle-separation harness
- Keeps the author away from what grades itNecessary because the author is a threat actor against its own scoring — threat class 6.
- Provenance integrity
- The record of what was produced from whatEnvelope formats rented from established standards rather than invented.
- Reproducible releases
- Bit-identical rebuilds of the toolchain itselfSo that the artifact you were given is demonstrably the artifact the source produces.
Everything else in the toolchain can be wrong without invalidating a guarantee. That is the point of enumerating it: an accreditor can ask what must be correct, get a list with five items on it, and scope a review to that list rather than to a product.
Section 03Two independent checkers, deliberately diverse
One implementation checking its own work is not evidence. The constraint set requires a second checker running differentially, and specifies the diversity rather than leaving it to convenience: a different model family, a different implementation language, and prompting from the specification only rather than from the first implementation.
The reason for that specificity is threat class 7. A backdoor introduced through a poisoned model or a compromised toolchain is only caught by a second opinion that does not share the first one's provenance. Two checkers built the same way by the same process will agree with each other about the same mistake.
This is expensive, and it is exactly the sort of commitment that gets dropped when a roadmap tightens. It is written into the binding constraint set so that dropping it would have to be a recorded decision rather than a quiet one.
Section 04Builds you can reproduce without us
The toolchain executes nothing that a dependency supplied, and the build has no network. Those two properties together make bit-reproducible builds achievable rather than aspirational — and reproducibility is what converts "this is what we shipped" from an assertion into something a third party can verify independently.
For a sovereign or defence context this is the load-bearing property: a build whose provenance can be established nationally, from source, without trusting the infrastructure it happened to run on.
A bit-identical rebuild of backdoored source is bit-identically backdoored. Reproducibility proves sameness, not goodness. The verifier is the control against malicious source; reproducibility is the control against substitution between source and artifact. Both are needed and neither substitutes for the other.
Section 05Provenance at definition granularity
Conventional provenance answers "which commit produced this build". That is the wrong granularity for a review process trying to work out what actually changed, and it degrades under refactoring — moving code produces a diff that looks like change where there is none.
The design records provenance per definition revision, keyed so that it survives refactoring, which supports the queries that reviewers actually want: what has genuinely changed in behaviour, what is derived from a given requirement, what has never been independently verified, and what is stale relative to something it depends on.
That last query is the one that matters after an incident. When a defect is found in a checker or a component, the question is what else did this touch — and a provenance record at the right granularity answers it mechanically instead of by investigation.
Section 06Evidence for review, not transcripts
The measured position from Chapter 3 is that human review cannot absorb machine-paced change, and that automated monitors good enough to catch most problems produce false-positive rates nobody can operate.[10] The design consequence is that trust attaches to artifacts, not to accounts of what happened.
So the reviewable output is a set of machine-generated deltas: what changed in the interface, what changed in the authority any component holds, whether the change is compatible and on what evidence, and what obligations it touches. The authority delta is the one no current review process has, and it comes free with the mechanism in Chapter 12 — it is the difference between reading a diff and being told "this component can now reach the payments database, and previously could not."
Human attention then goes onto a ranked queue of things a machine has already qualified. That is not a reduction in oversight. It is oversight pointed at the decisions where judgement is decisive.
Section 07Observability as a coverage guarantee
An assurance argument needs to extend past the build into what the running system reports about itself, and today that is a library promise: coverage depends on whoever remembered to instrument the code path.
Where the compiler already knows every point at which code reaches the outside world — because every such point is an authority being used — telemetry can be emitted from those points by construction. Instrumentation coverage becomes a property the toolchain guarantees rather than a discipline the team maintains, and a trace that follows a request across the client/server boundary becomes available by default. That last part is not a small thing: the mainstream specification still describes client-side instrumentation as experimental and mostly unspecified,[20] and the compile-time approach to instrumentation reached general availability only recently, which suggests this is the direction of travel rather than an eccentricity.
For an operator, the useful consequence is that "was this code path instrumented?" stops being a question with a discovered answer.
Section 08Exit, which is part of assurance
An assurance argument that assumes you will never leave is incomplete, and the historical failure of language-owned persistence is precisely that users could not get their data out.
The same applies to GDPR data-portability obligations: a subject's right to receive their PII in a portable form is a property of the storage model, not a feature somebody schedules. The constraint set therefore makes exportability a permanent commitment rather than a feature: user data must leave in standard formats at every milestone, including work that is suspended mid-flight. That is a deliberate limit on how much the platform is allowed to own, and it is recorded as a one-way door — a precommitment that cannot be traded away later for convenience.
Section 09What this chapter does not establish
No certification is held. The programme holds no security certification, accreditation, clearance, or approval of any kind, in any jurisdiction, and has applied for none. Nothing in this briefing should be read as implying otherwise.
These are commitments, not yet demonstrations. The trusted base is specified and sized; the second checker is required by the constraint set; reproducible builds are a stated one-way door. None of them has been demonstrated in a shipped toolchain, because there is not yet a shipped toolchain.
The verifier's soundness is the load-bearing assumption. Every guarantee above rests on the kernel checker being correct. That is why it is kept small, why a diverse second checker is mandatory, and why the conformance suite is part of the trusted base rather than an accessory to it. It remains the thing most worth attacking, and we would rather you attacked it now than after an implementation exists.