Assurance vector

RS-Key is not formally verified. This page is generated from the registry and reports what evidence exists, not that a whole-system theorem does. The Definition of done keeps this sentence a requirement until one exists, and scripts/claims_gate.py holds every page naming three or more registered properties to it. What is out of scope and what is accepted: limitations and the threat model.

One word per property mixes questions that move independently. Roadmap §4.1 argues it; the first closed slice measured it. That slice took SEC-FIDO-001 from one Kani harness to four and landed the first mutant in this tree ever to redden a proof — and its status would have read BOUNDED either way, because the word is derived from a harness name.

So the axes are printed apart. Every one is derived from the tree on every gate run by scripts/evidence_gate.py, which also regenerates this page and refuses a stale copy of it.

The axes

Three readings the axes are built to stop. A kani count does not fill in for hardware: a bounded proof is about execution paths and a board result is about a platform, and neither substitutes for the other. A trace count is DIRECT — a recorded session reaches a property only if a configuration checking that property replays it, so the refinement properties carry the session and the invariants they refine do not inherit it. And a configuration NAMING an invariant is not one ASSERTING it: most of them are mutants that exist for it to fall in, which is why model and trace are printed as two numbers each.

hardware reads two sources, and together they give 2 of 59. One is a bundle’s DECLARATION, and the gate’s job there is that a declaration cannot arrive without the board revision it was taken on. The other is docs/platform-assumptions.md’s registry, which is where a board result actually lands — an obligation moving to discharged with a real stepping recorded is what moves this column, whatever class it is filed under.

Neither direction of that number says more than it is. A 0 is “nothing here was measured on hardware” and never a measurement: the axis prints the same 0 over a question nobody asked and over one a board refused to answer. A non-zero is not the property holding on hardware either — it is THESE rows and no others, on the stepping and the boot configuration they name, and it lapses when either moves.

The freshness axis reads committed history only, so an uncommitted edit to an owner is invisible until it lands. That is deliberate: the answer must not change between writing this page and committing it.

What a release may say

• 56 of 59 security properties are ASSERTED by at least one finite TLA+ configuration whose recorded verdict is GREEN, and hold exhaustively over that configuration’s constants.
• 44 of 59 carry a model mutant whose code twin formal/comutants.toml records as patched into the real tree and killed. That verdict is re-driven by the weekly comutate run, not by the gate that writes this page.
• 33 of the 46 rows the v1 word calls MODELLED-ONLY carry such a twin: the word means no Kani harness, and never untested.
• 10 of 59 are checked by a configuration that ACCEPTS a recorded session, and 10 by one that must REFUSE a negative one.
• 11 of 59 carry at least one Kani harness named after them. That is all BOUNDED keys on — a harness NAME, not the #[kani::proof] attribute, not a bound, not a cfg — so it points at the bundle’s method table and is never the proof itself.
• Rows carrying a dated raw evidence bundle: 11 of 59; of those, still ahead of every input they are about: 0.
• No property is claimed on more than 10 built image(s) of the configuration ledger; every other column is a gap or out of scope.
• 2 of 59 carry a result measured on a board, each naming the revision it was taken on.

What a release may not say

• that any property is proven or verified without qualification — no row carries an unbounded deductive proof, and PROVEN-SOURCE is refused by the registry until one exists.
• that a kani count is a proof of anything in particular — the axis counts harnesses carrying the property’s name, and what each one bounds is the bundle’s method table.
• that a model count is the strength of the evidence — its denominator counts every configuration NAMING the invariant, and most of those are mutants that exist for it to fall in. asserted is the half a claim may rest on, and for a clause_of row it can be 0 while the parent invariant carrying that clause is asserted.
• that the model-checked properties hold on the firmware — they hold on the images the scope axis names, and docs/assurance-matrix.md carries the rest of that row.
• that the reconstructed v1 column is an independent check on the registry’s word. It reads the two derivations assurance_gate.py already forces that word from, so its disagreement set is empty on every input that gate accepts: it records that the scalar is a projection, and cannot discover that it is not.
• that 48 of the rows are current — they carry no evidence date at all, so nothing here says when they were last true.

The vector

v1 is the one word assurance/properties.toml publishes, reconstructed here from model and kani rather than copied: no configuration names it and it is ACCEPTED-RISK, a harness names it and it is BOUNDED, anything else is MODELLED-ONLY. All 59 rebuild exactly, which is the migration being lossless — and the reason it is lossless is that the word holds nothing of its own.

Model and Trace read asserted of naming and accepted of replaying. A 0 of 1 is a real state and not a defect: a clause row is asserted through the parent invariant its clause_of names, and RequiredGateAgreesWithRelation is registered precisely so that it is REFUTED.

Claimed on counts the columns disposed covered, equivalent or conditional; Out of scope counts the ones where the ledger says the claim is not made. Their sum is not the number of built images — everything else is a gap, and docs/assurance-matrix.md is the page that counts those.

Coverage by built image

The same 40 P0-family rows, counted the other way round: per column rather than per property. Placed is a disposition the ledger actually wrote, out-of-scope included, because a decision not to claim is a decision. Unplaced is the remainder, and it is what a per-property count cannot show — a property claimed on twenty images looks well covered while an image nobody disposed anything on stays invisible. The columns are matrix_gate.py’s, so this asks nothing about how many built images exist that another gate already answers.

Read the feature rows first: every one of them carries the same handful of placed cells and the rest unplaced, which is the shape roadmap §12 calls feature blindness. A default-build proof is not a proof about the image a feature builds, and the column is where that stops being invisible.

Stale and pending, in one place

Three spellings of “not current”, which used to sit on two different pages and in a registry: a bundle whose commit is behind an input it is about, a P0-family property with no raw bundle at all, and a platform obligation still waiting on a board. Reading any one of them alone reports a clean tree over an unclean one.

Review packet

For the commit that carries this page — which is why no commit is named here: a generated page that embeds the tree’s head is stale the moment it lands, and this section learned that on its first gate run. Every line is derived; none of it claims to be sufficient, because a reviewer who runs all of it has reproduced the software evidence and nothing about a board. The assurance case itself is a later stage’s artifact.

Generated artifacts, and the command that reproduces each.

Model runs this tree publishes counts from.

Raw evidence bundles: SEC-FIDO-001, SEC-FIDO-002, SEC-FIDO-003, SEC-FIDO-004, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-FIDO-007, SEC-FIDO-008 — of 59 registered properties. Stale against this commit: SEC-FIDO-001, SEC-FIDO-002, SEC-FIDO-003, SEC-FIDO-004, SEC-FIDO-005, SEC-FIDO-006, SEC-FIDO-006A, SEC-FIDO-006B, SEC-FIDO-006C, SEC-FIDO-007, SEC-FIDO-008.