Model checking for Sysprose — the eight candidates, the rider, and the order they ship in

Summary

You get the behaviour lane's missing half. Today reach answers Stanley & Laski's condition (1) — which states are unreachable — and nothing in the tool answers condition (2): once the system enters degraded, failsafe or maintenance, can it get back out? Today the only expressible spelling of "the design shall be able to enter failsafe" is absence (state failsafe), which exits 1 with verification/refuted on the design that satisfies the intent and exits 0 on the design that violates it — both polarities inverted, both measured on examples/uav-isr.sysml. This plan closes both, and it does so on top of one ten-line engine change: exploreMachine already computes the successor relation and throws it away one line later.

It ships in nine lanes. Lane A is the spine and is not optional: one publishability predicate replacing the two duplicated conjunctions that exist today, one exactness gate replacing the per-mechanism conditions on the whole increasing side, two registers that make an unguarded absence claim or an ungated witness a red test rather than a review comment, the retained successor relation, one Tarjan pass, and two guards — a vocabulary ratchet and a widened claims guard — that land before the features they protect. Lane B is a second spine — lanes C, G and I depend on it and lane H depends on lane E; given A and B, lanes C, D, E, F and G may be re-ordered or dropped whole. The draft called B…I mutually independent, which its own dependency lines contradict (§4).

Nine of the eleven features can emit an absence claim — not covered, no trap, not recoverable, guaranteed, holds on every maximal run, no fair cycle, no simulation relation, no cut set, current within this proof's scope. That is the single way this lane starts lying, and it is one line away: recording the retained edge at the admission point in exploreMachine — where a newly discovered configuration is enqueued — instead of at the revisit prune, where the edge into an already-seen configuration is the one being discarded, yields the BFS spanning tree, acyclic by construction on every machine in this repository, and Tarjan over it names {failsafe} a bottom SCC on the flagship example — a shipped model reported as having an inescapable failsafe that does not exist. So the ordering lens is risk retired, not value delivered, and every absence claim in §3 carries the exact conjunction that licenses it, registered in one table.

And the conjunction is not the same for all of them, which is the correction the adversarial review forced. An absence claim's soundness under this engine depends on its polarity in the edge relation: the two claims that ship today are monotone-decreasing, which is exactly why the walk's deliberate over-approximation of time is sound for them, and most of the claims this plan adds are monotone-increasing, for which the same mechanism is a licence to lie. §2.3 states the rule and makes it a reflection test rather than a paragraph. Three contract sentences move with it (§2.1) and three of this plan's own draft claims were withdrawn or re-worded rather than shipped.

A second review then broke the first fix in four places, and those corrections are in here too. The publishability predicate is two conjunctions, not one — a single boolean would have turned the two shipped absence claims into refusals on any timed machine and emptied a true finding out of reach. There is a second register, for positive witnesses: a refutation, a named avoiding cycle and a published witness trace are increasing claims over the retained relation, and the draft gated none of them. And the hazard's own reachability moved: accept after(n) is a parse error (§0 row 22, measured), so a timed transition is API-only, every dwell fixture is factory-built, and the dwell census is re-priced as an SDK-population number rather than a claim about a user's corpus.

Four reviews found four ways the walk's edge relation differs from the machine's, a fifth arrived while this section was being written, and the answer is structural rather than another patch — and the tree has since shipped the structure. Round 1 found time (after(n) labels enter the alphabet and no clock advances). Round 3 found the cooperative environment — every trigger in the alphabet is offered wherever the walk takes an event, so locked → nominal exists in the walk only because the walk hands the machine unlatch (measured, §2.3) — and the seeded store, which under-approximates in the other direction, so a guard over an attribute with no declared literal manufactured a trap and a not recoverable at exit 1 on a correct design. Round 5 found the fourth and it was of a different kind: an edge metaclass simply absent from the step relation, so a succession between two states parsed clean, landed in the model and was never walked. That one is fixed at a66ba1f — and the way it was fixed is what this plan now stands on. edgeCensus (explore.ts) counts every edge-bearing element under a machine without asking the walk and puts each in a bucket that says what became of it; an edge in the unaccounted bucket fails a test and refuses the machine. So the question is inverted: this plan stops enumerating the ways the relation can be wrong and requires instead that it be right — one predicate, walkIsExact, on the whole increasing side (§2.3), whose element-set half is already carried by the shipped census and whose remaining three clauses are about what the walk offers at a configuration rather than which edges exist. Every increasing absence claim reads it; every existential witness reads its relation half, because a bound can hide such a witness and can never invent one; the two witnesses that are really maximality claims — a cycle with no exit, a run with no successor — read the whole of it, and the register's kind column is what makes that a test rather than a paragraph. The measured survey of every state machine in the tree (§5(d), re-taken at dc6662c) says the gate is free on today's corpus and only partly falsifiable by it: nine of eleven machines are exact, the two that are not are already suppressed today, no model contains a dwell or a named trigger — so clauses (b) and (c) are exercised only by fixtures this plan invents — while clause (d) and the element-set half now have real corpus witnesses, in the fixture models c929278 and a66ba1f left behind.

Five of the eleven are held behind a census the tool itself installs, because their kill-measurement already reads no on this tree: 0 of 3 shipped machines are acyclic; 0 of every .sysml file in the tree relate two state machines by refine or :>; 0 of them carry a requirement that inherits a clause; exactly 1 part declares boundary ports over internal structure and it is degenerate; and the connector graph contains no dependency template at all, so conditions 1 and 2 as specified would fire on 100 % of ports on every model in the tree. Each of those five is specified here in full, so that the day its census reads non-zero the build is a transcription and not a fresh design.

Nothing here creates a new exit-code contract. Four sentences inside three existing contracts move, and the behaviour lane's 0 row moves three times — BEHAVIOUR_EXIT_CODES' 0 and 2 rows (commits 6 and 16) and its 0 row again in commit 18, FAULT_TREE_EXIT_CODES' 2 row, REFINE_EXIT_CODES' 2 row — and §2.1 writes each one out, because a verdict routed to an exit code whose published sentence means something else is the laundering §2.2 exists to refuse. The claim vocabulary opens exactly once, from four words to six, and is then closed for the rest of the plan.

Measured against main @ dc6662c, working tree clean. Five commits landed under this plan while it was being written (§0.1) and every figure and every citation below is re-taken against that tree. Baseline: the counts this plan would otherwise quote — subcommands, validation rules, catalogue codes, property patterns, exit-code contracts, examples, test files, .sysml files in the tree — are named by their guard rather than by their number wherever a sentence can carry the guard instead. test/unit/docs-counts.test.ts is that guard for every prose figure (COMMANDS.length, RULES.length, DIAGNOSTIC_CODES.length, the example count, the two file counts); test/unit/validation.rules.test.ts pins RULES.length; docs/CONFORMANCE.md's scorecard carries the suite figures and is itself checked. Where a number is unavoidable in prose it is stated once, at the point of use, with the guard that would redden if it moved. The two absolute figures this plan does still assert about the tree — that COMMANDS.length does not move and RULES.length does not move — are stated as does not move, which is what an implementer needs and what a test can hold.

0.0 The citation contract: line numbers are not normative anywhere in this document

Four revisions of this plan were spent re-pointing line numbers at a tree that kept moving underneath them, and roughly sixty percent of the last review's findings were exactly that. A 1,600-line plan pinned line-by-line to a repository under active change cannot converge. So the rule for this document, and it holds in every section:

• An instruction names a SYMBOL and an ANCHOR. "In reachOne, after the unsupported refusal and before the product search" — never "insert at :1177". The symbol is what an implementer greps for; the anchor is what tells them which of its occurrences.
• A line number, where one is kept, is a dated HINT. The form is `explore.ts` (`reachOne`, ~:1199 as of `dc6662c`) — and every bare `file`:NNN still standing in this document is to be read that way, as a hint measured at dc6662c and not as an instruction. A hint that misses is stale, not wrong; the symbol beside it is the instruction and it is what the implementer follows.
• An instruction that cannot be written without a line number is a sign the change is not yet understood. Describe the edit by what it must achieve instead, and let the per-commit brief find the position.
• The per-commit briefs carry the precision. They are written fresh against the tree at implementation time, and that is the only place an exact anchor belongs. §4's Files: lists name files, symbols and the sentence that moves; they do not name positions.
• A sentence being deleted or re-recorded is quoted, not located. The standing rule in §4 already says this for deletions — grep for the SENTENCE across test/ and docs/, never for the function that composed it — and it is now the rule for every re-record as well. A hand-pasted transcript is found by its text; it has never been findable by its line.

Two consequences worth stating before they surprise anybody. Nothing in this plan is blocked on a line number being right: every Files: entry resolves through a symbol name, a it(...) title, or a quoted string. And a reviewer who finds a stale number has found a stale hint, which is a one-word fix in a document, not a defect in a plan.

0. Corrections to the two source documents, measured before anything is built

Twenty-three statements in docs/05-model-checking-literature.md, the scope note, or docs/04 have moved or are wrong. Thirteen of them would have produced a wrong line of code or a false finding. Rows 15–21 were added after the first adversarial review of this plan and rows 22–23 after the second; rows 15, 17, 19 and 22 are the four that gate the build. Everything below uses the measured form; do not re-quote the originals into a commit message or a verdict line.

And what docs/05 §5 flags as unverified on the page. Item 2 (Baier & Katoen p.453, comparing over "the set of common atomic propositions") and item 4 (p.524, the O(M·|S|) simulation order) were not read on the page by their own author; item 5's Dependency Template and the SPARK DERIVES contrast carry the same label; item 3 (the BDD ordering and the explicit-state/symbolic scale figures) does too, and §6.1 is where this plan reuses it. Candidate 6 rests on 2 and 4; candidate 7 rests on 5. Neither is cited as a source for a verdict anywhere in this document. Candidate 6's labelling rule is declared as this tool's own choice, its cost is stated as "a genuinely new algorithm" rather than as a complexity bound, and candidate 7's conclusion is drawn from measurement on this tree and not from the book's transposition. Where item 5 nevertheless shows up in prose — §3.7b's derived-vs-declared axis — it is now labelled unverified at the point of use and the sentence commit 14 ships into docs/CONFORMANCE.md states only the measured half (correction 21's companion, §3.7b). docs/05 §5's two labelled inferences ("liveness is cheap at this scale", "explicit-state beats symbolic below N states") travel with their label wherever this plan reuses them, which is §6.1 and nowhere else.

0.1 Five commits landed under this plan while it was being written, and this is what they moved

None of them is a lane here; all five are ground the lanes stand on. Several things earlier revisions of this plan proposed to BUILD already exist, and the rule for reading §3 and §4 is therefore: where this document describes a mechanism, the mechanism is described because a claim reasons about it, not because a commit adds it. A commit adds only what its own Files: list says it adds. Each item below was re-executed against dc6662c for this revision rather than taken from the commit message.

• c929278 — an undetermined guard is no longer indistinguishable from a false one. reach used to publish exhaustive plus three absence findings on a model whose only transition is guarded by an attribute with no declared value. What SHIPPED, and what this plan therefore does not build: ExploreResult.undeterminedGuards, a readonly UndeterminedGuardRow[] populated by stepCandidates, which "returns the enabled transitions and the guards that decided" (config.ts); the three-valued guardVerdictStore beside it; a fifth publishability conjunct — const guardsDecided = walk.undeterminedGuards.length === 0, conjoined into const publishable in reachOne; the verification/guard-undetermined warning; and the undetermined under {…} — N guard(s) the walk could not evaluate; the unreachable, dead and no-way-out lists are WITHHELD qualification. undetermined is deliberately WIDER than "no declared value", and the docstring on guardVerdictStore says so in as many words: it also covers a non-boolean operand under not/and/or, a mixed-type comparison and non-finite arithmetic — so not mode over a fully valued mode is undetermined while mode is decided. Any clause in this plan written as "no declared value" would be strictly narrower than the shipped predicate and would read green on a walk that is missing an edge; §2.3 spells clause (d) against the shipped field and nothing else. Three consequences run through this plan. (i) reach's golden output already moved, so §3.P's "the golden must not move" differential is baselined on dc6662c; correction 23 below and §2.3's third mechanism are labelled with the tree they were taken on. (ii) A bound does NOT withhold a deadlock row. A bound stops the walk enqueueing successors and takes nothing from a configuration already dequeued and offered every input, so recordDeadlock's subject is unaffected by it — which is a different fact from §2.4(b)'s Tarjan hazard, where a bound-dropped successor does leave a configuration looking like a sink in the retained relation. (iii) A nondeterminism row IS withheld when an undetermined guard sits strictly inside the level where the choice is reported, because that guard may have been the transition the priority rule would have picked — so §2.4(d)'s trigger is "nondeterministic > 0 or a nondeterminism row was withheld under that rule", or the simulator disclosure disappears on exactly the walks that least resemble the simulator.
• c37eb00 — connectivity's self-contradiction is FIXED, and so is the same defect one level up. It used to print "every declared port is wired" above three dangling ports its own connection list showed wired, because the wired and occurrence halves normalised the part reference differently. Re-executed at dc6662c: connectivity examples/vehicle.sysml prints 4 port(s), 2 connection(s), 4 connected, 0 unconnected, the two connections, every declared port is wired, and the lifted-endpoint accounting line — no unconnected port usages block at all, exit 0. ConnectivityReport.unreconciledPorts exists and is the report's own check that the two readings agree; it is [] on the examples and non-empty only where they genuinely disagree. This plan ships no commit for it, and §3.7a cites the post-fix behaviour as the baseline its tests re-run rather than as a defect its census surfaces. Lane F's dependency lines say needs the fixed inventory, not needs an unassigned fix.
• a66ba1f — every edge the machine has is walked, or the walk says which it did not. Succession is now in STEP_EDGE_KINDS beside TransitionUsage; SuccessionFlow is refused by payload rather than by metaclass; danglingTransitions reads CONTROL_EDGE_KINDS so first busy then nowhere; and transition busy then nowhere; get the same answer. And edgeCensus exists — every edge-bearing element under a machine, counted off the model and not off the walk, each in exactly one bucket: walked, opening, refused, off-stack, not-a-step, unaccounted. It is published as ExploreResult.census and MachineReach.census (--json only). The unaccounted bucket is the failure bucket: a row in it fails a test and refuses the machine, through unsupportedConstructs, so an edge kind nobody enumerated cannot silently shrink an absence list. Re-executed at dc6662c on the probe that found the defect — three states, three transitions and one succession degradedA then nominal — reach now prints 4 of 4 transition(s) fired, 0 dead and raises the nondeterminism row the fourth edge creates. This is the generalisation the exactness gate was reaching for, and §2.3 is rewritten around it.
• 189fc6d and dc6662c — the gate is 549 s, not 790 s, and the CLI campaign is restructured. test/campaign/cli.sysprose.test.ts was 787 s of a 790 s run because every case spawned npx tsx scripts/sysprose.ts. scripts/sysprose.ts now exports main(argv) and runs runMain only when it was run as a script, and the campaign file keeps two invokers: spawnCli(…) for everything only a process can be wrong about — exit status, - on stdin, a payload past the pipe buffer, an unknown flag, an unreadable file, --help, one end-to-end run per exit contract — and every solver-bearing subcommand, because z3's WASM module carries process-global state and does not survive being driven many times in one worker — and run(…), in-process, for what a case asserts about the TEXT. Measured at the gate: npx vitest run went 760.83 s → 548.74 s, 0 failed and 0 solver aborts, over the file and test counts docs/CONFORMANCE.md's scorecard records and test/unit/docs-counts.test.ts holds — read them there rather than from this plan, because they move with every commit that adds a test file and this document is not their guard. Every commit in §4 that budgets time, or that adds a case to that file, assumes this file: a case asserting text uses run, a case asserting the program or invoking a solver uses spawnCli, and a position in the file is named by its it(...) title. The failure mode of getting it wrong is a green run — vitest's own warning for an unhandled WASM abort says it "might cause false positive tests" — which is why the choice of invoker is part of a Tests: line and not a style preference.

1. What the tool has and lacks today, per candidate

Every "has" below is code that runs now; every "lacks" was reproduced this session.

2. The exit contract

2.1 Seven contract kinds exist, and this plan creates none

Measured: ExitContract (scripts/lib/sysprose-spec.ts:327) is 'report' | 'verify' | 'refine' | 'bounds' | 'write' | 'behaviour' | 'fault-tree', dispatched by exitCodesFor at :353-359. Six of the seven judge; report does not, and its 1 means the model did not load cleanly rather than refuted. Every feature here lands under one that already exists:

The two places an eighth kind could be argued, and why neither earns one.

• cover's not covered. It is a decided absence: neither a discharged obligation (0) nor a refuted one (1). BEHAVIOUR_EXIT_CODES' 2 row already reads "or ANY undecided property", and not covered is decided — so the row gains one clause naming it, rather than the contract gaining a kind. The clause is: "…or a cover property whose behaviour this walk did not find on any run it saw whole, which is a missing behaviour and not a violated requirement — --cover-required spends the 1 for it instead." One sentence in one contract beats an eighth contract that would then have to be quoted by renderCommandUsage, the reference generator and test/unit/cli-reference.test.ts's per-row assertion.
• reach's trap row. A trap is a finding about a machine, exactly like verification/unreachable-state, and reach is report: exit 0 with findings. Giving reach a judging contract would change the meaning of its existing 1 — which today says the model did not load cleanly — for every one of its shipped rows.

Four contract SENTENCES move, across three of the seven constants, in five edits — and the behaviour lane's 0 row is one of them, three times. The draft of this plan said only the 2 row moved, and closed the subject with "Nothing else in any of the seven changes"; that was wrong in the direction that matters, and the first review caught it. The revised version then said the constant did not move again after commit 16, and the third review caught that too — 5b's fair pass discharges under none of the three shapes commit 16 leaves behind (the row below, and §3.5b). Measured, BEHAVIOUR_EXIT_CODES (sysprose-spec.ts:201) publishes its 0 as "every property stated on this machine was shown to hold on every reachable configuration, over a graph this walk saw whole, and there was at least one of them to decide". Today that sentence is true by construction: exit 0 requires every row to be pass, and pass is unreachable past the publishability conjunction at patterns.ts:1178, so exit 0 entails an exhaustive walk. Two of this plan's verdicts break that entailment:

• covered is existential and explicitly stands on a partial walk (§3.1). check-behaviour <reachable probe> --element M --pattern "pattern=cover, …" --max-configs 2 yields one covered row, counts.failed = 0, nothing vacuous or inconclusive ⇒ exit 0, while boundHit !== 'none'. And even on an exhaustive walk a cover is Manna–Pnueli Guarantee (◇β) witnessed on ONE run: on the cover-reachable probe state failsafe holds at exactly one of the reachable configurations, so "held on every reachable configuration" is false of it in a second, independent way.
• 5a's pass holds on every maximal RUN, not on every reachable configuration, and commit 16 decides a liveness pattern — which falsifies the 2 row's clause "a liveness pattern no bad-prefix search decides" the moment it lands.

So the contract moves as follows, and the edits are commits, not review comments:

Nothing else in any of the seven contracts changes, and no eighth kind is created. That sentence has now been wrong twice, so it is stated as a rule with a test rather than as a promise: every commit that creates a new discharge shape re-reads the row it discharges under, and the byte-identity assertions between neighbouring commits are scoped to the rows those commits do not touch (commit 18's, narrowed in §3.5b, is the one this rule was written from). Each edit is asserted in test/unit/cli-reference.test.ts's per-contract block (the BEHAVIOUR_EXIT_CODES block at :206-214) in the commit that makes it, because the same constant is rendered into --help and into the byte-pinned docs/CLI-REFERENCE.md by exitCodesFor. The alternative — routing covered on a non-exhaustive walk to exit 2 — was considered and rejected: it would make --max-configs change the claim of a witness that a bound can hide and can never invent, which is the one thing §3.1's condition row is right about.

2.2 The claim vocabulary opens once, from four words to six

PropertyClaim (patterns.ts:270) is 'pass' | 'fail' | 'vacuous' | 'inconclusive'. It gains exactly two words — 'covered' | 'not-covered' — at the cover commit, used only by cover, and is then closed for the rest of this plan. Every later feature reuses pass/fail:

• recovery is a universal assertion (AG EF p) the author wrote. Its exhaustive refutation is a violated requirement: fail, verification/refuted, exit 1. No new word, and no rendering of one word as another — the JSON claim and the printed sentence must agree.
• existence / response under 5a are assertions: pass / fail.
• cover is the only feature here whose negative answer is a behaviour the design does not admit rather than a requirement the design violates, which is exactly why hard constraint 4 exists.

Why not launder it into the existing four. The cheap option — covered ⇒ pass, not covered ⇒ inconclusive — files a decided answer under the word this tool reserves for undecided. That distinction is the whole load-bearing content of the exit contract, and saving six lines by dissolving it is the one economy this lane cannot make.

The four sites that move together, or the run silently exits 0. A word added to PropertyClaim and not to counts leaves every bucket at zero with rows.length > 0, which falls through the ternary at patterns.ts:1375-1380 to exit 0 — a green run that decided nothing. The sites, measured: counts (:1369-1374, filters by literal string) · exitCode (:1375-1380) · BehaviourVerdict/judgeBehaviour (scripts/sysprose.ts:410-418) · the printed sentence at scripts/sysprose.ts:3235, "pass, fail, vacuous, inconclusive are the four words this command reaches", which appears in every transcript — plus docs/CONFORMANCE.md:882.

The guard that makes the failure impossible: one assertion that counts.passed + counts.failed + counts.vacuous + counts.inconclusive + counts.covered + counts.notCovered === rows.length, on every behaviour fixture.

The new arithmetic:

exitCode =
  counts.failed > 0                                             ? 1
: coverRequired && counts.notCovered > 0                        ? 1
: counts.vacuous || counts.inconclusive || counts.notCovered
    || rows.length === 0                                        ? 2
: 0                                     // `covered` and `pass` are both discharged

--cover-required raises the exit code and never the claim: promoting not-covered to fail would print verification/refuted about a design that violates nothing — the exact defect candidate 1 exists to fix, reproduced by the fix. A test asserts both spellings produce byte-identical claim words and different exit codes.

Severity is a property of the code — but the shipped code does not yet read it that way, and commit 6 is what makes the sentence true. The intent stands: a catalogue entry carries one severity, test/unit/diagnostic-codes.test.ts:67-89 asserts VERIFICATION_ERROR_CODES and VERIFICATION_WARNING_CODES (src/api/verification.ts:1078 and :1061) equal the catalogue's marked verification/* entries exactly, and no flag may re-grade a code. What the review measured is that the behaviour lane does not honour it: behaviourReport's findings loop hardcodes severity: row.claim === 'fail' ? 'error' : 'info' (patterns.ts:1401), so severity is a function of the claim with per-branch overrides above it (--strict-vacuity's own branch at :1384-1397 continues before :1401). A not-covered row is not fail, so verification/cover-required would be catalogued error and emitted info — and the guard cited compares two hand-maintained constants against the catalogue, never an emitted diagnostic, so it stays green through exactly that drift. Commit 6 therefore ships three things together: a dedicated findings-loop branch for not-covered under --cover-required (severity 'error', mirroring :1384-1397), the registration of the new code in VERIFICATION_ERROR_CODES, and the assertion this plan assumed already existed — for every diagnostic any behaviour fixture emits, its severity equals the catalogue's severity for its code.

And the precedent cited for the two-code design does not exist. Measured: verification/vacuous and verification/vacuous-property never coexist. The loop at patterns.ts:1384-1397 handles a vacuous row by continue-ing with no finding when the flag is absent and by pushing exactly one verification/vacuous-property when it is present — one code or none, never two — and the catalogue says so verbatim at diagnostic-codes.ts:586: "check-behaviour raises it from a third row, which carries no code of its own." The SMT lane is a ternary substitution too (api/verification.ts:1626). So the two-code design is this plan's own choice, not an inherited pattern, and the reason is stated rather than borrowed: the info row must survive so that a --cover-required run and a plain run print the same claim word and the same verification/not-covered finding, differing only by the added error and the exit code — which is what §3.1's byte-identity test asserts. An implementer copying the substitution shape literally would drop verification/not-covered on the flagged run, and that is the failure this paragraph exists to stop.

--allow-inconclusive is untouched. It is scoped over SMT-lane codes (docs/04 §2) and the behaviour lane's verification/behaviour-unsupported-construct is published as un-lowerable. Nothing in this plan widens it, and no new code joins its scope.

2.3 The publishability spine, and the absence-claim register

The rule that governs every absence claim exists twice today, as a local const publishable in reachOne (explore.ts:786-787) and a local const exhaustive in checkProperty (patterns.ts:1177-1178), each with a comment saying the other must not be deleted alone. This plan adds five more readers of it. Commit 1 lifts it into one exported predicate and one register, before anything reads it.

// src/semantics/mc/publishable.ts   (new, commit 1)
export interface Publishability {
  readonly exhaustive: boolean;      // walk.exhaustive — boundHit === 'none'
  readonly alphabetOffered: boolean; // every named trigger was actually offered
  readonly supported: boolean;       // walk.unsupported.length === 0
  /** The fifth clause, SHIPPED at `c929278` and not built here (§0.1):
   *  `walk.undeterminedGuards.length === 0` — no transition guard was
   *  consulted and left undecided. Transcribe it as that expression and
   *  nothing else. "No declared value for a feature it reads" is STRICTLY
   *  NARROWER than the shipped predicate — `guardVerdictStore`'s own docstring
   *  says `'undetermined'` also covers a non-boolean operand under
   *  `not`/`and`/`or`, a mixed-type comparison and non-finite arithmetic, so
   *  `not mode` over a fully valued `mode` is undetermined while `mode` is
   *  decided — and a narrower copy would let commit 1 regress a shipped
   *  withholding on a walk its own byte-equality gate cannot see, because none
   *  of the six examples carries a guard at all (§5(d)).
   *  `verification/guard-undetermined` is the warning that prints where it
   *  fails, and the decreasing lists are emptied rather than shortened. */
  readonly guardsDetermined: boolean;
  /** found.boundHit === 'none'. PRODUCT SEARCH ONLY. On a walk-only claim
   *  no search ran, there is no `found`, and this field is absent — never
   *  `false`, which would print "bound exhausted" about a bound nobody hit. */
  readonly searchComplete?: boolean;
  /** The conjunction over the fields present. What a monotone-DECREASING
   *  claim asks for. `reachOne` and today's `checkProperty` read THIS, which is
   *  why they stay byte-identical on every model, timed or not, and it is the
   *  ONLY thing this plan asks of the claims that ship today. */
  readonly decreasingOk: boolean;
  readonly sentence: string;         // the qualification string the row prints
}

/** THE GATE FOR THE WHOLE INCREASING SIDE. One predicate, two named halves.
 *  Read `walkIsExact` from an increasing ABSENCE claim; read
 *  `relationIsTheMachines` from an EXISTENTIAL witness (a bound can hide such a
 *  witness and can never invent one); read `walkIsExact` again from a
 *  MAXIMALITY witness — W3's cycle with no exit, W4's run with no successor —
 *  which a bound and an undecided guard both manufacture. Nothing on the
 *  increasing side reads anything else from this family, and the register's
 *  `kind` column is what selects between the two readings. */
export interface Exactness {
  /** The walk saw the graph whole: `walk.exhaustive` ∧ `walk.boundHit === 'none'`
   *  ∧ `walk.unsupported.length === 0`. Both conjuncts of the first are stated
   *  because the unsupported early return sets `exhaustive: false` with
   *  `boundHit: 'none'` and a bound sets `boundHit` before it `continue`s —
   *  neither implies the other. The `unsupported` conjunct is also where the
   *  ELEMENT-SET half of exactness is enforced; see the note below. */
  readonly seenWhole: boolean;
  /** THE PROPERTY, and the three clauses are how it is checked — not what it
   *  means. What it means: every edge the machine has was retained, and every
   *  edge retained is one the machine has.
   *
   *  The first direction is answered OFF THE MODEL by `edgeCensus`
   *  (`explore.ts`, shipped at `a66ba1f`) and needs no clause here: an edge
   *  under the machine that the relation does not follow and nothing refused
   *  lands in the census's `unaccounted` bucket, which REFUSES the machine
   *  through `unsupportedConstructs` — so `seenWhole` is already false and no
   *  absence, increasing or decreasing, is published over it. That is why this
   *  field has no clause (e) for the succession hole that found it (§0.1).
   *
   *  The three clauses below are the OTHER direction, and they are all of one
   *  kind: an edge that IS in the relation but whose availability at a
   *  configuration the walk gets wrong. The census cannot see any of them,
   *  because to the census the edge is present and walked.
   *   • (b) `walk.timedTransitions` is empty — no transition of this machine is
   *     a dwell, whether or not it contributed a label to the alphabet. The
   *     walk offers the edge without waiting out its dwell, and advances no
   *     clock;                                                               AND
   *   • (c) `walk.alphabet` is empty — this engine cannot establish that an
   *     offered trigger is one the environment could actually supply, so the
   *     only alphabet it can be exact over is the empty one;                 AND
   *   • (d) `walk.undeterminedGuards.length === 0` — no transition guard was
   *     consulted and left undecided. THE SHIPPED FIELD (`c929278`), read as
   *     the shipped predicate: not "no declared value", which is narrower and
   *     which reads empty on `not mode` over a fully valued `mode`. */
  readonly relationIsTheMachines: boolean;
  /** Both. NAMED `walkIsExact`, which is what every register cell, verdict row
   *  and MUST-NEVER in this plan calls it; the function that computes an
   *  `Exactness` is `walkIsExact(walk, bounds)` and returns this field under
   *  the same name, so a row wired to `walkIsExact` names a field that exists.
   *  (An earlier draft declared it `exact` here and used `walkIsExact`
   *  everywhere else, which would have landed commit 1's reflection test red
   *  against a producer with no such field on nine rows.) */
  readonly walkIsExact: boolean;
  /** Which clause failed, for the `inconclusive` sentence. Exactly one is
   *  reported, in THIS order, so two machines that fail for two reasons never
   *  print the same sentence:
   *    'bound'       — !walk.exhaustive with a boundHit
   *    'unsupported' — the early return for a refused construct, which includes
   *                    an `unaccounted` census row
   *    'environment' — `alphabet ∖ timedLabels` non-empty: a named trigger that
   *                    is not a dwell label. FIRST of the three relation
   *                    clauses, because an author whose machine names `abort`
   *                    has something to do about it and the dwell sentence
   *                    would send them to the wrong carrier (§3.R rows 5-6)
   *    'time'        — not the above, and `timedTransitions` non-empty
   *    'store'       — neither, and `undeterminedGuards` non-empty
   *  The draft ordered 'time' before 'environment', which contradicted §3.R's
   *  own row-precedence test (row 5 beats row 6 on a machine carrying both). */
  readonly failedClause:
    | 'bound' | 'unsupported' | 'environment' | 'time' | 'store' | null;
  /** The one-line reason, printed beside every claim this gate withholds. */
  readonly sentence: string;
}

One name per predicate, and the numbered-condition vocabulary survives only on the decreasing side. walkIsExact(walk, bounds): Exactness is the function; where a register cell, a verdict row or a MUST-NEVER says walkIsExact it means that function's walkIsExact field, and where a row needs one half it names the half — seenWhole or relationIsTheMachines. The numbered conditions belong to Publishability and to nothing else, and the mapping is recorded once, here, so an older reading of a §3 row can be checked against it: PC1 → Publishability.exhaustive, PC2 → .alphabetOffered, PC3 → .supported, PC4 → .searchComplete. There is no PC5 and there never was one in this document's own vocabulary — the draft's fifth, time-only condition has no numbered successor; it is a clause of relationIsTheMachines, and a clause of the gate is named by its letter and its producer, never by a number. Publishability.guardsDetermined shipped at c929278 and has no number either. No PC name appears in publishable.ts, in a register cell, in a verdict row, in a MUST-NEVER list or in a test name, and a cell naming one is a red test in exactly the way a per-mechanism conjunction is — the numbers are what let the last two rounds of this defect be re-argued one row at a time, and they survive here only as a decoder ring for the decreasing conjunction.

exhaustive, alphabetOffered and supported are reachOne's conjunction verbatim; searchComplete is checkProperty's extra conjunct; guardsDetermined is the fifth conjunct that shipped at c929278 (§0.1). Together they are decreasingOk, which is what the claims that ship today already read and what they keep reading, unchanged, byte for byte — against the dc6662c golden, which is the baseline commit 1's byte-equality gate is measured on.

Why the gate is a predicate and not a list, stated once here and not re-litigated per feature. Five readers have now found five distinct ways the retained relation differs from the machine an author wrote, one per review round, each invisible to the condition set built for the last one. That is not five bugs; it is one observation about the method. Enumerating mechanisms cannot converge, because the enumeration is written by reading the code and the next mechanism is precisely the one the code did not make visible. So the question is inverted, and the tree has already shipped the inversion: edgeCensus counts the edge-bearing elements under a machine without asking the walk and requires each one to land in a bucket that says what became of it. An edge nobody thought about does not shrink an absence list quietly; it lands in unaccounted, fails a test and refuses the machine. The five mechanisms below are the evidence for that rule, not the definition of it, and they divide cleanly along the line the census draws:

1. Time, over-approximating — the walk's offering, not the edge set. machineAlphabet (explore.ts) puts every after(n) label in the alphabet by design; exploreMachine offers every alphabet member wherever it takes an event; matches (config.ts) applies the dwell test only on the timeout branch, and the walk issues no timeout and advances no clock. The edge is in the relation; what is wrong is when it is available. Clause (b).
2. The cooperative environment, over-approximating — also the offering. Every trigger in the alphabet is offered wherever the walk can decide that the interpreter takes its next event — at a configuration where no completion transition is due, and at one where the 64-step chase budget is spent with a completion transition still due — whatever an environment would actually send there. [Dated note, 2026-10-15 (O1 behaviour-sound, review B's M1): this item first read that every trigger was offered everywhere, unconditionally, which was the walk at dc6662c. H1 (0c9d2bd) made the walk obey run-to-completion and offer an event only where no completion transition is due, which lost the runs the interpreter takes where its chase budget stops (§8.5); since §8.5 the walk offers the alphabet there too. On a walk that finished, where an event arrives is now the interpreter's exactly, and an absence the walk publishes is exact over that semantics — the U2 fallback, which would have offered the alphabet on whole completion cycles, was not needed. The one place the two part is one the walk cannot decide: where nothing is due but a completion transition whose guard is undecided, the interpreter reads the guard as false and takes its next event, and the walk offers no trigger — it fails closed, and reading 3's store clause withholds every absence on the machine (§8.7). What stays over-approximated is WHICH trigger arrives: every one, at every such place.] Measured on a clean-loading file — state nominal; state locked; transition nominal then locked; transition locked accept unlatch then nominal; — reach prints 2 configuration(s) explored, depth 1 — exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64, alphabet unlatch}, 2 of 2 state(s) reachable; 2 of 2 transition(s) fired, 0 dead, rc=0, no findings. Every publishability condition holds — the guard clause included, since this machine has no guard at all — and no transition is a dwell, so the retained relation is one SCC of two containing the opening: exemption 3 fires, §3.2a would publish no component of this walk is inescapable beyond its endings, and §3.2b would answer recovery p = state nominal with recoverable at exit 0 — about a design in which locked → nominal exists only because the walk hands the machine unlatch wherever it takes an event. In the system where unlatch never arrives, locked is an inescapable mode: the defect §3.2a exists to find, published as its negation. Clause (c).
3. The undecided guard, under-approximating — the offering again, in the other direction. seedStore (config.ts) sets a feature only where literalValueOf(f) !== undefined, so a guard over an attribute declared without a literal evaluates undefined; before c929278 guardHoldsStore collapsed that into false and the machine's edge was simply missing from the walk with nothing said. Measured at 2aced3c on attribute resetOk : Boolean; with transition nominal then degradedA; transition degradedA then degradedB; transition degradedB then degradedA; transition degradedA if resetOk then nominal;: 3 configuration(s) explored, depth 2 — exhaustive under {…}, 3 of 4 transition(s) fired, 1 dead, rc=0, every publishability condition of the day holding. c929278 closed the decreasing half — re-executed at dc6662c the same file reports undetermined under {…} — 1 guard(s) the walk could not evaluate, 3 of 4 transition(s) fired, dead withheld, rc=0 — and left the increasing half exactly where it was: the retained relation still holds a non-trivial bottom SCC that does not contain the opening and whose states are neither final nor terminal, so all three of §3.2a's exemptions still pass, and without a gate §3.2a would publish trap — 2 configuration(s) form a set nothing leaves: {degradedA, degradedB} and §3.2b would answer not recoverable: 2 configuration(s) cannot reach \state nominal`, verification/refuted, **error, exit 1**, on a design whose escape edge the model states. **Clause (d)**, and it reads the field c929278` shipped rather than a narrower re-derivation of it.
4. The unlabelled dwell — the same mechanism as 1, reached through the producer nobody instrumented. A transition carrying a numeric attrs.after and no attrs.trigger is timed by the tool's own predicate (afterDuration reads the number before it tries the string), is a completion transition to isCompletion so matches never reaches the dwell test, and contributes nothing to the alphabet because triggerLabelOf is ''. Measured on a Model+ModelFactory machine — failsafe --after(5)--> failsafeHold, failsafe --after(60)--> standby, failsafeHold --after(5)--> failsafe, all three written m.create('TransitionUsage', {attrs:{after: n}}) — afterDuration(t1) = 5, isCompletion(t1) = true, alphabet = [], configs 3 exhaustive true boundHit none unsupported 0 offered [] fired 3 reachable 3. A clause (b) scoped to alphabet contributors reads empty here, clause (c) reads empty and clause (d) reads empty — the gate would return true on a machine every one of whose edges is a dwell the walk erased. So clause (b)'s producer is the TRANSITION SET and not an alphabet subset, the timedLabels ⊆ alphabet containment and the "clause (c) entails clause (b)" inference that rested on it are deleted, and the per-step disjunction tests afterDuration on the step's transition id and never on the recorded label, which for such a step is ''. This one is not a fifth mechanism; it is the first mechanism read through the wrong field, and it is the sharpest argument in this section against clause-by-clause reasoning.
5. The missing edge KIND — the element set, and the one the census now owns. A succession degradedA then nominal; written between two states of a state def parsed clean, landed in the model as a real edge, and was dropped by the step relation because that relation enumerated TransitionUsage alone. Every clause above read green on it: no dwell, no alphabet, no guard, exhaustive, nothing unsupported. It manufactured a trap and a not recoverable at exit 1 in the increasing direction and invented a verification/unreachable-state and a verification/deadlock in the decreasing one — the only mechanism so far that falsifies both sides. It is FIXED at a66ba1f (STEP_EDGE_KINDS is {TransitionUsage, Succession}; SuccessionFlow is refused by payload) and, more to the point, the class is closed: edgeCensus reads its domain off model.descendants(machineId) — every element carrying an endpoint — so a sixth edge kind lands in unaccounted, refuses the machine, and is caught by the census's own test before any absence is published. Re-executed at dc6662c, the probe walks 4 of 4 transition(s) fired, 0 dead and raises the nondeterminism row the fourth edge creates.

What that leaves the gate to do, exactly. relationIsTheMachines asks one question — is the relation this walk retained the machine's relation? — and it is answered in two places, deliberately: the element set by the shipped census, which needs no clause here because an unaccounted row already refuses the machine and therefore already falsifies seenWhole; and the availability of an edge at a configuration by the three clauses, which the census cannot see because to the census those edges are present and walked. A sixth mechanism of the first kind costs this plan nothing — the census catches it and no register row, verdict table or commit moves. A sixth mechanism of the second kind costs one clause inside Exactness and, still, no register row, no verdict table and no commit. That is the whole property the collapse was built for, and it is why the answer to "a fifth mechanism will be found" is not a fifth patch.

What the gate costs, and where it is unfalsifiable. Clause (c) is the expensive one: the alphabet must be empty. This engine has no carrier for "which triggers can the environment actually supply", so the only alphabet over which it can honestly claim exactness is the empty one — and that is a real narrowing, not a formality. It means A6 (traps), A7 (recoverable) and A11 (no fair cycle) publish only on completion-driven machines. §5(d)'s measured survey says what that costs today, and it is the kill-measurement every feature that reads this gate is retired on: all eleven analysable machines in this tree have an empty alphabet and no dwell transition, so the gate suppresses nothing that ships — and no model in the corpus can falsify clause (b) or clause (c): there is no after(n) and no accept anywhere in it. Clause (d) is the exception, and it is a recent one: test/fixtures/verification/models/guard-undetermined.sysml (c929278) carries an undecidable guard and two decided controls, so that clause has a corpus witness and this plan's trapguard fixtures extend a family rather than inventing one. Every inconclusive path this predicate creates is exercised only by the fixtures this plan invents (the latch machine, the trapguard machine, the preempted-dwell machine, and the numeric-attrs.after machine of reading 4 above), which makes those fixtures the only coverage those branches will ever get and not optional colour. The element-set half is the exception and it is worth saying why: census.unaccounted is checked on every machine every walk, including all six that ship, so the one clause of exactness with real corpus coverage is the one this plan does not implement. §5 states this plainly rather than implying the corpus exercises them, and each affected feature's census row carries the same number as its own kill-measurement.

And one thing the gate does NOT cover, which must print anyway. walkIsExact says the walk explored the machine's relation. It does not say the walk explored what the shipped simulator does: measured, verification/nondeterministic-choice reads 1 on UAVSurveillanceSystem::FlightModes (at autonomous) and 1 on VehicleModel::VehicleStates (at idling) — on two of the three shipped machines the walk explores both branches of a declaration-order tie-break that runStateMachine resolves by firing enabled[0]. That is exact for the machine and inexact for the simulator, so §2.4 gains a fourth standing sentence saying so, printed on every increasing claim.

There are two conjunctions and not one, and that is a correction the second review forced. The draft exported a single ok, "the conjunction over the fields present", and it would have shipped a regression on already-shipped behaviour the moment commit 3 landed. reachOne has one call site for its conjunction — const publishable = walk.exhaustive && alphabetOffered && walk.unsupported.length === 0 && guardsDecided, four conjuncts at dc6662c, not the three it had before c929278 — feeding five published fields: unreachable: [], dead: [], exhaustive, suppressed, and the qualification string with its four branches. A1/A2 are monotone-decreasing: the polarity argument below is that the time clause is unnecessary for them. Under a single ok, any machine carrying an after(n) transition would flip publishable false, empty a sound verification/unreachable-state finding out of a shipped command, and print the partial under {…} — a trigger the machine names was never offered branch when every trigger was offered. The register's walkRequires column is per claim; a boolean cannot express it. So each claim's producer reads the conjunction its own row names — decreasingOk on the decreasing side, Exactness.walkIsExact or Exactness.relationIsTheMachines on the increasing one — and the reflection test of §5(a) asserts the selection rather than trusting it. The regression is also invisible to commit 1's gate — byte-equality on the six examples, none of which contains an after(n) transition, a named trigger or a guard (measured, §5's census; and correction 22 says why no .sysml file will ever carry the first) — so commits 1 and 3 each carry a factory-built timed machine in their differential, which is the only input that can tell decreasingOk and the exactness gate apart.

The polarity rule, which the draft of this plan did not state and which is the reason the increasing side is gated at all. Publishability is not one property. An absence claim is a statement of the form "no object of this kind exists in the graph", and the graph this lane reasons over is not the machine's: it over-approximates what the machine offers in two ways (a dwell taken with no clock, a trigger nobody would send), under-approximates it in a third (an edge behind a guard nothing decided), and — until a66ba1f — could miss an edge kind outright, which is the one direction that falsifies both sides at once and the one the census now closes off the model rather than off the walk. Two things follow, and they point in opposite directions:

• A1 and A2 — the two absence LISTS reach publishes today — are monotone-DECREASING in the edge relation. (A0, the third shipped claim, is the exception that proves the rule and is why it has its own row: it is decreasing in the two over-approximating mechanisms and increasing in the undecided-guard one, because a missing edge invents a deadlock rather than hiding one — which is exactly why c929278 gates it, and why the row survives as a register entry over shipped machinery rather than as a code change.) Add edges and the unreachable list can only shrink and the dead-transition list can only shrink. That is precisely why the over-approximation is sound for them, and the engine says so in its own words, in explore.ts's header: "an over-approximation can only shrink the absence claims, never invent one, which is the direction a finding may be wrong in", and again in profile.ts's time facet, "the unreachable and dead lists stay lower bounds." Both sentences are about an over-approximation and neither covers a missing edge, which is why reading 5 above falsified them and why the census, not a clause, is what makes them true again. A5 (not covered), A3 (pass) and A4 (vacuous) are decreasing for the same reason: every one of them gets harder to state as edges are added, and they keep decreasingOk and nothing more.
• A6, A7, A11, A12 and A13's positive half are monotone-INCREASING. "Nothing this walk found is inescapable", "state standby is reachable from every reachable configuration", "no fair cycle", "no simulation relation", and every published witness — a cover, a trap entry, a cut set — get easier to state as edges are added. The exact mechanism that protects A1/A2 falsifies them, and they read walkIsExact.
• A8 (guaranteed) and A10 (holds on every maximal run) are decreasing in edges and still read the exactness gate, which is the case that shows why the mechanisms are not all edge-polarity phenomena. Both quantify over the run set, not over the edge set, and the cooperative environment changes the run set in a direction the edge polarity does not see: on the measured latch machine, nominal forever is a maximal run of the system and is not a run of the walk at all, so guaranteed is published about runs that were never candidates. Their own §3 sections already required an empty alphabet for exactly this reason; reading walkIsExact is that clause plus three more, and it removes the third independent spelling of one idea.

The polarity column stays honest, and the executable column is SPLIT IN TWO — which is the decision the fourth review forced, because the draft's "one of exactly two values" was false of nine of its own fifteen absence rows and of all six of its witness rows. The draft asked one column to hold both the walk predicate a producer reads and every non-walk conjunct a claim happens to need (acyclicity, a fair continuation, four solver digests, a non-empty dependency template), then asserted by reflection that the column held one of two values. That test could not have been written against the plan's own data, and the repair under a red gate is to weaken the test. So the register carries two columns and the assertion moves to the first:

• walkRequires — what the producer reads out of this family, and it takes one of exactly four values: 'decreasingOk', 'walkIsExact', 'relationIsTheMachines', or null for a claim that is not about a walk at all (A9, A14, A15). relationIsTheMachines is admissible because it is what a positive existential witness reads — a bound can hide a witness and can never invent one — and the draft's two-value rule made every witness row illegal by construction, which is how the register and §5(a) came to assert something no row could satisfy.

• alsoRequires — free-form conjuncts that are not members of this family: acyclic === true, the fair-continuation condition, both run classes checked, the four digests of A9, a non-empty dependency template. A per-mechanism conjunction is still a red test in walkRequires; what is now legal is a shape conjunct that was always legal and had nowhere honest to sit.

• polarity — and this column takes the same treatment walkRequires just got, because the two-value version of it was false of six of the plan's own fifteen absence rows in exactly the way the requires column was false of nine. It is a closed enumeration wide enough for its own data: 'decreasing' | 'increasing' | 'mixed' | 'not-a-walk'. mixed is A0 (decreasing in the over-approximating mechanisms, increasing in the undecided-guard one), A8 and A10 (decreasing in edges, but quantifying over the run set) and A13 (no cut set decreasing, each published cut set increasing); not-a-walk is A9, A14 and A15. Beside it sits polarityNote, free-form, which names the mechanism the polarity flips in — "increasing in the undecided-guard mechanism: a missing edge invents this row", "over the run set, which the cooperative environment changes" — because that detail is what the reflection test needs and what a two-valued cell was silently dropping.

The reflection test asserts, mechanically: walkRequires is one of the four values; A1–A5 read decreasingOk byte-identically to their shipped conjunctions; no alsoRequires entry on any row names a member of the bound family (seenWhole, decreasingOk, Publishability.searchComplete) — that is where a bound condition would otherwise creep back onto a witness one conjunct at a time; and walkRequires: null appears only on a row whose polarity is 'not-a-walk'. And the polarity rule, restated so that it is satisfiable and still bites: no row whose polarity is 'increasing' or 'mixed' may have walkRequires === 'decreasingOk' unless its alsoRequires names a conjunct that covers the mechanism its polarityNote identifies. Exactly one row in the register uses that escape — A0, whose leaf-wise guard conjunct covers the one mechanism its note names — and it is legal by stating why, which is what the two-valued column could only have achieved by mis-typing the row. A row whose polarity is 'decreasing' and whose walkRequires is the gate is legal in the other direction with no escape needed, and states the strengthening in its own Otherwise cell; the reverse, unexcused, is a red test.

The over-approximation is not hypothetical and it is not a bound. machineAlphabet (explore.ts, and its own docstring says so) puts every after(n) spelling in the alphabet on purpose; exploreMachine offers every alphabet member wherever it takes an event; and matches (config.ts) tests the dwell only on the timeout branch — cfg.clock - entryTime[sid] >= n — while the walk issues no timeout input and advances no clock. Measured, on a machine built through ModelFactory — f.transition(failsafe, failsafeHold, { trigger: 'after(5)' }) declared before f.transition(failsafe, standby, { trigger: 'after(60)' }) — the interpreter fires enabled[0] on any clock advance (execute.ts), so no run ever takes the dwell-60 edge and {failsafe, failsafeHold} is an inescapable trap — the exact defect §3.2a exists to find. The walk offers "after(60)" as a named event with no dwell test, the escape edge exists in successors, the component is not bottom, and the walk is fully exhaustive: boundHit: 'none', alphabet offered, nothing unsupported, the census clean — every edge of this machine is walked, which is the point: the census is blind here by construction, because nothing is missing from the relation. Under the draft's four publishability conditions, A6 and A7 both held; recoverable printed at exit 0 and reach --json said nothing was inescapable. Under walkIsExact the machine fails clause (b) and clause (c) — it has dwell labels, and it has a non-empty alphabet — and both claims are withheld with the failed clause named. No compensating diagnostic fires — recordNondeterminism is per (configuration, input) and the two transitions match different trigger strings, so there is not even a verification/nondeterministic-choice row. And §2.4(a)'s standing sentence does not cover it: a dwell is not a trigger an environment can withhold, so that disclosure names the wrong hazard.

And the dwell fixture is written through the factory because it cannot be written any other way — correction 22, and it re-frames what clause (b) costs and what it buys. accept after(n) is a parse error: measured, npm run check on a file carrying transition failsafe accept after(5) then failsafeHold; reports expected: then | -> found: ( and FAILED — 8 error(s), rc=1, because AcceptClause is 'accept' payload=QualifiedName (sysml.langium:214-215). The escaped spelling accept 'after(5)' parses and is a different trigger string — quotes included — which afterDuration (config.ts:265-270) does not match, so it is not a timed transition either. A timed transition is therefore API-only, exactly like attrs.parallel: it arrives through ModelFactory's { trigger: 'after(5)' } or a numeric attrs.after, and never from a .sysml file. Three consequences run through the rest of this plan, and none of them is that clause (b) is dropped — the SDK is a supported surface, reach, check-behaviour and fault-tree all run over API-built models in-process, and the over-approximation is real there:

1. Every dwell fixture in this plan is factory-built, in a .test.ts. The names stay — the two-dwell fixture, the preempted-dwell fixture — but they are ModelFactory machines, never corpus files. A campaign fixture written in text would fail the corpus gate on landing with 6–8 parse errors and then assert a failed time clause over a walk that never ran.
2. No time-clause assertion is made at the CLI level. Commits 6, 8, 9, 16 and 23 assert the dwell rows through the in-process API (checkProperty, reachReport), not through check-behaviour/reach argv. The environment and store clauses are the opposite — the latch machine and the trapguard machine are ordinary .sysml files that load clean (both measured this session), so those two clauses are asserted through argv as well as in-process, and they are the only clauses of the gate a corpus fixture can reach.
3. The dwell census is a census over SDK-built machines, not over a user's .sysml corpus. On anything a CLI command can load timedTransitions.size is 0 by construction, so §5's commit-3 row is re-priced accordingly: it can retire the time clause's apparatus only against API traffic, and against text models the honest reading is that the clause costs nothing and guards a surface only the SDK reaches.

The gate's producers, and TWO OF THE FOUR ALREADY SHIP. Read this list as what the gate reads, not as what commit 2 builds; the Files: line in §4 is what says which of them is new.

• timedTransitions: ReadonlySet<ElementId> — clause (b)'s gate producer. NEW, commit 2. Recorded by exploreMachine over walkableTransitions(model, machineId).filter(tr => afterDuration(tr) !== undefined) — the transition set, not the subset of the alphabet those transitions contributed, which is the correction reading 4 forced above: a numeric attrs.after with no trigger is a dwell that contributes no label, and a clause scoped to alphabet contributors reads empty on a machine made entirely of them. afterDuration has two producers, a numeric attrs.after and a trigger string matching /^after\s*\(\s*n\s*\)$/; correction 22 measured that neither is writable from the notation — the first arrives through model.create (not a ModelFactory.transition option, which accepts only {ownerId, trigger, guard, effect} and silently drops the rest) and the second through ModelFactory's { trigger: 'after(5)' }.
• timedLabels: ReadonlySet<string> — not a gate producer. NEW, commit 2. The alphabet members contributed by those transitions, retained for one job only: deciding whether a non-empty alphabet is real triggers or all dwells, which is what §3.R's rows 5-6 and §3.5a's rows 2-3 split on and what failedClause's 'environment'-before-'time' order is computed from. The containment claim — timedLabels ⊆ alphabet, therefore "clause (c) entails clause (b)" — is deleted. It is true of the field and false of the clause: the two clauses are independent, and the machine that shows it has alphabet === [] and three dwell transitions.
• bounds.alphabet — clause (c). Already computed and already published on every bounds line; the gate reads alphabet.length === 0 and nothing new is produced.
• walk.undeterminedGuards — clause (d). ALREADY SHIPPED at c929278, as readonly UndeterminedGuardRow[] on ExploreResult, populated by stepCandidates — "returns the enabled transitions and the guards that decided" — and already read by reachOne as the fifth publishability conjunct. The gate reads walk.undeterminedGuards.length === 0 and nothing else. No second field, no narrower re-derivation, and no edit to guardHoldsStore or its callers: a second copy under a second name is precisely the drift config.ts's own header exists to prevent, and the narrower reading would go green on not mode over a fully valued mode. On the decreasing side this clause is not this plan's — the earlier warrant here, "the walk and the interpreter agree there, so no publishability condition on that side can see it", was true of unreachable, dead and not covered, whose polarity a missing edge does not flip, and false of verification/deadlock, whose polarity it inverts outright. c929278 closed that too, gating the deadlocks array on the guards alone. What survives here is register row A0, which is now a row about shipped machinery plus one strengthening (below).
• walk.census — no clause, and that is the point. census.unaccounted non-empty already refuses the machine, so seenWhole carries the element-set half and the gate needs no producer for it. It is read by §5's exactness census as a recorded number.

Equivalently and more cheaply stated: every retained edge is an edge the machine has, and every edge the machine has was retained — the second half checked off the model by the census, the first half by the three clauses. Where the gate fails, the honest answer is stated per feature — an inconclusive naming the failed clause for A6, A7, A8, A10, A11, A12 and A13, and a re-worded or withheld witness for every positive claim (§2.4(c), and WITNESS_CLAIMS per row) — never a silent publish.

A sixth mechanism arrived while this section was being written, and it is left without a clause on purpose. Run-to-completion preemption is an availability difference: a transition the model states can be unavailable at a configuration because the completion chase took the machine elsewhere first. It is the second kind, so by the rule stated just above it would cost one clause — and it is recorded here instead, because six mechanisms found by six readers is no longer a list that can be completed by looking harder. What closes this class is the element-set half, which edgeCensus answers off the MODEL without asking the walk: an edge nobody accounted for refuses the machine whether or not anyone predicted the way it would go missing. A seventh will arrive. The register's job is to make its arrival a red test rather than a published sentence, and the census is the half that does that without being told what to look for.

The seventh arrived (2026-10-14, review B's C1 and H2), and it is the chase budget. The interpreter chases trigger-less transitions for at most maxCompletion (64) steps after each event and then takes the next event wherever the chase stopped; the walk read the budget as a bound instead, and on a completion cycle never met it at all. It is fixed in the walk, not gated: the walk now follows the budget (§8.5), so the decreasing claims are about the interpreter's runs again. What remains is one clause on the increasing side — (e), chaseStops === 0, failedClause === 'budget': where the budget stops a chase with a completion transition still due, the walk follows the interpreter and does not fire it, so the relation holds a resting point the budget makes where the machine states an edge. It is evaluated after (d), so only a machine with no trigger, no dwell and no undecided guard is ever told it. A machine that names no trigger at all keeps the relation it states and fails no clause for the budget: there only the two claims read over where a run ENDS — A7's recoverable and A8's guaranteed — are checked against the configurations where the budget stops its one chase (budgetStops, §8.5), and each register row names that conjunct. So, since the branch review, is the run W3's potential names: a cycle or a sink of G₀ only where a path inside G₀ reaches it within the budget, else the run the budget stops inside G₀.

And the bounds line names the store, in every lane, because that is what exhaustive under {…} has always meant. Correction 23's clause is lifted out of §3.1 and into boundsSentence itself, which today names maxConfigs, maxDepth, maxCompletion and alphabet and omits the one parameter that decided the trapguard measurement above. After commit 3 it reads …, store seeded from declared literal values — a guard over an attribute with no declared value is read as false. One edit covers A5, A6, A7, A8, A10 and A13 at once, and it is the honest reading of the qualification string every one of them prints. It is a disclosure and not a clause, and it says less than clause (d) does: c929278's predicate covers guards that decided nothing for reasons other than an undecided feature, and the bounds line names only the common one. Where the two differ the verification/guard-undetermined row is what a reader acts on.

What the exactness gate is NOT for. It is not a truncation flag. A truncation flag was considered and rejected as a soundness device: measured, every bound gate in exploreMachine — completion, depth, configs — sets boundHit before it continues, so an edge into a dropped successor always implies !exhaustive, which already implies !decreasingOk. What ships beside the gate is one walk-level boolean, openFrontier, defined as !walk.exhaustive — not as boundHit !== 'none', and the difference is a real bug the review caught. exploreMachine has an early return for a refused construct that sets configs: 0, exhaustive: false and boundHit: 'none': no bound was hit because no walk happened. Reproduced from ordinary surface syntax — a transition with an unresolved endpoint gives reach dangle.sysml → 0 configuration(s) explored … not explored — transition-without-endpoints, so this is reachable from the corpus and not only through attrs.parallel via the API. Under the draft's definition that walk would publish openFrontier: false and, over an empty successor relation with no cycle, acyclic: true — a census field asserting a property of a graph that was never built, on the one machine class the tool refuses to walk, flipping lane G's release gate on a false reading. So: openFrontier === !walk.exhaustive is what the test asserts (the draft's openFrontier === (boundHit !== 'none') would have pinned the bug), and the census field acyclic is three-valued — true | false | null.

And acyclic reads null whenever walkIsExact is false, not merely whenever openFrontier is true — which is the fourth review's correction and is the difference between a census and an artefact. Acyclicity of the retained relation is precisely the property clause (d) manufactures: an edge the model states and seedStore never offered is a cycle-closing edge that is simply absent. Measured on the trapguard shape's two-state sibling — attribute resetOk : Boolean; with transition nominal then degraded; transition degraded if resetOk then nominal; — the retained relation is two nodes and the single edge 0→1, so acyclic reads true on a machine whose stated relation has the cycle nominal → degraded → nominal. Re-measured at dc6662c the printed report is undetermined under {…} — 1 guard(s) the walk could not evaluate, 1 of 2 transition(s) fired, dead withheld, boundHit none — the report is withheld and the relation is unchanged, which is the whole point: c929278 gates what is published and does not add the edge back. A10 is safe on its own (it conjoins the gate), but the census field is not A10 — it is published in --json as a fact about the machine and it is the number §5's table and lane G's release gate read, so a corpus machine that is acyclic only because a guard was unbound could flip lane G green and release §3.5a on a measurement of an artefact. §5's note that not one transition in this repository carries a guard is the same sentence read the other way: the first user model that does is also the first model that can flip this gate. Lane G's release condition therefore counts only acyclic === true on a walk where walkIsExact holds, and §3.P's test list asserts acyclic: null on the trapguard file and acyclic: false on its = true variant, with acyclic: true named as the wrong answer.

The register. Every claim in this plan whose truth is "nothing of this kind exists" is a row of data in publishable.ts, and test/unit/semantics.mc.publishable.test.ts asserts by reflection that each registered claim's producer is unreachable unless its condition holds. Each row also carries its polarity — 'decreasing' | 'increasing' | 'mixed' | 'not-a-walk', plus a free-form polarityNote — and the reflection test asserts the rule mechanically in the form stated above: no increasing or mixed row may read decreasingOk unless alsoRequires names a conjunct covering the mechanism its note identifies. That is how the polarity argument stops being prose. walkRequires takes one of exactly four values and alsoRequires holds everything that is not one of them (above), so the register is the wiring between the predicate and the claims and the reflection test checks the wiring rather than trusting the implementer to have read the right field. Any per-mechanism conjunction in walkRequires is a red test: the whole point of the collapse is that the increasing side has one gate and no menu.

The Polarity column below carries the enumerated value in bold and the note after it.

A0 was the fourth review's finding, and the fifth review found that the tree had closed it first — so the row survives as a REGISTER ENTRY over shipped machinery, plus one strengthening. verification/deadlock — "no transition is enabled at this configuration" — is a fifth absence claim reach publishes, and it was in neither register. It used to be emitted unconditionally: reachOne returned deadlocks: walk.deadlocks with no guard, in contrast to the neighbouring unreachable and dead. c929278 gated it, and gated it on exactly the argument A0 was written from — the comment above the line says so: "Gated on the guards ALONE, not on publishable. A deadlock row says one configuration the walk REACHED had no enabled edge out, and a bound cannot make that wrong … An undetermined guard CAN make it wrong: it is an edge out that may have been enabled, and nothing here decided whether it was." The shipped expression is deadlocks: guardsDecided ? walk.deadlocks : [].

So the pre-c929278 measurement this row was built on no longer reproduces, and quoting it would send an implementer to write a fixture that cannot fail. Re-executed at dc6662c on the file A0 named — package P { state def Modes { attribute resetOk : Boolean; state nominal; state degraded; transition nominal then degraded; transition degraded if resetOk then nominal; } } — reach --json gives "exhaustive": false, "boundHit": "none", "deadlocks": [], "suppressed": true, and one finding, verification/guard-undetermined. No deadlock row, and no dead-transition row either. The pre-c929278 transcript (deadlocks ['P::Modes::degraded'], codes ['verification/dead-transition','verification/deadlock'], rc 0, with the shipped hint "Give it a way out" on a model that states one) is retained above only as the record of what the defect was.

What is left for this plan is one strengthening, and it is stated unambiguously because the earlier wording contradicted itself. The shipped gate is walk-wise: one undetermined guard anywhere in the machine empties the whole deadlocks array. A0 proposes to make it also leaf-wise — decreasingOk ∧ (no outgoing transition of the deadlocked leaf is in walk.undeterminedGuards) — so that an undecided guard in one region does not silence a genuine, fully-decided sink in another. That is a strengthening of the row's availability, not a relaxation of its gate: the walk-wise conjunct stays and the leaf-wise conjunct is added on top. The earlier phrasing said "suppressed leaf-wise, not walk-wise" in one clause and "the walk-wise clause is the first conjunct" in the next; read the first way it would have regressed c929278, and read the second way it is a no-op on every input this plan names. It is written as a conjunction here and nowhere else.

And the fixture the row needs is one no earlier revision named, because on the trapguard family the two gates agree: a machine with an undetermined guard in one region and a real, fully-decided sink in another. That is the only input on which the leaf-wise conjunct changes an output, and without it commit 3's A0 assertion passes vacuously. §5(d)'s two fixture machines that do carry a deadlock (on, running) carry no guard at all, so both gates are vacuously true on them and their goldens do not move; no shipped example carries a deadlock row, so the campaign's exact diagnostics array does not move either. The motivating contradiction also has a sharper form now, and it survives c929278: the succession probe of reading 5 invented a verification/deadlock with every guard clause vacuously true — which is what the census, not this row, is what closes.

A9 is the odd one out, deliberately: it is the only row whose condition is not a walk fact at all but a set of global solver facts (§3.3b). A13 is the second odd one: its two halves have opposite polarity, so it is the one row where the gate holds a report rather than a sentence — the no cut set half would survive without it, but the two print together and a reader cannot be asked to know which half is which.

Why A7 names no product-search condition, stated so the register is not decorative. §3.2b makes recovery a dispatch arm that never reaches search, and the commit's headline test asserts exactly that. With no search there is no found, so Publishability.searchComplete has no value on this path. The draft required it anyway, which is executable — the register is asserted by reflection — and so had two failure modes and no third: read as false, recovery on examples/uav-isr.sysml with p = state standby (an exhaustive four-configuration walk, boundHit: 'none') publishes "inconclusive: bound exhausted" about a bound nobody hit and §3.2b's own recoverable test goes red; read as vacuously true, the register row is decoration and the reflection test passes on nothing. The collapse fixes this by construction: Exactness has no searchComplete field to get wrong. searchComplete stays optional and absent on decreasingOk for walk-only claims, asserted once in semantics.mc.publishable.test.ts.

The second register: positive witnesses, because a refutation is a positive claim too — and an EXISTENTIAL one reads the RELATION half of the gate, not the whole of it, while the two that are maximality claims read all of it. The draft registered absences and left every witness to prose, and the second review found the hole in three places at once: §3.1's two covered rows leave a walk with dwell labels whose witness fired no after-label matched by neither row, with no test that could go red either way; §3.R's potential names an avoiding cycle computed over the retained relation and is gated on nothing; and §3.5a's fail and §3.5b's refuted under fairness spend exit 1 on a witness run — the existence of a p-free maximal run is monotone-increasing in the edge relation, which is the polarity §2.3 says the approximation falsifies. So publishable.ts carries a second table, WITNESS_CLAIMS, with the same shape and the same reflection assertion, and §5(a)'s "the polarity rule is machine-checked" becomes true of witnesses as well as absences.

And the split of the gate is forced by measurement, not by taste. A witness row must read relationIsTheMachines and must not read seenWhole, because a bound can hide a witness and can never invent one — while a wrong relation can invent one. Measured at this plan's own named boundary: check-behaviour examples/uav-isr.sysml --element FlightModes --pattern "pattern=absence, scope=globally, p=state failsafe" --max-configs 3 (witness depth 3) gives rc=1 FAIL with the qualification 3 product state(s) explored — **partial under** {maxConfigs 3, …} — the configuration bound was reached; at --max-configs 4 the same row reads exhaustive under. cover reuses that identical breach, so a witness row that required seenWhole would make commit 6's own headline test ("--max-configs <depth> keeps covered", §3.1) and §5(a)'s reflection test mutually unsatisfiable — one of them lands red, and the cheap repair under time pressure is to weaken the reflection test, which hollows out one of the two mechanisms §5 counts. §2.1 already rejected routing a bounded covered anywhere else, and §3.1 already says the covered row "stands on a partial walk, for the same reason fail does". So the rule is stated once, positively, and asserted — but it is scoped by an explicit column, because two of the six witness rows are not existential at all and the draft's unscoped assertion could not have been satisfied by its own register. WITNESS_CLAIMS carries a kind column, 'existential' | 'maximality'. An existential witness says this run exists; a bound can hide it and can never invent it, so such a row reads relationIsTheMachines and is required NOT to read the bound family — not seenWhole, not decreasingOk, not Publishability.searchComplete — and the reflection test asserts exactly that, scoped to kind === 'existential'. A maximality witness says this cycle has no exit or this run has no successor: an absence wearing a witness's clothes, falsified by a missing edge, which is what a bound and clause (d) both produce. Such a row reads the whole gate, walkIsExact, and its kind cell is what exempts it — the draft instead wrote a bare bound condition into two rows and then asserted, four times over, that no row had one. The --max-configs <depth> case lives in semantics.mc.publishable.test.ts as well as in commit 6's fixture list, so the next author cannot re-add a bound condition to an existential row without a red test.

ridesOn is the second column, and it is what stops a row naming another row's gate. Three witnesses are riders on an absence row rather than independent claims — W2 on A6, W5 on A11, W6 on A13 — and the draft spelled that by writing "A6's gate" into the Required cell, which is neither of the admissible values and is unassertable. ridesOn names the row; the reflection test resolves it and requires the rider's own walkRequires to be no weaker than what its host publishes under.

The per-step disjunction, written once here and referenced by row — and the environment is deliberately NOT in it. A witness may still publish on a walk whose relation is not the machine's, provided no step of the witness was taken across a dwell transition and no step crossed a transition in undeterminedGuards. The first half is tested as afterDuration(step.transition) !== undefined on the step's transition id, never as a match against the recorded label — labelFor (config.ts:617-621) records a completion step as '', so a numeric-attrs.after dwell is a step whose label is empty and a label-based test waves it through, which is the same defect the gate's clause (b) had and must not be re-introduced one row down. That is a per-trace check over the retained edges the trace used, not a walk-level one, and it is what makes W1's two covered rows partition rather than overlap. Its store half is satisfied by construction and stated anyway: an edge in undeterminedGuards was never offered, so no witness can have crossed one — the store cannot invent an existential witness, which is why the store gates the maximality rows and only discloses on the existential ones. When it fails, the witness is re-worded (§3.1, §3.2a, §3.8) or withheld (§3.R, §3.5a, §3.5b) — WITNESS_CLAIMS says which per row, and §2.4(c) or the store sentence prints beside whatever survives.

A step that consumed a trigger is a different case and keeps the bare claim, with §2.4(a) beside it — stated here so the asymmetry is a decision and not an oversight. A trace that fires abort is a run of the system, under an environment that supplies abort; §2.4(a)'s sentence names that environment, and the reader is told what the witness costs. A step under a dwell is not that: the interpreter fires enabled[0] at every advance granularity, so the trace is a run of no environment. A step across an undecided guard is not that either: the model states the edge and the walk never had it, so a witness that crossed one crossed an edge the walk manufactured from a false it should have read as unknown. That is why the environment mechanism gates the increasing absence side (clause (c), where "no escape exists" is falsified by a trigger nobody will send) and discloses on the witness side, while time and the store do both. The register carries the asymmetry as data, so it is checkable rather than argued: WITNESS_CLAIMS' per-step clause names two mechanisms and Exactness.relationIsTheMachines names three.

Why the refutation direction is not free, which the draft asserted and the review broke. §3.5a's warrant for leaving refutations ungated was: any prefix of a p-free run is p-free, so a restricted environment either admits the same refuting run or stalls earlier. That argument is about a withheld trigger — an environment that offers less. A dwell is not that. Under a dwell the interpreter does not stall; it takes a different edge, and that edge may satisfy the property. Measured shape: a machine built with { trigger: 'after(5)' } idle → done declared before { trigger: 'after(60)' } idle → stuck, stuck terminal. The alphabet is ["after(5)","after(60)"], the graph is acyclic, the walk is exhaustive and boundHit is 'none' — seenWhole holds and only relationIsTheMachines fails — and existence (state done) globally finds the walk-only maximal run idle → stuck and prints fail — refuted — finite maximal run of 1 step(s) on which \state done` never holds, verification/refuted, **error, exit 1**, on a design where runStateMachinefiresenabled[0] at every advance (execute.ts:1305-1308) and matchestests the dwell only on thetimeout branch (config.ts:601-604), so stuck` is entered on no run. 5b's lasso has the identical shape: the fair cycle may be composed entirely of dwell edges. Hence W4 and W5, and hence the re-worded transfer argument in §3.5a: it covers withheld triggers and not preempted dwells, and it says nothing at all about the store.

2.4 The four standing sentences

(a) The environment sentence. exploreMachine offers the alphabet wherever it can decide that the interpreter takes its next event — at a configuration where no completion transition is due, and at one where the chase budget is spent with a completion transition still due — and completion alone everywhere else (§2.3 reading 2, §8.5, §8.7). Any witness that consumed a trigger, and any escape from a trap, is a claim under a maximally cooperative environment. Measured: grep -rniE 'cooperative|offers every trigger|every trigger in the alphabet' over src/ scripts/ docs/ returns zero hits outside docs/05. This sentence does not exist in the tool today — it is new prose, written once as a shared constant and printed by 1, 2, 5 and 8 on every verdict line whose alphabet is non-empty:

the environment offered every trigger this machine names wherever the walk could decide that the interpreter takes its next event (no completion transition due, or the chase budget spent), so a witness that consumes \abort` is a claim about that environment and not about one that withholds it`

Dated note, 2026-09-16 (commit 24). The sentence above names abort because this plan's example does. It was shipped as a constant, verbatim, and pinned verbatim by three lanes with the example trigger inside it — measured printing consumes abort about latch.sysml, a machine that names unlatch. Since commit 24 it is environmentSentence(triggers): the same words with the consumed triggers backticked in the caller's order, throwing on none. The plan's example stays the pin for the spelling; §8.4 records the change.

(b) The absence rule. Every A-row above is suppressed, never qualified, when its condition fails. Two measured hazards attach:

• search returns at the first violation (patterns.ts:944-953), so found.configs is "product states seen up to the witness" and the code says so in its own words at :1223-1228. No absence sentence may quote found.configs as a total. Where a row's prose wants the configuration-graph count instead, it quotes a named field — PropertyVerdict gains machineConfigs (§3.1) — because base sets configs: found.configs unconditionally at :1189 and every verdict branch spreads it, so a row that says one number in JSON and another in prose publishes two unlabelled counts for one row.
• A configuration whose successors were all dropped at a bound looks, to Tarjan, exactly like a sink. Under seenWhole — the gate's first half, which every SCC-derived claim reads through walkIsExact — no such claim publishes from such a walk at all; openFrontier keeps the census honest as well. This is not the same fact as c929278's (§0.1): a bound does not withhold a verification/deadlock row, because recordDeadlock's subject is a configuration that was dequeued and offered every input and found nothing enabled, which a bound does not touch. The bound damages the retained relation (an edge into a dropped successor is not recorded), and that is what Tarjan reads. Two objects, two rules, and a §3 row that reasons about one may not quote the other.

(c) The dwell sentence. Printed on every verdict line whose walk has a non-empty timedTransitions — i.e. wherever the gate's clause (b) fails — beside whatever claim survives:

this walk advances no clock: a transition carrying an \after(n)` dwell is offered without waiting out its dwell — as a named event where the dwell is written as a trigger, as a completion where it is written as `attrs.after` — so a step taken across one is a step the interpreter may never take`

The second half of that sentence is the fourth reading of §2.3 made visible to the reader: the draft's wording said "every after(n) label", which is a true sentence about the machines the draft measured and a false one about a machine whose dwells carry no label at all.

It is not a substitute for the gate. Where the claim is increasing the claim is withheld and this sentence says why; where the claim is a positive witness, WITNESS_CLAIMS says per row which of the two happens — the witness is re-worded at §3.1 (covered), §3.2a (a trap's entry path) and §3.8 (a published cut set), and it is withheld at §3.R (the named avoiding cycle or sink — the row the draft left ungated entirely), §3.5a (the refuting finite maximal run) and §3.5b (the lasso). In every case this sentence stands beside whatever survives. The two hazards are different and the disclosure must not be asked to do the suppression's job — which is exactly the error §2.4(a) would have made if it had been left to cover this case, since a dwell is not a trigger an environment can withhold or offer out of order. The store has the third sentence of this family, printed by boundsSentence on every bounds line in every lane (§2.3): store seeded from declared literal values — a guard over an attribute with no declared value is read as false.

(d) The simulator sentence — what the exactness gate does NOT cover, and the reason it must print on every increasing claim. Every increasing claim in this plan is a claim about the MACHINE's semantics and never a claim about what the shipped simulator does. That sentence is the standing one; the rest of this paragraph is why it has to be printed rather than assumed. walkIsExact establishes that the retained relation is the machine's. It establishes nothing at all about what the shipped interpreter does with that machine, and the two differ on every nondeterministic choice point: the walk explores both branches of a declaration-order tie-break and runStateMachine fires enabled[0] (execute.ts:1300-1308). Measured, this is not a corner case — verification/nondeterministic-choice reads 1 on UAVSurveillanceSystem::FlightModes (at …::autonomous, event="", enabled autonomous→manual and autonomous→failsafe, taken →manual, notTaken →failsafe) and 1 on VehicleModel::VehicleStates (at …::idling, event="", enabled idling→moving and idling→off, taken →moving, notTaken →off). On two of the three shipped machines, every increasing claim this plan publishes is therefore a claim about the machine's semantics and not about the simulator's. So, printed once as a shared constant beside every increasing claim and every published witness, whenever nondeterministic > 0 or a nondeterminism row was withheld under c929278's rule (§0.1 — a row is withheld when an undetermined guard sits strictly inside the level where the choice is reported, and a trigger written as "the count is non-zero" would drop the disclosure on exactly the walks that least resemble the simulator):

every claim above is about this MACHINE's semantics — the walk explores both branches of a nondeterministic choice; the simulator takes the first declared one, so a run this verdict quantifies over may be a run \simulate` never produces`

It is deliberately not gated away. Correction 13 already forbids deriving a verdict from the tie-break — that would print a claim about the simulator as a claim about the model — and this sentence is the mirror discipline: the verdict is about the model, and the reader is told so rather than left to assume the two agree. Where §3.R's potential names a cycle and §3.5a's fail names a run, the same sentence prints, because those are the two rows a reader is most likely to try to reproduce with simulate.

2.5 The census rule

mc-scope's standing rule — a feature that cannot report on its own usefulness is not finished — ships as a field in a report, not a note. Every census is --json-only, costs nothing on the text path, and lands inside the existing payload object, never beside it: test/campaign/cli.sysprose.test.ts pins the top-level key lists (['file','ok','reach'], ['connectivity','file','ok']) and a census at the top level breaks them on contact. §5 is the single table of what each census retires.

And a HELD feature owes a census in the same way, but it does not write one: it is retired or released by the census of the commit that gates it. §3.4b reads commit 12's, §3.7b reads commit 14's, §3.5a reads commit 3's acyclic, §3.6 reads commit 19's pair count — which is why those four subsections carry a Release condition where a shipped feature carries a Census, and why each of those release conditions names the field and the number it is read against rather than a judgement. §3.8 was the exception and it was an oversight: it is HELD behind commit 21's census and ships a permanent vocabulary commitment, so it now carries both, and §5's table has the row for commit 23 that the draft never wrote.

2.6 Reserved words, and what the guard does not catch

Measured in test/unit/claims.test.ts: RESERVED_FORMS[1] bans deadlock-free and realizable as bare words with no allowance at all. Consequence for 5b: Baier & Katoen's fair-continuation condition may never be called by its book name; it is written here as the fair-continuation condition, and its verdict says "the declared assumption has a fair continuation from every reachable configuration".

And the guard is narrower than three of the input analyses assumed. SUBJECT (:303) is sysprose|(the|this|that|these|those|our) (tools|models|properties|requirements|obligations|proofs|clauses|verdicts|results|architectures|systems). It does not contain machine, design, state, run or cut set, and no form mentions guaranteed, covered, recoverable, no cut set or no simulation relation. So:

• "the machine is safe to enter failsafe" would pass the guard today.
• guaranteed and every run is guaranteed to … pass it today.

And the guard, as it is written, CANNOT RESERVE A NEGATIVE PHRASE AT ALL. This is the third of the three findings that gate the build, and it was confirmed by running the guard's own scanner. scanDocs calls negated(before, m[0]) at claims.test.ts:157, and negated (:100-102) returns true when NEGATION.test(matched) — NEGATION (:93) being /\b(not|never|no|non|without|isn't|aren't|nor|neither)\b/i. Any form whose matched span contains no, not or never is defused unconditionally, before the allowance window is even consulted. Executed on planted sentences:

"This design has no cut set."                    -> 0 hits   (defused)
"The design is not covered."                     -> 0 hits   (defused)
"There is no simulation relation between them."  -> 0 hits   (defused)
"The machine is recoverable."                    -> 1 hit
"The machine is guaranteed."                     -> 1 hit

So two of the four forms the draft promised, and the negative half of a third, are dead on arrival — and the claims they would have covered are exactly the ABSENCE claims (no cut set, no simulation relation, not covered) that hard constraint 1 and §1 name as the single way this lane starts lying. Worse than a gap: the draft's own it('… asserted to fire') test would either go red on landing or be quietly rewritten to pass on a positive stand-in, and then §5(c) counts a guard that covers nothing as one of two mechanisms.

Commit 4 therefore changes negated() itself, and that is the point of the commit. RESERVED_FORMS' entry shape (claims.test.ts:328, {what, pattern, allow}) gains a fourth optional field, negativeIsTheClaim?: true; the call site at :157 passes the form and skips the in-span half of the defusal for those entries, keeping the look-back half (NEGATION in before) for every form, so "we do not claim there is no cut set" is still defused by the words in front of it.

And then the tree was measured with that change in place, before any form was written — which is what decided the forms' shape, and which contradicts the draft's own promise. The draft said each new form is "measured at 0 pre-existing hits over the tree first". Executed against the real tree — 698 scanned files, the shipped SKIP_FILES applied, the look-back defusal kept and only the in-span half skipped — the bare phrases are not at 0:

bare  no cut set              -> 23 hits
bare  not covered             ->  3 hits
bare  recoverable             ->  2 hits
bare  no simulation relation  ->  0 hits

Nine of the 23 are in src/semantics/fault-tree.ts, and two of those are the command's own shipped verdict strings — :859 `${input.events} basic event(s); no cut set was found ${input.bound} and ` and :861 `… no cut set ${input.bound} — ${ORDERS_NOT_EXPLORED_NOTE}` — i.e. the honest, bounded absence A14 that this plan's register keeps. The rest are prose about the sentence (sysprose-spec.ts:45/:215, sysprose.ts:2444/:2446, refinement.ts:2619/:2660, USER-GUIDE.md:1411, cli-reference.test.ts:419, verification.test.ts:3641/:3931/:3933/:3960) and innocent uses elsewhere (CONFORMANCE.md:11 "states, candidly, what is and is not covered", metaclasses.ts:258, AGENT-AUTHORING-CAMPAIGN.md:2511, analytics.ts:896 and metamodel.ts:15's "recoverable from"). A bare-phrase form lands red on arrival with 28 violations, and the only allowance that clears :859/:861 is one matching no cut set (was found|up to order) — which defuses precisely the sentence the form was added to reserve. Reserving the bare phrase fails in one direction or the other, and there is no third setting.

So commit 4 scopes the new forms rather than landing a triage list, and the scoped forms are measured at 0. That is the choice, and it is the one the guard's own design already makes — RESERVED_FORMS reserves sentence forms, not words, and every form that ships today is subject-scoped for exactly this reason. Re-measured with negativeIsTheClaim in place, over the same 698 files:

Each row was executed both ways in this session: 0 hits over the tree, and the planted sentence asserted to fire. Widening SUBJECT with machines?|designs?|state machines?|runs? costs 0 additional hits on the three subject-scoped forms that ship today — verified/correct/safe 0 → 0, proved 0 → 0, consistent 0 → 0 — so the widening is free and is measured to be, exactly as the GAP widening was.

What this buys, stated exactly, so §5(c) is not overclaimed. The guard now reserves the sentence a reader would quote for all five pieces of new vocabulary — that is the prose half, and it is real: "the machine is recoverable", "this design has no cut set" and "the design is not covered" each go red on landing after commit 4. It does not reserve the verdict strings themselves, which carry no subject (not covered under {…}, no cut set up to order 2) and are pinned byte-identically by mechanism (b) instead. That division is the honest one and it is written into §5(c) rather than left to be discovered: no claim in this plan is covered by fewer than two mechanisms, and for these five the two are the register (a) and the fixture (b), with the sentence guard (c) covering the prose.

Commit 4 adds these five forms before any feature that could print them. A form that is planted and does not fire is a red test in commit 4, not a review comment in commit 23. This plan does not lean on a guard that would not fire, and it does not claim a measurement it did not take.

3. Tools and features

3.P — Retain the successor relation exploreMachine already computes

What it decides. Nothing. It is an engine change with no report, no diagnostic and no verdict, and that is why it is its own commit: its gate is "reach's output did not move", and that gate proves something only when nothing else moved with it.

Command and flags. None.

Engine. In-process TypeScript. Zero new compute — every edge is already produced by stepConfig at explore.ts:509 and discarded at :512.

The change, ~12 lines inside exploreMachine. Every row below names the construct it edits; the positions are found by reading exploreMachine top to bottom, and the order of the rows is the order they appear in it.

ExploreResult — thirteen fields at dc6662c — gains six readonly fields. Clause (d)'s producer is not among them: undeterminedGuards is already there, and a seventh field duplicating it is what the fifth review found and what this list no longer asks for.

  /** Successor indices, in BFS discovery order. No edge points at a
   *  configuration a bound refused — that configuration is not a node. */
  successors: readonly (readonly number[])[];
  /** The ACTIVE STACK per index — not the leaf. One state spans many
   *  configurations and a composite sits on the stack of every configuration
   *  inside it, so `stack.includes(p)` is the correct target predicate for a
   *  `state` atom, for recovery and for simulation labelling. */
  configStates: readonly (readonly ElementId[])[];
  /** The ACTIVE LEAF per index — `leafOf(config)`, `null` where there is none.
   *  One integer array beside `configStates`, and it is NOT redundant with it:
   *  `atomHolds` reads a `state` atom as `obs.config.stack.includes(...)` and a
   *  `node` atom as `leafOf(obs.config) === ...` (`atoms.ts`:341-345), and
   *  `nodesOf` (:137-151) admits every StateUsage in the machine, composites
   *  included, so the two readings DIVERGE on any composite state. Retaining
   *  both is what lets §3.2b and §3.R read `p` through `atomHolds`'s own
   *  selection instead of a hand-written predicate that silently picks one. */
  configLeaves: readonly (ElementId | null)[];
  /** This walk did not see the graph whole. Equals `!exhaustive`, asserted —
   *  NOT `boundHit !== 'none'`, which reads `false` on the unsupported-construct
   *  early return at :440-455 (`configs: 0, exhaustive: false, boundHit: 'none'`)
   *  and would let the acyclicity CENSUS publish `acyclic: true` over an empty
   *  relation on the one machine class this engine refuses to walk. */
  openFrontier: boolean;
  /** Every walkable transition of this machine for which `afterDuration` is
   *  defined — a numeric `attrs.after` OR an `after(n)` trigger string, and
   *  NOT only the ones that reached the alphabet. Empty is the exactness
   *  gate's clause (b). Non-empty means every escape, every recovery and
   *  every witness in this walk may be an artefact of a dwell the interpreter
   *  never grants (§2.3, mechanism 1). Measured: a transition carrying only
   *  `attrs.after` is a COMPLETION transition to `isCompletion` and
   *  contributes nothing to the alphabet, so the draft's alphabet-scoped
   *  version of this field read empty on a machine all of whose edges are
   *  dwells. */
  timedTransitions: ReadonlySet<ElementId>;
  /** The alphabet members those transitions contributed. Gates NOTHING. Its
   *  only reader is the `alphabet ∖ timedLabels` subtraction that decides
   *  whether a non-empty alphabet is real triggers (`failedClause` reads
   *  'environment') or all dwells ('time') — §3.R rows 5-6, §3.5a rows 2-3. */
  timedLabels: ReadonlySet<string>;

  //  NOT ADDED — clause (d)'s producer already exists on this interface:
  //    undeterminedGuards: readonly UndeterminedGuardRow[];
  //  shipped at c929278, populated by `stepCandidates`, and already read by
  //  `reachOne` as the fifth publishability conjunct. The gate reads
  //  `walk.undeterminedGuards.length === 0`. Do not add a narrower ElementId
  //  set beside it: the shipped predicate is "consulted and decided nothing",
  //  which is WIDER than "no declared value" and catches `not mode` over a
  //  fully valued `mode` — the machine on which the narrow reading publishes
  //  a trap over a missing edge with the gate green.
  //
  //  NOT ADDED, for the same reason:
  //    census: EdgeCensus;
  //  shipped at a66ba1f. §2.3 reads it; nothing here produces it.

Clause (c) needs no new field: it reads bounds.alphabet, which is already computed, already published on every bounds line, and already [] on every machine in this tree (§5(d)).

The census field acyclic (commit 3) is three-valued — true | false | null — and reads null whenever walkIsExact is false, which subsumes openFrontier and adds the three clauses that matter here: an undecided guard is a cycle-closing edge the walk never had, so a walk that is exhaustive and inexact can report acyclic: true about a machine whose stated relation has a cycle (§2.3, measured). Lane G's release condition counts only acyclic === true on a walk where walkIsExact holds.

Never export a Map keyed on the configuration hash. hashConfig (config.ts:677-696) builds regionId|stack|dwell|store|history from element ids, ids are fresh per load (docs/04 D3), and the FlightModes hash is 114 characters of them. Intern to integers in BFS discovery order, which depends only on model structure because hashConfig sorts store and history by name. No hash string may reach a report, a digest or a JSON payload.

The one line that decides whether this feature lies. Recording at the admission point (:537) instead of at the prune (:512) yields the BFS spanning tree — nodes − 1 edges, acyclic by construction on every machine in this repository — and Tarjan over it names {failsafe} a bottom SCC on examples/uav-isr.sysml. The two pruned edges on FlightModes are precisely the cycle-closing ones (autonomous → manual, failsafe → standby). This is the exact failure direction docs/04 §6 forbids, and it is one line away.

Verdict vocabulary. None.

MUST NEVER. Emit anything. The moment this commit adds one diagnostic, test/campaign/cli.sysprose.test.ts:3175-3177 — expect(body.reach.diagnostics.map(d => d.code)).toEqual(['verification/nondeterministic-choice']), an exact array — moves, and the differential that is the whole point of the commit stops proving anything. That assertion is the intended trip-wire, not a nuisance.

Exit-code contract. Unchanged everywhere.

Tests.

• NEW test/unit/semantics.mc.successors.test.ts: on FlightModes, successors is the 5-edge relation over 4 nodes — standby→manual, manual→autonomous, autonomous→manual, autonomous→failsafe, failsafe→standby; on examples/vehicle.sysml 3 nodes / 4 edges; on views-tour 2 / 2.
• The named negative test: a fixture asserting that recording at the admission point yields 4 nodes / 3 edges, so the regression has a name in the suite rather than a comment.
• --max-configs 2 on uav-isr: successors.flat().every(i => i < configs), and openFrontier === true.
• The unsupported-construct fixture, which is the second named negative test. A .sysml file with a transition whose endpoint does not resolve — reproduced: reach dangle.sysml prints 0 configuration(s) explored … not explored — transition-without-endpoints — asserts configs: 0, exhaustive: false, boundHit: 'none' and openFrontier === true. The assertion is openFrontier === !walk.exhaustive; writing it as openFrontier === (boundHit !== 'none') would pin the bug, so the wrong spelling is named here for the reviewer.
• timedTransitions holds both dwell transitions on the two-dwell fixture and timedLabels is {"after(5)","after(10)"} — built through ModelFactory in this test file, because accept after(n) does not parse (correction 22) — and both are empty on every machine in the tree (§5(d)), so clause (b) holds everywhere the notation reaches today and costs nothing on any model a CLI command can load.
• The numeric-attrs.after fixture, which is the test the draft's clause (b) could not have passed. A machine whose only timed transitions carry attrs.after and no trigger — written m.create('TransitionUsage', {attrs:{after: n}}), since ModelFactory.transition drops the field (factory.ts:98-113) — asserts afterDuration defined and isCompletion true on each, bounds.alphabet === [], timedLabels empty, timedTransitions non-empty, and walkIsExact === false with failedClause === 'time'. The wrong answers are named: walkIsExact === true, and downstream of it §3.2b's recoverable at exit 0 and §3.2a's no component of this walk is inescapable beyond its endings on a machine whose {failsafe, failsafeHold} is absorbing under enabled[0].
• undeterminedGuards, from both sides, and unlike the dwell fixture this one is a .sysml file. The trapguard model — attribute resetOk : Boolean; with transition nominal then degradedA; transition degradedA then degradedB; transition degradedB then degradedA; transition degradedA if resetOk then nominal; — loads clean and, re-measured at dc6662c, walks 3 configuration(s) explored, depth 2 — undetermined under {…} — 1 guard(s) the walk could not evaluate, 3 of 4 transition(s) fired, dead withheld, rc=0. walk.undeterminedGuards already holds exactly the if resetOk transition on it — that is c929278's field and this plan asserts it rather than building it. Both literal variants assert it empty: = true with the escape edge present, = false with the escape edge absent-but-decided (3 of 4 transition(s) fired, 1 dead, dead degradedA -> nominal, exhaustive under {…}). The trio is what shows the field tracks decidedness and not the presence of a guard, and it is the only fixture set in this plan that separates clause (d) from a narrower "no declared value" reading — for which the fourth member is attribute mode : Integer = 3; with transition degradedA if not mode then nominal, measured "undeterminedGuards": [{ … "guard": "not mode", "unresolved": [] }]: a fully valued feature, an empty unresolved, and the guard undetermined all the same. Measured baseline: undeterminedGuards is empty on every machine in the tree, because not one transition in this repository carries a guard at all (grep -c ' if ' is 0 in every one of the six source files) — which is exactly why this fixture is the only coverage clause (d) will ever have. And the acyclic census is asserted on the same file's two-state sibling, because that is where the artefact shows: transition nominal then degraded; transition degraded if resetOk then nominal; walks 2 configuration(s) explored, depth 1 — exhaustive, 1 of 2 transition(s) fired, 1 dead, and asserts acyclic: null with acyclic: true named as the wrong answer; the = true variant asserts acyclic: false, because the escape edge closes the cycle the walk could not see. That pair is what stops lane G's release gate being flipped green by a machine that is acyclic only because a guard was unbound.
• The alphabet baseline, asserted rather than assumed: bounds.alphabet is [] on all eleven machines in the tree (grep -c accept is 0 in every source file), so clause (c) is satisfied everywhere today; the latch model — state nominal; state locked; transition nominal then locked; transition locked accept unlatch then nominal;, also a clean-loading .sysml file, measured alphabet unlatch — asserts a non-empty alphabet and is the fixture every clause-(c) refusal in §3 is written against.
• The parse fact itself is a test, so it cannot rot back in as an assumption: a .sysml source carrying transition idle accept after(5) then done; is asserted to fail the parse with the no-viable-alt at the (, and the escaped spelling accept 'after(5)' is asserted to yield attrs.trigger === "'after(5)'" with afterDuration returning undefined. If a future grammar change makes after(n) writable, this is the assertion that goes red and tells the next author to re-price the time clause's census.
• configStates[i] is the full stack and configLeaves[i] is the leaf, asserted on the composite-state fixture where the two differ: state nominal; state degraded { state sub1; state sub2; transition sub1 -> sub2; } transition nominal -> degraded;. The same fixture pins the two readings apart at the atom level, because that is where a hand-written predicate goes wrong — measured on the same walk, one atom spelled two ways: --pattern "pattern=absence, scope=globally, p=node degraded" → PASS, `node degraded` never holds, over the whole run; p=state degraded → FAIL with a 1-step witness. The test asserts configStates explains the second and configLeaves explains the first, and that both agree with atomHolds (atoms.ts:341-345) on every configuration of the walk.
• The differential: reachReport(model) is deep-equal before and after on all six examples, by structural comparison in the same file. test/unit/semantics.mc.reach.test.ts (26 tests) and the campaign reach block are re-run untouched; any movement is a defect, not a re-record.

Cost. Compute zero; memory one integer pair per innermost-level stepConfig call — measured 5 on uav-isr, 4 on vehicle, 2 on views-tour. Code ~12 lines plus six ExploreResult fields, of which one (configLeaves) is the third review's addition and a plain integer array, and one (timedTransitions) is the fourth's. The seventh field earlier revisions listed here — a re-derived undetermined-guard set — is not built: c929278 shipped it. reachReport on uav-isr is 3.0 ms warm today and gains one array push per existing call.

Census. successors.length, openFrontier, timedTransitions.size, timedLabels.size, alphabet.length, walk.undeterminedGuards.length and walk.census.counts — the last two already produced, recorded here rather than computed — plus the existing boundHit, per machine, which makes commit 3's acyclicity census, lane C's trap census and — new here — the exactness census free. The last is the number §5's table reads: how many machines in a corpus walkIsExact would publish about at all. Measured on this tree it is 5 of 6 (the sixth is the unsupported-construct fixture, already suppressed), and the three clauses that could ever refuse are at 0 across the board: 0 dwell transitions, 0 named triggers, 0 guards. timedTransitions.size is priced honestly, not as the draft priced it. The draft offered it as "how many machines in a user's corpus this plan can make an increasing-polarity claim about", which correction 22 makes impossible: on every model any CLI command can load it is 0 by construction, because no .sysml file can carry a timed transition. What it actually measures is API traffic — machines built through ModelFactory or carrying attrs.after, which is where the SDK's own callers live. So the census is recorded per machine and read as an SDK-population number, and the retirement question it answers is "does anything but our own test suite build a timed machine?" — not "is the time clause a wall for users?", whose answer is already known and is no.

3.1 cover — an existential reachability property with a witness

What it decides. Can this design ever get into the situation I care about — and did my safety property pass because the machine cannot get anywhere interesting? Manna–Pnueli's Guarantee class (◇β): not finitely refutable, which is why the bad-prefix engine correctly refuses existence; finitely witnessable, which is why the same engine can confirm it.

Why it is a gap and not a rename, measured on both polarities. A probe machine that can reach failsafe and one that cannot, against the only expressible spelling of the intent:

• --pattern "pattern=absence, scope=globally, p=state failsafe" on the reachable machine → rc=1, 1 fail, verification/refuted, error severity. The design that satisfies the intent is red.
• The same pattern on the sealed machine → rc=0, 1 pass. The design that violates the intent is green.
• pattern=existence on the reachable machine → rc=2, verification/behaviour-unsupported-construct, "there is no flag that lowers it".

Command and flags.

npm run sysprose -- check-behaviour <file> --element REF \
    [--pattern "pattern=cover, scope=globally, p=state failsafe"] [--cover-required]

--cover-required is a flag, never a subcommand: COMMANDS.length stays 22, so test/unit/readme.test.ts:307 (APP_DOORS.length === COMMANDS.length + 1), the README capability table and the two docs-counts subcommand claims all stay still. The carrier form needs no new metaclass — resolveProperty reads pattern.fields ++ scope.fields generically at patterns.ts:539-551 and the five atoms need no work: @SysproseVerification::PropertyPattern { attribute pattern = "cover"; attribute scope = "globally"; attribute p = "state failsafe"; }

But the VALUE is a forward-compatibility commitment, and it is priced here rather than left unsaid. The carrier shape is unchanged; the string "cover" is persisted in a user's .sysml file. Any build before commit 6 reads it through the same generic cell reader (patterns.ts:460-475) and then refuses it in resolveProperty as verification/malformed-property (:499-502), which the docstring at :505-509 says makes the property inconclusive — reproduced today: rc=2 on a model that is green on the new build. That is the same direction and the same permanence as an added evidence-record field, so hard constraint 6's reasoning applies to a persisted enum value as much as to a metadata def. It is recorded in docs/CONFORMANCE.md beside the two metadata def commitments, in the commit that spends it. The alternative — making cover a --pattern-only feature with no carrier value — is rejected explicitly: it would make the one pattern class an author cannot write into the model the one class the model cannot be re-checked on, and PropertyPattern exists so a property travels with the file. §3.2b's "recovery" carries the identical row.

Engine. In-process TypeScript, no solver, and no dependency on P (correction 2). search is unchanged. The monitor breach for cover is byte-for-byte absence's (breach = v.p === true), so monitorStep (:688-794) gains one case falling to the same body; all the work is in checkProperty's verdict tail (:1200-1299), re-reading the same result.

Catalogue placement, and the one ordering rule. PatternClass gains 'guarantee'; the PATTERNS entry inserts before existence, because test/unit/cli-reference.test.ts asserts PATTERNS.filter(p => p.kind === 'liveness').map(p => p.name) equals PATTERN_NAMES.slice(-2) with the message "the liveness pair moved" — appending breaks it by construction, and inserting before existence keeps it green with no edit, which is the point. PATTERN_NAMES (sysprose-spec.ts) is a hand-copy kept free of model imports and is compared for order in the same file; that comparison does move, in this commit.

Verdict vocabulary it MAY print, with the precise condition for each.

Sentences it MUST NEVER print, and why.

• "reachable", unqualified, when the witness consumed a trigger. The walk's environment offers every letter wherever the walk can decide that the interpreter takes its next event; the word without §2.4(a) beside it claims something about the real environment. Measured on the probe: the witness consumes abort, and the bounds line says alphabet abort while nothing says where every letter is offered.

• "not covered" on a non-exhaustive walk — A5, suppressed exactly as reach's unreachable list is at explore.ts:792.

• "not covered over N product states" where N is found.configs — the search short-circuits and :1228 says in the tool's own words that the number was never a total. And the JSON must not disagree with the prose: base (:1189) sets configs: found.configs unconditionally and every branch spreads it, so this commit adds machineConfigs to PropertyVerdict, the sentence names that field, and a test asserts the two numbers are both present, both labelled, and equal only where they should be.

• covered — … a run this semantics admits on a walk whose timedTransitions is non-empty and whose witness crossed one of them. This is the first affirmative claim this lane has ever published, and the engine's soundness note (explore.ts:29-31, "an over-approximation can only shrink the absence claims, never invent one") was written when the lane had no positive claims at all. Measured, on a ModelFactory machine with {trigger:'after(5)'} idle → A declared before {trigger:'after(10)'} idle → B (there is no .sysml spelling — correction 22): the interpreter fires enabled[0] at every advance granularity, so B is entered by no run; the walk offers "after(10)" as a named event with no dwell test and finds a one-step witness. reach reporting B reachable is the safe direction — it only shrinks the unreachable list — while cover republishes the identical over-approximation as an affirmative finding with a witness, flipping the direction. The re-worded sentence above is what prints instead; the bare one is banned. The two rows are exhaustive and mutually exclusive, and the draft's were not: the draft required the time condition on row 1 and its negation plus an after-label step on row 2, leaving a real shape — a walk with timedLabels non-empty whose witness fired no after-label — matched by neither row, with the implementer free to pick either sentence and no test able to go red. Row 1's condition is therefore the disjunction, over all three mechanisms rather than only time, and WITNESS_CLAIMS row W1 is what makes the choice machine-checked instead of a coin toss. Measured shape: {trigger: 'abort'} idle → target and {trigger: 'after(5)'} target → sink; cover (state target) has timedLabels = {"after(5)"} and a one-step witness that fired abort — row 1, and the bare wording, correctly.

• Exit 1 under --cover-required when every unreached state of the cover sits behind a guard that evaluated undefined. Correction 23: seedStore (config.ts:231-243) fills the store from declared literal values only, so attribute mode : Integer; with no value is absent, evalStr yields undefined, guardHoldsStore (:70-77) returns false and the edge is never offered. Before c929278 that happened on a walk where every publishability condition held; after c929278 (§0.1) it is Publishability.guardsDetermined that fails and verification/guard-undetermined that prints, and this flag's refusal is the cover-shaped answer to the same shape rather than a substitute for it. The draft's warrant here — "the walk and the interpreter agree on the decreasing side, which is why no publishability condition can see it" — is withdrawn: it is true of not covered, whose polarity a missing edge does not flip, and false of verification/deadlock, which a missing edge invents (register A0, §2.3). (undeterminedGuards is non-empty on this walk, so the increasing side is already refused by the gate's clause (d); the flag's refusal below is the decreasing side's answer to the same shape, and the two are not interchangeable.) Reproduced this session: part def Ctrl { attribute mode : Integer; state def Modes { state idle; state hazard; transition idle if mode == 3 then hazard; } } walks 1 configuration(s) … exhaustive under {…} and raises verification/unreachable-state, verification/dead-transition and verification/deadlock. not covered is still the honest answer there — the design as written admits no run into hazard — but it is an answer about an unbound model parameter, not about a violated requirement, so the store clause prints on the line and the flag does not spend the 1. The refusal sentence: --cover-required not applied: every unreached state of this cover sits behind a guard over an attribute with no declared value, so the walk read it as false — exit 2, not 1.

• claim: 'fail' + verification/refuted on a not-covered row. cover reuses absence's identical monitor breach, so falling into that branch (:1229-1234) exits 1 for a correct design — the exact defect this feature exists to fix, reproduced by the fix.

• "verified" / "safe", and "the design can enter failsafe" as a bare sentence — it drops the bound and the environment, and (measured, §2.6) today's guard would not catch it, which is why commit 4 widens the guard first.

• Exit 1 by default. A missing behaviour is not a violated requirement.

Exit-code contract. behaviour. covered counts toward the 0 row — and the 0 row's own sentence moves in this commit to say so (§2.1): it names the two discharge shapes separately, an assertion shown to hold on every reachable configuration over a graph seen whole, and a cover witnessed on a run this walk saw. Without that edit the command publishes, in its own --help and in the generated docs/CLI-REFERENCE.md, a 0 that means something the run did not establish — on every covered row, exhaustive or not. not-covered ⇒ 2, or 1 under --cover-required — except on correction 23's shape, where the flag refuses to spend the 1 and says so (the MUST-NEVER above): a cover whose unreached states all sit behind a guard over an attribute with no declared value is an answer about an unbound model parameter, not about a design that violates something. The flag is recorded on the summary line and in the --json payload, and nowhere else. The draft said "recorded in the evidence record's flags"; measured, check-behaviour writes no evidence record and has no way to — its flags are exactly element · pattern · max-configs · strict-vacuity (sysprose-spec.ts:878-907), --record is declared on verify alone (:616), and EvidenceRecord.flags (api/evidence.ts:613) is only ever filled on that path. Adding one would mean a new record kind through evidence-record.schema.json's additionalProperties: false, i.e. exactly the one-directional schema commitment §3.3a says this plan does not spend outside commit 11. If a durable record of a flag-raised exit is wanted, it is §7 decision 11, priced the way commit 11's is — not a clause here. BEHAVIOUR_EXIT_CODES (:201) gains the 0-row rewrite and the 2-row clause, both quoted in §2.1, and both asserted in cli-reference.test.ts's per-contract block at :206-214.

Tests.

• A fixture pair (cover-reachable, cover-sealed): cover is covered with a 2-step witness on the first and not-covered / exit 2 on the second, with the inverse absence verdicts asserted in the same test — that pair is the polarity regression.
• --cover-required turns the second into exit 1 with the second code, turns nothing else red, and leaves both claim words byte-identical.
• The bound frontier, asserted from BOTH sides, because the draft's version of this test would have failed on landing. A witness at depth d needs --max-configs ≥ d: the violation check runs on a freshly-stepped successor (patterns.ts:944-953) but that successor is only enqueued past the config bound at :969, and seen starts holding the root. Measured on the shipped example — check-behaviour examples/uav-isr.sysml --element FlightModes --pattern "pattern=absence, scope=globally, p=state failsafe", a 3-step witness — gives rc=2 inconclusive / verification/bound-exhausted at --max-configs 1 and 2, and rc=1 fail only from --max-configs 3. cover reuses absence's identical breach, so the draft's "--max-configs 1: covered still stands" was false for the 2-step probe. The test asserts the frontier instead of assuming it: --max-configs <depth> keeps covered, --max-configs <depth − 1> gives inconclusive. The sealed machine is inconclusive at any bound below exhaustion, not not-covered.
• The two-dwell fixture (§2.3), built through ModelFactory inside the test file and exercised through checkProperty in-process, never through argv — accept after(n) is a parse error (correction 22), so there is no .sysml spelling of it and a CLI-level assertion here is unwritable. cover (state B) where the shorter dwell preempts prints the walk-admits wording and never a bare covered, and timedTransitions is asserted non-empty in the same test.
• The row-1 disjunction, which the draft could not have tested: the {trigger:'abort'} idle → target, {trigger:'after(5)'} target → sink machine — timedLabels non-empty, witness fired no after-label — asserts the bare covered wording with §2.4(a) beside it, because the witness consumed abort; the walk-admits wording is named as the wrong answer. Together with the previous bullet the two rows are shown to partition, which is what W1 asserts by reflection.
• The witness row does not read the bound, asserted from the register rather than only from the fixture. In semantics.mc.publishable.test.ts, every row of WITNESS_CLAIMS whose kind is 'existential' is asserted to read relationIsTheMachines and not to name any member of the bound family (seenWhole, decreasingOk, Publishability.searchComplete) in either column, and the --max-configs <depth> case is repeated there: the measured partial under {maxConfigs 3, …} walk still publishes covered. Without this assertion the reflection test and commit 6's bound-frontier test are mutually unsatisfiable and the cheap repair is to weaken the reflection test (§2.3).
• The undecided-guard witness, which is the store's half of the same partition and is an ordinary .sysml file rather than a factory machine: a cover whose witness crosses transition idle if mode == 3 then hazard; with attribute mode : Integer; undeclared cannot arise (the edge is never offered), so the fixture is its mirror — attribute mode : Integer = 3; gives a bare covered, and dropping the = 3 gives not covered with the store named on the bounds line and undeterminedGuards non-empty. The pair pins that clause (d) tracks the declared literal and not the guard.
• The unset-guard fixture (correction 23): attribute mode : Integer; with transition idle if mode == 3 then hazard; ⇒ not covered whose bounds line names the seeded store, exit 2, and — under --cover-required — still exit 2 with the refusal sentence, never exit 1. The census field coverUnreachedBehindUndefinedGuard is asserted non-zero on it and zero on the sealed probe, so the two shapes are told apart by a number and not by a reviewer.
• Cover over a fires T atom, over an expression atom, and under a between scope — the three shapes reach structurally cannot answer, which are this feature's whole justification. (cover accepts all five atom kinds; recovery does not, and §3.2b says why.)
• The counts-sum guard (§2.2) across every behaviour fixture.
• cli-reference.test.ts's PATTERN_NAMES-order assertion re-recorded, and its liveness-pair guard asserted UNCHANGED — green with no edit, because cover inserts before existence and [existence, response] stays the last two.
• The carrier round-trips idempotently from the second save.

One semantic decision, written down before the first fixture is recorded. absence's before/between scopes only establish a breach once the segment closes (needsClosing, :782-793), so a cover witness under those scopes extends to the closing R. Defensible, but a decision and not a re-label: it goes in docs/CONFORMANCE.md §8.5 with the pattern table.

Cost. One PatternClass member, one PATTERNS entry, one monitorStep case, ~60 lines of verdict tail, two claim words, two codes, one flag. The real cost is documentation: CONFORMANCE.md:865-883 ("Four patterns … are safety", "Two … are liveness", "the verdict vocabulary is four words" — all three move), USER-GUIDE.md:1744-1751 (the pattern table with its Decided here? column), DIAGNOSTIC-CODES.md, AGENT-AUTHORING-CAMPAIGN.md:3556/:3608, docs/04:337/:590, and the sentence at scripts/sysprose.ts:3235 that appears in every transcript.

Census. check-behaviour --json records {atomKind, scope, coverUnreachedBehindUndefinedGuard} per cover row — the third being correction 23's exposure, counted rather than argued about: the number of states this cover did not reach whose only inbound guard read undefined against the seeded store. The kill measurement: if ≥80 % are state X × globally, reach already answers them and cover should be retired in favour of printing the witness path in reach. Sharpened by measurement: that shape is answered today — in the negative direction only, as a warning that changes no exit code, with no witness for the positive direction — and nothing in reach's JSON reports an expression atom, a fires T or a scoped question. The escape hatch is real and the census is what decides it.

3.R — The guaranteed / potential modality on an existing fail

What it decides. Whether the violation the tool just printed happens on some run or on every run. It annotates; it replaces nothing.

Command and flags. None. PropertyVerdict (:286-314) gains one field and the text row gains one clause.

Engine. In-process TypeScript over P's relation. walk is already in lexical scope at checkProperty's fail block — it is the same const walk = exploreMachine(…) the function opens with — so after P the machine graph with edges is in hand at the fail site at zero extra cost.

Scope, restricted three times, all three restrictions measured.

1. Memoryless monitors only — absence / universality × globally — where the product collapses onto the configuration graph. search short-circuits at :944-953, so the product graph does not exist at the fail site; a stateful monitor (precedence, bounded-existence, every non-globally scope) needs a second, non-short-circuiting pass and is refused with that reason.

2. BOTH modality values require an empty alphabet, and the draft restricted only one of them. Measured on nominal --latch--> locked, locked --latch--> locked: the naive computation calls absence(locked) guaranteed, because under the maximally cooperative environment every configuration has a successor. In the real system where latch never arrives, the machine sits in nominal forever. Restricting to completion-only machines is the only honest option before 5b lands a fairness carrier; the alternative — admitting "the environment stops offering" as a maximal run — degenerates the modality to potential on every triggered machine. potential needs the same gate, for the mirror-image reason, and the draft left it ungated. Its sentence names a specific avoiding cycle computed over the retained relation, and that relation over-approximates time: on a machine built with {trigger:'after(5)'} nominal → hazard declared before {trigger:'after(60)'} nominal → hold plus {trigger:'after(1)'} hold → nominal, absence (state hazard) globally correctly fails, the violating set is {hazard}, G₀ holds the cycle nominal → hold → nominal built entirely from dwell edges the walk offers as named events — and the tool would print potential — some run avoids it: the cycle nominal → hold → nominal never enters \hazard`about a machine on whichenabled[0]sends **every** run intohazardand the named cycle exists on no run at all. That is this section's own MUST-NEVER — a claim about the simulator's tie-break, published as a claim about the model — reached from the other side. **The draft closed both hazards with one clause, on the containmenttimedLabels ⊆ alphabet; that containment is deleted (§2.3) and the two clauses are independent**, so the modality field is not decidedwhenever the alphabet is non-empty **or a transition of this machine is a dwell** — for either value — and §2.4(c)'s dwell sentence prints beside the refusal rather than beside a claim. On the measured machine above both clauses fail; on a machine whose dwells carry a numericattrs.afterand no trigger only the time clause does, and that is the machine the alphabet-only version of this rule publishedpotentialabout. It is registered asWITNESS_CLAIMS**W3** so §5(a)'s reflection test sees it. **And the third review added a third hazard to the same gate**: on the trapguard machine (§2.3, mechanism 3 — a clean-loading.sysmlfile, unlike the dwell fixtures) the escape edgedegradedA → nominalis guarded by an attribute with no declared value, so the walk never offered it, *G₀* holds the cycledegradedA → degradedB → degradedA, and the tool would print potential — some run avoids itabout a machine whose model states the escape. That is neither a time nor an environment hazard and neither of the draft's two rows caught it, which is precisely why this section now reads one gate —walkIsExact` — rather than its own conjunction. Row 7 is its sentence.

3. Configuration-valued atoms only, and that means state and node — not expression. The restriction the draft stated over patterns and scopes is not enough, because the violation set is a predicate over CONFIGURATIONS and three of the five atoms are not configuration predicates readable from what §3.P retains. fires T and trigger t are properties of a step (atoms.ts:93-99, and patterns.ts's monitor reads the fired label). And expression needs the store: atomHolds evaluates evalStr(atom.argument, obs.config.store, scope) (atoms.ts:350-353), while the only per-configuration data §3.P retains is configStates, the stack of state ElementIds. The draft accepted expression here and refused it in §3.2b, and the two sections stated opposite gates — §6.1 and §7 decision 12 both already say expression "needs the store", so §3.R was the outlier and it is the one that moves. Measured consequence if left open, and it is the identical failure to the fires one: --pattern "pattern=absence, scope=globally, p=(mode == 3)" partitions the configurations with no store, so no configuration is marked violating, G is the whole graph, which on any cyclic machine holds a cycle, and the row prints potential — some run avoids it: the cycle … beside the fail on a machine where every run sets mode = 3 and every run violates. So state and node are accepted; fires, trigger and expression are refused, each with the reason its own kind earns. That is the same shape as the stateful-monitor refusal, and §3.2b takes the identical gate — one gate, one wording, two sections.

The decision, written over the retained relation explicitly. Let G be the sub-graph induced on the non-violating configurations, and let G₀ be the configurations of G reachable from the opening within G. A run avoiding the violation exists iff G₀ holds a cycle, or G₀ holds a configuration i with successors[i].length === 0 in the full retained relation. guaranteed iff neither.

Both scopings in that sentence are load-bearing, and the draft got both wrong.

• "reachable from the opening" alone admits a cycle that is only entered by passing through a violating configuration. On such a machine every run violates, the truth is guaranteed, and the tool would print potential naming a cycle no violation-avoiding run reaches — a sentence about a specific run that does not exist.
• "a configuration with no successors" alone reads naturally as no successors in G, and that reading is unsound. Take nominal --completion--> hazard, hazard --completion--> hazard, property absence (state hazard) × globally. Violating = {hazard}; G = {nominal}; in G, nominal has no successor, because its only successor is outside G. The rule would report potential — some run avoids it, while every maximal run is nominal → hazard → hazard … and every one violates. A sink is a sink in the full graph or it is not a sink.

The failure direction of both mistakes is toward potential, which is the safe direction for the claim word and the wrong direction for the sentence — and the sentence is the entire deliverable of this feature.

Verdict vocabulary — and the rows are a DISPATCH, evaluated top to bottom, because the precedence is part of the specification. The draft listed them unordered, the potential row and the alphabet row overlapped, and the prose beside the table resolved the overlap toward the unsound answer. The order below is the fix; a test asserts it by running a machine that satisfies rows 5, 6 and 7 at once and requiring row 5's sentence.

Rows 1 and 5–7 are the four clauses of walkIsExact, spelled as four sentences rather than one. The gate is one predicate and the dispatch is one failedClause switch: the implementer computes Exactness once and the table selects the sentence. That is what the collapse buys here — the draft had this section carrying its own bespoke conjunction (walk.exhaustive ∧ alphabet.length === 0 on one value and nothing on the other), and §3.2a, §3.2b, §3.5a and §3.8 each carried a different one. Why the clauses stay four sentences and not one: an author whose machine names abort and an author whose machine guards on an unset attribute have two different things to do about it, and a single "this walk is not exact" would tell neither of them which.

Why rows 5 and 6 are two rows and not the draft's one. The draft's condition was alphabet.length > 0 and its sentence was "this machine names triggers". But bounds.alphabet is machineAlphabet, which by design contains every after(n) label (explore.ts:277, docstring :266-276), so on a machine whose only labelled transitions are dwells the tool would print "this machine names triggers" about a machine that names none — and send the author to a carrier for a hazard §2.4(c) explicitly says is not one. The split is by subtraction, and §3.5a takes the identical split for the identical reason.

MUST NEVER print, and why.

• guaranteed on a triggered machine — the latch measurement above.
• guaranteed from a non-exhaustive walk — A8.
• potential on a triggered machine, on one whose timedTransitions is non-empty, or on one whose undeterminedGuards is non-empty — rows 5, 6 and 7, and W3, which reads the whole gate because a claim that a cycle has no exit is a maximality claim (§2.3). The avoiding cycle is a positive existential claim over a relation that over-approximates the environment and time and under-approximates the store; the draft gated the universal value and left the existential one open, which is the polarity error §2.3 exists to stop, committed inside the section that names it.
• guaranteed on a machine with an undecided guard — row 7, and the mirror of the same measurement: an edge the model states and the walk never offered can only make G₀ smaller, so it manufactures guaranteed as easily as potential.
• potential or guaranteed from an expression atom — row 4. The store is not retained, so no configuration is ever marked violating and G is the whole graph: the answer would be potential on every cyclic machine, whatever the model says.
• The sentence "this machine names triggers" about a machine whose alphabet is all dwells — row 5 vs row 6.
• A modality derived from the declaration-order tie-break (correction 13): it would print a claim about the simulator as a claim about the model.
• A modality derived from found — the prefix walked before the first witness is an accident of where the search stopped.
• Any downgrade of the existing fail. claim, code, severity, the witness and exit 1 are untouched.

Exit-code contract. Unchanged. counts and exitCode never see the field.

Tests. Four measured machines, four answers: uav-isr absence(failsafe) ⇒ potential, with the reason string asserted to name the cycle and not the tie-break; a mission DAG ⇒ guaranteed; a sink ⇒ guaranteed; the latch machine ⇒ not decided — the regression that stops the naive guaranteed. A precedence row ⇒ not decided with the stateful reason. --max-configs 1 on the DAG ⇒ not decided. Two fixtures that pin the corrected decision, and each names a wrong answer: (a) a machine whose avoiding cycle sits behind a violating configuration — the reachability-within-G test, asserted guaranteed, with potential named as the wrong answer; (b) nominal → hazard, hazard → hazard, absence (state hazard) — the sink-scoping test, asserted guaranteed, with potential named as the wrong answer. Plus a fires atom ⇒ not decided with the step-property reason, and an expression atom (p=(mode == 3)) ⇒ not decided with the store reason — the refusal the draft's §3.R did not have, with potential — some run avoids it: the cycle … named as the wrong answer on a machine where every run sets mode = 3. The dwell-cycle fixture, factory-built (correction 22): {trigger:'after(5)'} nominal → hazard before {trigger:'after(60)'} nominal → hold, {trigger:'after(1)'} hold → nominal ⇒ row 6's not decided with §2.4(c) beside it, with potential … the cycle nominal → hold → nominal named as the wrong answer and FairnessAssumption asserted absent from the string. The same fixture re-spelled with numeric attrs.after and no trigger — alphabet [], so the draft's alphabet-only rule decided the modality — asserts row 6 as well, with guaranteed and potential both named as wrong answers; it is the fixture that shows rows 5 and 6 are two independent clauses and not one. The trapguard fixture — an ordinary .sysml file, driven through argv as well as in-process (attribute resetOk : Boolean; with nominal → degradedA → degradedB → degradedA and degradedA if resetOk then nominal) ⇒ row 7's not decided with the store sentence beside it, with potential — some run avoids it: the cycle degradedA → degradedB → degradedA named as the wrong answer; both literal variants of the same file assert the modality is DECIDED — = true and = false alike, because clause (d) is about whether the guard was decided and not about which way it went — so the row is shown to track decidedness and not the presence of a guard; the value each one decides to is asserted from the run rather than quoted here. The latch fixture (transition locked accept unlatch then nominal;, also a .sysml file) ⇒ row 5, which is the same machine §3.2a and §3.2b use for their clause-(c) refusals — one model, three sections, one gate. The row-precedence test: a machine satisfying rows 5, 6, 7 and 8 at once — a real trigger, a dwell, an undecided guard, and an avoiding cycle — asserts row 5's sentence, so the dispatch order is pinned rather than inferred. And a test asserting claim, code, severity, detail prefix and witness are byte-identical to today's with and without the field.

Cost. ~35 lines and one field. No new code, no new pattern, no doc-count movement — the cheapest honest thing in this plan. guaranteed is not caught by today's claims guard (§2.6); commit 4 adds the form.

Census. {guaranteed, potential, notDecided} per run — the observation that says whether the annotation ever separates anything on real models.

3.2a — Traps on reach: bottom strongly-connected components

What it decides. Which reachable configurations form a set nothing leaves — Stanley & Laski's condition (2), the half reach does not ship. "If condition (2) is violated, program exit is never reached if the node is reached on some computation."

Command and flags. npm run sysprose -- reach <file> [--element REF] [--max-configs N] — unchanged. No new flag, no new subcommand: the engineer changes nothing about what they type.

Engine. In-process TypeScript. One iterative Tarjan pass (commit 3) over ExploreResult.successors, then the bottom-component filter.

The report. MachineReach (:653-684) gains one field, gated on walkIsExact — not on the publishable the unreachable and dead lists use, which is decreasingOk and which register row A6 (polarity increasing) may not read. A bound or an unsupported construct empties the field rather than shortening it, exactly as states.unreachable is emptied; the other three clauses produce the named inconclusive rows of the verdict table below. The draft's sentence here said publishable, and it is the one place in this section that contradicted its own table — an implementer writing the field from this paragraph lands semantics.mc.publishable.test.ts red on the reflection rule "no increasing row reads decreasingOk", on the very commit that introduces the register's first new increasing consumer, and the cheap repair under a red gate is to weaken the reflection test:

traps: readonly {
  configs: number;
  states: readonly StateRef[];   // the union of the ACTIVE STACKS, not the leaves
  entry: readonly StateRef[];    // shortest path from the opening
}[];

Three exemptions, each with code already in the tree, and the third is the one that keeps the shipped examples silent.

1. A trivial bottom SCC with no self-loop is already verification/deadlock. It is a configuration with no successors — precisely recordDeadlock's subject (explore.ts:631-648). Same defect, two codes, two rows, and the report looks like it found twice as much. This exemption hands the claim to another producer, so that producer has to be gated too, which is register row A0 (§2.3): without it, this section's clause-(d) refusal — "a set it calls inescapable may not be" — prints two lines above an ungated deadlock row asserting the configuration has no way out, on a file whose model states the escape. The exemption is what makes that structural rather than incidental, and A0 is what closes it.
2. An ending is not a trap. A bottom SCC whose configurations are final or terminal is where the machine is meant to stop. Reuse isFinalState and isTerminalNode verbatim — recordDeadlock already calls both at :639-640 with the comments "an ending, not a deadlock" and "done — the same ending, spelled in the notation". Measured on a four-state mission DAG into done: its only bottom SCC is {landed}.
3. A bottom SCC containing the opening configuration is the machine's recoverable core, not a trap. Nothing leaves a bottom SCC, so if the opening lies inside one, the reachable set is that component: there is no configuration to be trapped from. This exemption is load-bearing, not decorative. Measured: FlightModes is one SCC of all four configurations (standby → manual → autonomous → failsafe → standby closes the cycle), it is its own bottom SCC, and none of its four states is final or terminal — so exemptions 1 and 2 alone would file a trap row saying "no run leaves them once entered" about the flagship example's entire normal operating region, and would move cli.sysprose.test.ts:3175's exact diagnostics array. All three shipped machines are single SCCs and all three are silent for exactly this reason.

The genuinely new information over shipped reach is therefore: non-trivial bottom SCCs that do not contain the opening, plus trivial self-looping ones that are neither final nor terminal. The trap probe of §1 — failsafe ⇄ failsafeHold absorbing, completion-driven throughout — is exactly that shape, and it is the feature's positive fixture.

And the exactness gate takes the draft's second positive fixture away, which is stated here rather than discovered in the commit. The draft also offered a latch machine (nominal ⇄ degraded → locked, locked → locked accept latch) as a trap this section finds. Under clause (c) it is refused, because latch is a named trigger and the walk supplies it: locked → locked is a self-loop the environment causes, and whether {locked} is inescapable is a question about the environment this engine has no carrier for. That is the correct answer and it is a real narrowing of the feature — the trigger-driven trap, which is the intuitive one, is the one the gate withholds. What survives is the completion-driven trap, which is what the trap probe is and what the corpus contains. Whether that is enough to justify the feature is what the trap census is for (below), and it is now the honest question.

Verdict vocabulary.

Why the "no trap" sentence is two sentences and not one, and why it counts. The draft printed every reachable configuration lies in one component — nothing this walk found is inescapable. Both clauses are false on this section's own fixtures. (a) The mission DAG into done has four configurations in four trivial SCCs, so "lies in one component" is plainly false — that wording is only ever true of the single-SCC shape the three shipped machines happen to have, while the condition that triggers it (no component qualifies) is satisfied by every DAG whose ending is exempted. (b) On the two-state sink fixture the report would carry a verification/deadlock row saying a configuration has no way out and this sentence saying nothing is inescapable, in one reach output — the tool contradicting itself in one report, which is the identical defect §3.5a forbids for the "every run of this machine terminates" clause and which the draft did not carry over to here. The replacement asserts no component cardinality and names what was exempted, so the deadlock row and the sentence are two halves of one accounting rather than two answers. It is asserted byte-identically on the mission DAG and on the sink, which is where the old wording failed.

MUST NEVER print, and why.

• "the system can always recover" — escaping a trap may need a trigger the real environment never offers.
• "livelock", "deadlock-free" — the second is a bare-word ban with no allowance. (Since U1, 2026-10-14, the first is the name of a finding of its own — a cycle the interpreter's chase goes round, verification/completion-livelock, §8.8 — and stands on that row and nowhere else; the trap row still never says it.)
• A trap row on a non-exhaustive walk — A6.
• Any trap row, and any "nothing is inescapable" sentence, on a machine walkIsExact refuses — A6, all four clauses, and this is where the collapse earns its keep. Four separate measured shapes reach this section and the draft's single time condition caught exactly one of them — and then only in the spelling it was written for. (i) Time: failsafe with after(5) → failsafeHold declared before after(60) → standby — built through ModelFactory, since accept after(n) is a parse error (correction 22) — is a genuine inescapable trap that the walk sees an escape from, on a walk that is exhaustive, alphabet-offered and fully supported, with no verification/nondeterministic-choice row to hint at it. (ii) The environment: the latch machine, an ordinary .sysml file, is one whole-graph SCC only because the walk supplies unlatch; without clause (c) exemption 3 fires and the no-trap sentence publishes. (iii) The store: the trapguard machine, also an ordinary .sysml file, publishes a trap row naming a component the model states an escape from. (iv) Time again, in a second spelling: the numeric-attrs.after machine of §2.3, whose three dwells contribute no alphabet member at all, so an alphabet-scoped clause (b) reads clean and this section publishes "no component of this walk is inescapable beyond its endings" about a machine whose {failsafe, failsafeHold} no run leaves. Enumerating one condition per shape is what failed twice, and scoping a clause to the producer that happened to be measured is what failed the third time; the gate plus a producer defined over the transitions is what stops a fifth shape needing a fifth MUST-NEVER bullet.
• A trap entry witness whose path crossed a dwell transition, stated as a run the semantics admits. The entry path is a positive claim and takes §3.1's re-wording: Entered in 3 step(s) from \standby` — on a run this WALK admits: step 2 fires `after(10)` …`. In practice A6's gate already suppresses the whole row, so this clause exists for the day the gate is relaxed per-claim rather than per-walk, and the sentence is written now so that relaxation cannot be made silently.
• A trap row for an SCC of final states, or a trap row and a verification/deadlock row about the same configuration — exemptions 2 and 1.
• A trap row about the whole reachable graph — exemption 3.
• A trap named by leaf state — one state spans many configurations; states is the union of configStates, never leafOf().
• The bottom-SCC cardinality printed under the recovery question. Measured on the trap probe: the bottom SCC is 2 configurations while the set that cannot reach standby is 4, because that machine has no edge back to standby at all. docs/05's own verdict sentence fuses the two and prints the first number under the second question. They are separate answers, in separate sections, with separate sentences.

Exit-code contract. reach stays report: exit 0, with findings. A trap is verification/unrecoverable-mode, a warning — the severity explore.ts:114-119 reserves for "findings about a MACHINE — a state nothing reaches, a transition nothing fires, a state nothing leaves", which is exactly what this is.

Tests. The trap probe (one trap of 2 configurations, 3-step entry, completion-driven so the gate holds) · the mission DAG into done (none — exemption 2, with the no-trap sentence asserted byte-identically, naming 1 ending exempted) · a two-state sink (verification/deadlock only, trap list asserted empty — exemption 1, and the no-trap sentence asserted byte-identically in the same output as the deadlock row, naming 1 deadlock exempted) · examples/uav-isr.sysml, vehicle.sysml, views-tour.sysml (none — exemption 3) with cli.sysprose.test.ts:3175's exact array unchanged and re-run · --max-configs 2 on the trap probe (list empty, not shortened).

The three gate fixtures are the commit's named negatives, one per mechanism, and two of the three are ordinary .sysml files.

• The preempted-dwell fixture (after(5) → failsafeHold before after(60) → standby), built through ModelFactory in the test file and driven through reachReport in-process — not a corpus .sysml file and not through argv, because the text spelling does not parse (correction 22): the trap list is suppressed with the time sentence, and the test names the wrong answer explicitly — a recoverable/no-trap pair on a machine whose failsafe is genuinely inescapable.
• The latch fixture, state nominal; state locked; transition nominal then locked; transition locked accept unlatch then nominal; — a .sysml file, asserted through argv and in-process. Measured today it walks 2 configuration(s) explored, depth 1 — exhaustive under {…, alphabet unlatch}, 2 of 2 state(s) reachable; 2 of 2 transition(s) fired, 0 dead, rc=0, no findings. The test asserts the clause-(c) refusal and names no component of this walk is inescapable beyond its endings … 1 whole-graph component was exempted as the wrong answer — the sentence the draft would have published about a machine whose locked is a mode nothing leaves unless an operator acts.
• The trapguard fixture, in THREE variants and not two, and the arithmetic of which variant proves what is where an earlier revision was wrong. The base file is attribute resetOk : Boolean; with nominal → degradedA → degradedB → degradedA and degradedA if resetOk then nominal — a .sysml file, asserted through argv and in-process. Re-measured at dc6662c: 3 configuration(s) explored, depth 2 — undetermined under {…, alphabet no named trigger} — 1 guard(s) the walk could not evaluate; the unreachable, dead and no-way-out lists are WITHHELD, 3 of 3 state(s) reachable; 3 of 4 transition(s) fired, **dead withheld**, one verification/guard-undetermined, rc=0. It asserts the clause-(d) refusal and names trap — 2 configuration(s) form a set nothing leaves: {degradedA, degradedB}. Entered in 1 step(s) from \nominal` as the wrong answer. **= falseis the variant that asserts the trap row IS published** — measured3 of 4 transition(s) fired, 1 dead, dead degradedA -> nominal, exhaustive under {…}: the guard is present and *decided*, undeterminedGuardsis empty, the gate holds, and{degradedA, degradedB} is a genuine bottom SCC that survives all three exemptions. **= trueis the THIRD variant and it asserts the exemption-3 sentence, not a trap** — with the guard true the escape edge is retained, the relation is one SCC of all three configurations containing the opening, and the correct output isno component of this walk is inescapable beyond its endings … 1 whole-graph component was exempted. Written as two fixtures with = truein the positive slot, this test lands **red on commit 8**, and the cheap repair under a red gate is to weaken exemption 3 — the exemption §3.2a calls load-bearing, without which the flagshipFlightModes gets a trap row over its entire normal operating region. Written as three, the pair proves both halves of the intended claim: **the clause tracks the guard's decidedness, not the guard's presence** (= falsepublishes a trap, the unset variant refuses), and **a decided-false guard is not a withheld edge**. The code-set guard —it('names the seven codes this engine can raise')intest/unit/semantics.mc.reach.test.ts`, an exact sorted array — goes to eight, title string included; see commit 8.

Cost. One MachineReach field, one Tarjan consumer, one code (+1; npm run codes regenerates the figure, which is why no absolute catalogue count appears in this plan), one renderer block in machineLines (scripts/sysprose.ts:3085-3111), npm run codes. the guide's reach transcript is not machine-checked — docs-counts.test.ts pins its figures from the shipped example and not one of them is a reach number — so it is re-pasted by hand here and added to the claims list rather than trusted. Grep the guide for configuration(s) explored.

Census. {sccs, bottomSccs, trapsAfterExemptions, exemptedAsEnding, exemptedAsDeadlock, exemptedAsCore, refusedByGate} per machine, the last carrying the failed clause. The kill measurement — three consecutive real models that are one SCC or a DAG into final states — becomes a query over recorded runs, and the gate adds a second, sharper one: if refusedByGate reads 'environment' on most machines carrying a trigger, the feature answers only completion-driven designs and the honest question is whether that population exists. Measured, from §5(d): 3 of 3 shipped examples are exempted as core, and of the eleven machines in the tree only GuardProbe::Ctrl would be refused by the gate, on clause (d) — every machine has an empty alphabet and no dwell transition — so the gate costs this feature nothing on the shipped examples and the whole exposure is in models nobody in this tree has written. That is a pass and not evidence; the census is what turns it into data.

3.2b — The recovery pattern: reverse reachability to a named state

What it decides. Once the system enters degraded / failsafe / maintenance, can it get back to a state the engineer names? AG EF p, over any atom and any scope — which is what §3.2a's structural report cannot ask.

Command and flags. check-behaviour <file> --element REF --pattern "pattern=recovery, scope=globally, p=state standby", or the same fields on a PropertyPattern carrier. p is read by the existing readAtom — but only two of the five atom kinds are accepted, and the gate is part of the arm. AtomKind is 'state' | 'trigger' | 'fires' | 'node' | 'expression' (atoms.ts:58) and resolveProperty applies no per-pattern filter: it calls readAtom for every field in pattern.fields ++ scope.fields (patterns.ts:539-550), so p=fires T and p=(mode == 3) both resolve today. They must not reach the reverse-reachability pass. configStates[i] holds state ElementIds only (the stack, from MachineConfig.stack), §3.P deliberately retains no MachineConfig, and trigger/fires hold on a step rather than at a configuration (Observation, atoms.ts:93-99). Left ungated the target set is empty, and an empty target set lands on this section's own second fail row — not recoverable: \fires T` holds at no reachable configuration at all, verification/refuted, **error, exit 1**, printed about a well-formed model on the strength of an atom kind the engine cannot observe. So the arm accepts stateandnode, and refuses the other three with verification/malformed-property, **each with the reason its own kind earns**: a trigger is observed on a step, not at a configuration, so `recovery` has no target set to reverse fromfortriggerandfires, and this atom reads the store, which this walk does not retainforexpression. **§3.R takes the identical gate in the identical wording** — the draft had §3.R accepting expressionand this section refusing it, two sections stating opposite gates for one restriction, and §3.R is the one that moved (§3.R restriction 3), because §6.1 and §7 decision 12 already said the store is whatexpressionneeds. (The larger alternative — retaining a per-index atom valuation inExploreResultinstead of justconfigStates` — is a much bigger change than §3.P describes and is not taken here; it is what would release the other three kinds, and §7 decision 12 records that.)

The carrier value is a forward-compatibility commitment, exactly as "cover" is (§3.1): a file carrying pattern = "recovery" is refused by any build before commit 9 as verification/malformed-property and exits 2 there. Recorded in docs/CONFORMANCE.md in this commit.

Engine. Reverse reachability over P's relation from {configurations whose stack contains p}, read reflexively — a configuration already holding p reaches it in zero steps, or standby's own configuration is reported as unable to reach standby.

The dispatch arm, which is not optional, and its position is load-bearing. recovery is branching-time, and this engine is a bad-prefix search: search finds no bad prefix for AG EF p on any graph and would return pass for free — the exact failure mode the liveness refusal at :1122-1146 exists to prevent. PatternClass gains 'branching' and checkProperty gains a third dispatch arm placed AFTER the unsupported-construct refusal and BEFORE the search call — by anchor, and only by anchor: after the if (walk.unsupported.length > 0) { … } block, and before const found = search(…). An earlier revision named a line number for this, and the line it named held a comment sitting above the const walk = exploreMachine(…) call; an arm placed there would have no walk, no successors and no configStates and could only ever return inconclusive. That is the whole reason §0.0's contract exists, committed in the one instruction where the position is the specification. Calling exploreMachine a second time inside the arm to make it work is worse: the arm then sits ahead of the unsupported refusal, which is the only enforcement point on this function for the unsupported clause of seenWhole (walk.unsupported.length === 0, one of the two conjuncts §2.3 spells out because the early return sets exhaustive: false with boundHit: 'none') — A7 would read a gate half nothing on this path enforces. The stated position is the only one where the walk exists, that clause has been enforced, and no bad-prefix search has run, which is what the commit's headline test asserts.

The target predicate, and the draft got it wrong in a way that flips an exit code. The draft mandated one predicate for both accepted kinds — "reaches p" is configStates[i].includes(p), never leafOf() === p — and that is state's observation function, not node's. atomHolds (atoms.ts:341-345) reads a state atom as obs.config.stack.includes(...) and a node atom as leafOf(obs.config) === ..., and nodesOf (:137-151) admits every StateUsage in the machine, composites included, so the two readings diverge on any composite state. Measured this session on state nominal; state degraded { state sub1; state sub2; transition sub1 -> sub2; } transition nominal -> degraded; — same command, same walk, one atom spelled two ways: --pattern "pattern=absence, scope=globally, p=node degraded" → PASS, `node degraded` never holds, over the whole run; p=state degraded → FAIL with a 1-step witness.

The consequence in this section is a flipped verdict and a flipped exit code. Under the mandated configStates[i].includes(p), recovery p = node degraded sees 2 target configurations and prints recoverable, exit 0. Under the shipped reading the target set is empty and the row is this section's own second fail — not recoverable: \node degraded` holds at no reachable configuration at all, verification/refuted, **error, exit 1**. Whichever is implemented, recoveryandabsence` then disagree about the same atom inside one command, which is what this section's MUST-NEVER ("a claim word rendered as a different word") and its one gate, one wording discipline exist to stop.

So p is read through atomHolds's own selection, never through a hand-written predicate. §3.P retains configLeaves beside configStates — one integer array — and the arm selects stack.includes(p) for a state atom and configLeaves[i] === p for a node atom, exactly as atomHolds does. The selection is asserted against atomHolds on the composite fixture in commit 9's test file, on every configuration of the walk, so the two cannot drift. The fallback, if configLeaves is judged not worth its array: restrict the gate to state alone and refuse node with the reason its own kind earns — a \node` atom names the active leaf, which this walk does not retain per configuration— in this arm **and** in §3.R's dispatch, in the identical wording the plan already requires forexpression. What is not available is keeping nodeand reading it asstate. And **do not reuse walk.reachable** under either reading: it is fed from next.effects.visited` (the entry cascade), so a state can be in it without being any configuration's leaf or on any configuration's stack.

Verdict vocabulary.

A note on the asymmetry, stated rather than left to the implementer. recoverable is monotone-increasing and not recoverable is monotone-decreasing, so a strictly minimal design would gate only the first on the time and environment clauses. This section gates both, for two reasons and not one. First, the two sentences print from one arm under one qualification string, and a per-direction condition would put two different exhaustiveness promises on one row — the shape §2.2 refuses. Second, and this is the third review's finding rather than an aesthetic: the store clause is not decreasing-safe in either direction. An edge the model states and the walk never offered makes not recoverable easier to state, and measured on the trapguard machine it produces not recoverable: 2 configuration(s) cannot reach \state nominal`, verification/refuted, error, **exit 1**, on a design that declares the recovery transition. A per-direction gate would have kept exactly that row. The cost of gating both is one lost refutation on a timed or triggered machine; the alternative is a row whose qualification means one thing when it says passand another when it saysfail`, and a correct design at exit 1 — which is the shape §3.1 exists to abolish, re-entering through the store.

MUST NEVER print, and why.

• vacuous when p is unreachable. AG EF p over a non-empty reachable set with an empty target set is decidedly false: there is no antecedent left unopened and no scope left un-entered. Printing it as undecided would file a refutation at exit 2.
• The bottom-SCC cardinality under the cannot-reach question — 2 vs 4, measured.
• A recoverability claim, in either direction, from a walk walkIsExact refuses — A7. Three measured shapes, one gate: the latch machine (environment), the preempted-dwell machine (time), the trapguard machine (store).
• A node atom read as a state atom. Measured, the two disagree on any composite state and the disagreement flips both the verdict and the exit code; p is read through atomHolds's own selection or node is refused outright.
• A refutation whose target set is empty because the atom kind cannot be observed. That is the atom-kind gate above, and it is a MUST-NEVER and not only a design note: it is the one path in this plan where a well-formed model earns verification/refuted and exit 1 from a tool limitation.
• "the system can always recover" — §2.4(a).
• A claim word rendered as a different word. The JSON says fail and the text says not recoverable; the text is a detail, and no reader or downstream consumer is shown two different claims for one row. The same rule applies to numbers: where a sentence quotes a configuration count it quotes the named machineConfigs field (§3.1), never the configs field base fills from the product search.

Exit-code contract. behaviour. recoverable counts as pass ⇒ 0. not recoverable is a refuted assertion the author wrote: verification/refuted, error, exit 1. This is the substantive difference from cover, and it is the right one — cover asks whether the design admits a behaviour, recovery asserts that it always does. BEHAVIOUR_EXIT_CODES does not move for this feature, and that was checked rather than assumed: recoverable is a property that holds at every reachable configuration (AG EF p is configuration-wise), so the 0 row's shipped sentence is true of it as written — unlike covered (§3.1) and 5a's pass (§3.5a), which are run-wise and forced the two edits §2.1 lists. The atom-kind refusal exits 2 as verification/malformed-property already does.

Tests. The trap probe ⇒ not recoverable naming 4 configurations, with the trap row's 2 in its own clause. uav-isr with p = state standby ⇒ recoverable, exit 0 — and searchComplete asserted absent, not false, which is the register's half of the dispatch test. A machine whose p is unreachable ⇒ fail with the second sentence, not vacuous. Reflexivity: recovery with p = the opening state does not report the opening configuration. Composite, and it is now a pair rather than one assertion: p = state degraded on state nominal; state degraded { state sub1; state sub2; transition sub1 -> sub2; } transition nominal -> degraded; matches every configuration inside it, and p = node degraded matches none — asserted against atomHolds on every configuration of the same walk, with the absence pair (node degraded PASS / state degraded FAIL, both measured today) asserted in the same test as the thing the two readings must keep agreeing with. Under the fallback design the same fixture asserts node is refused with the leaf reason instead. What must go red either way is recovery p = node degraded answering recoverable at exit 0 while absence p = node degraded passes. The dispatch test: a recovery row never reaches search, asserted by a spy, and the arm's position asserted by a fixture with an unsupported construct ⇒ the unsupported refusal wins, never the recovery arm. The atom-kind tests, one per refused kind: p=fires T, p=trigger abort and p=(mode == 3) each ⇒ verification/malformed-property and never verification/refuted — with not recoverable … holds at no reachable configuration at all named as the wrong answer, and with the expression row's reason asserted byte-identical to §3.R's row 4, so the two sections cannot drift back apart. The three gate fixtures, one per mechanism, with the wrong answer named in each: the preempted-dwell machine — factory-built and driven through checkProperty in-process (correction 22) — ⇒ the time sentence, with recoverable named as the wrong answer; the latch machine, an ordinary .sysml file asserted through argv and in-process, with p = state nominal ⇒ the environment sentence, with recoverable, exit 0 named as the wrong answer (measured: the walk is 2 configuration(s) … exhaustive under {…, alphabet unlatch}, one whole-graph SCC, so the draft's A7 held and published it); the trapguard machine, also a .sysml file both ways, with p = state nominal ⇒ the store sentence, with not recoverable: 2 configuration(s) cannot reach \state nominal`, verification/refuted, **exit 1** named as the wrong answer — the one gate fixture whose wrong answer is a refutation rather than a pass, and the reason the arm gates both directions. --max-configs 2⇒inconclusive`.

Cost. One PATTERNS entry, one PatternClass member, one dispatch arm, one reverse-reachability pass, one atom-kind gate. No new claim word — it reuses verification/refuted, verification/bound-exhausted and verification/malformed-property. The catalogue prose moves in four documents (six patterns → eight).

Census. check-behaviour --json records, per recovery row, {atomKind, targetConfigs, cannotReach, bottomSccOverlap, refusedByGate} — the last carrying the failed clause, or null. The kill measurement: if cannotReach is always either 0 or the whole complement of the opening's component, recovery is answering the question reach's trap row already answers and the pattern should be retired in favour of the structural report — which is the same escape hatch §3.2a's census offers from the other side, and the two are read together at Checkpoint A. refusedByGate replaces the draft's timeSound and asks a wider question: it records how often the pattern refuses and on which clause, which is the number that says whether the gate is a guard or a wall. Measured baseline from §5(d): on this tree it would read null on ten of the eleven machines and 'store' on GuardProbe::Ctrl — no dwell and no trigger anywhere — so the honest reading today is that the gate costs recovery nothing on the shipped examples, that clause (d) has one corpus witness, and that clauses (b) and (c) are still fixture-only.

3.3a — verify --why: the axioms a proof used

What it decides. Nothing new. It publishes a value the tool computes on every run and throws away.

Command and flags. npm run sysprose -- verify <file> [--case REF] --engine smt --why. A flag on the existing row, so COMMANDS.length stays 22.

Engine. z3, already the --engine smt dependency, and zero new solver calls. Half the display already ships: axioms-inconsistent prints the core at smt.ts:676-678 and vacuous at :784, both through coreSentence (:1014), which sorts because the order was measured to move under worker-pool contention (:1003-1013). Only the proved path (:810-834) drops it.

Verdict vocabulary.

MUST NEVER print, and why.

• "minimal core" — there is no deletion loop here. consistency.ts owns that machinery (minimized, coreLabel, DEFAULT_MAX_CORE = 8, the loop at :107-118) and --minimize is what earns the word.
• "the axioms this proof depends on" / "this proof does not depend on X". Measured: with mtow = 18.5, mtowCapA {mtow <= 20} and mtowCapB {mtow <= 22} all in scope, z3's core for mtow <= 25.0 [kg] is {axiom:…mtowCapB, goal:…} — cardinality-minimal, naming the weakest of three sufficient reasons, and not naming the model's own value at all. Swapping the two caps' declaration order did not change the pick, so this is not an ordering artefact. The permitted line in docs/05 covers the false-positive direction only; the measured hazard is the false-negative one.
• A display filtered to the axiom: prefix. R-UAV-001's core is six labels, not three: four axiom:, one goal:, and side:…AirVehicle::endurance — the divisor-non-zero condition on capacity * fraction / cruisePower (encode.ts:169-176, emitted at smt.ts:449/:658), a real proof dependency that shares its qualified name with an axiom. A filter drops it; a name mapping must dedupe.
• "what the verdict stands on". Measured on examples/uav-power-budget.sysml: ComputerDraw, PropulsionDraw and RadioDraw each assert a premise: and none of the three cores contains it — yet the non-vacuity step (smt.ts:768-800) that separates proved from vacuous is exactly a check on those premises.

Exit-code contract. Unchanged. --why changes what is printed and nothing about what is decided.

No schema change here — a deliberate ordering decision. The core is displayed, and EvidenceRecord is not touched. docs/schemas/evidence-record.schema.json is 184 lines of draft-07 with additionalProperties: false at all ten levels, compiled with ajv in two places (test/campaign/verification.test.ts:958 and loadRecords in scripts/sysprose.ts, which refuses the whole attach if any record fails), so a field added there is one-directional: a record written by the new build is refused by evidence-attach on an older build. It is not spent until the census that justifies it comes back positive, and it lands with 3b, which is the feature that actually needs a recorded core.

It is not, however, the only forward commitment in this plan, and the draft's "only" was wrong. Three others have the same direction and the same permanence, and all three are recorded in docs/CONFORMANCE.md in the commit that spends them: a .sysml carrying pattern = "cover" (commit 6) or pattern = "recovery" (commit 9) is refused by any older build as verification/malformed-property and exits 2 there — reproduced today, rc=2 — and the two metadata defs of commits 17 and 22 are compatibility commitments by hard constraint 6. What is true of the evidence field, and distinguishes it, is narrower: it is the only one a later commit cannot undo by re-recording the artifact, because the artifact is validated by ajv in two places with additionalProperties: false. A model file's pattern value can be edited back; a written record cannot be un-written on a build that refuses to read it.

Tests. uav-isr --why: R-UAV-001's core is the six labels, rendered as "4 of 12 axioms plus 1 side condition", with the side: member present and deduped against the same-named axiom; R-UAV-002 is 1 of 12. uav-power-budget --why: BatterySupply 5 script axioms → 1 core axiom; ComputerDraw 6 + 1 premise → 1 core axiom with the premise absent; aggregate 24 → 9 over six obligations. The three-reasons fixture asserts the core is {mtowCapB, goal} and that the sufficiency sentence prints — the test that stops the false-negative sentence being written later. Byte-stability across two processes, because the tool's own comment at :1003-1013 records that the core's order already moved between a solo run and the full suite. The three proved fixtures' detail re-recorded here with the reason.

The trap that makes this look pointless if measured in the wrong place. On uav-isr the core equals the syntactic footprint relevantAxioms (smt.ts:643, :956-983) already computes — 4 of 4 and 1 of 1, zero further narrowing — and the four symbols are already printed as witnessSymbols in the golden. Any measurement of this feature against the flagship example alone will conclude it does nothing.

Cost. ~30 lines of display, one field on SmtJudgement (:133-156) carried to ObligationVerdict (api/verification.ts:850-898). Blast radius: the proved detail string (:818-825) is pinned in six places, of which only 3 of 38 verification fixtures carry a proved claim.

Census. verify --json records, per obligation, {scriptAxioms, coreAxioms, footprintAxioms} — the three numbers that decide 3b.

3.3b — Staleness scoped to a proof's core — gated on 3a's census

Gate. 3a's census shows real narrowing (core axioms < footprint axioms) on a model the user runs. Measured today: zero narrowing on uav-isr, 24 → 9 on uav-power-budget.

What it decides. Whether an edit could have invalidated this proof, rather than whether the model changed at all.

The kill measurement, run, and it survives wide. One edit at a time, whole-model digest vs a digest over the canonical form of exactly the elements the core names: uav-isr, 19 edits × 2 proofs — whole-model stale 38/38 = 100 %, core-scoped 4/38 = 11 %. uav-power-budget, 8 edits × 5 proofs — 40/40 vs 8/40 = 20 %. Combined 12/78 = 15 % against a stated 90 % kill threshold.

And it is unsound as sketched. Measured via the CLI: adding assert constraint powerCap { uav.cruisePower <= 100.0 [W] } to uav-isr flips both obligations to verification/inconsistent-axioms — MassRequirement included, whose core is {AirVehicle::mtow} and whose read-closure never touches cruisePower. Cause: STEP 0 is global. smt.ts:364 checks the satisfiability of every axiom in the model, once per run, and :667 makes every obligation stand on that one answer. proved here means "negation unsat under a satisfiable axiom set", and the second conjunct is a whole-model property no per-proof scope can capture. docs/05's MUST-NEVER list names the per-obligation vacuity hazard and not this one, and this one is worse: the vacuity check at least overlaps the core, and STEP 0 shares nothing with it.

So it ships as three parts, all solver-free and inside ValidationRule.run's synchronous contract (src/validation/types.ts:97) — and part (ii) needs a function that does not exist yet. The draft budgeted one line, "export relevantAxioms". Measured, that gives src/validation/rules.ts nothing it can call: relevantAxioms(axioms: readonly EncodedRow[], premises: readonly EncodedRow[], goal: EncodedRelation) (smt.ts:956-960) is typed over SMT-encoded artefacts, EncodedRow (:309) is a non-exported local interface and encodeRow (:406) a non-exported local function, so the rule cannot construct an argument. Exporting the three of them alongside it would make every npm run check of any file carrying an evidence record run the encode half of the verify pipeline synchronously — and, because RULES is reached from safeValidate in src/ui/store.ts, would pull the SMT encoder into the browser bundle. That cost is real, it is not in this section's cost paragraph, and it is not paid. What ships instead: footprintOf(model, obligation): ReadonlySet<ElementId> — the same read-closure computed over Obligation rows at the model level, with no encoding — placed beside the obligation worklist and exported from src/api/index.ts. It is not asserted to be cheaper; it is asserted to be the same answer: a test runs it against relevantAxioms' membership on all 38 verification fixtures and requires set equality, so the two cannot drift and the rule reads the model-level one. The rejected alternative is written down here, with its bundle impact, so nobody re-derives it as a shortcut in the commit.

(ii) is KeY §9.3.1 made mechanical — "a specification cannot possibly talk about memory entities which are only to be included in an extension". (iii) is the price of honesty, and it is the trade this candidate hides: it is measurable per model before anything is built, which is what 3a's census is for.

(iv) is the third review's finding, and without it this feature ships a green absence claim over a proof the tool itself calls vacuous. Part (iii) closes STEP 0 and leaves STEP 2 open, and STEP 2 is the check that separates proved from vacuous. The premise set is in none of the other three digests: STEP 0's script is built from axioms alone (smt.ts:347-366), relevantAxioms returns kept over axioms and never returns a premise — premises only seed the symbol closure (:950-983) — and §3.3a's own measurement records premises absent from the cores (uav-power-budget: "ComputerDraw 6 + 1 premise → 1 core axiom with the premise absent"). So a premise edit that changes no symbol moves nothing (i)–(iii) look at. Executed this session on a copy of examples/uav-power-budget.sysml, one edit, assume constraint { fc.supplyVoltage >= 20.0 [V] } → >= 200.0 [V] — same feature, same symbols, no axiom touched: the run goes from 0 inconclusive, 6 discharged with UAVPowerBudget::ComputerDraw … proved to 1 inconclusive, 5 discharged with vacuous: the premises are unsatisfiable under the axioms … verification/vacuous. Under the three-part design the stored evidence for that obligation reports current within this proof's scope after that edit. §3.3b's own MUST-NEVER names the hazard ("the non-vacuity precondition can break and turn proved into vacuous") and trap 18 names it again; three conjuncts that do not reach it are not a scope, they are a gap with a sentence in front of it.

Verdict vocabulary.

MUST NEVER print. Plain current — the claim is scoped and the words say so. "this edit cannot affect the claim" — UNSAT of a subset survives, so the negation stays unsat, but the non-vacuity precondition can break and turn proved into vacuous; part (iv) is what makes that sentence checkable rather than a warning. A verdict from part (i) alone, or from any three of the four. current within this proof's scope after a premise edit — measured, one >= 20.0 [V] → >= 200.0 [V] and the obligation the record covers is vacuous. "the axioms this proof used" as a synonym for "what the verdict stands on".

Exit-code contract. validation/stale-evidence stays a warning under npm run check. RULES.length stays 25 — no new rule — so the eight docs-counts assertions keyed on it stay green.

Tests. The 19-edit and 8-edit sweeps as golden tables — and, separately, the census fields asserted on a single run of each sweep member, because the goldens are a one-off pre-build measurement and the census is the instrumentation. footprintOf equals relevantAxioms' membership on all 38 verification fixtures, asserted as set equality. powerCap ⇒ stale via (iii), on a proof whose core it never touches. packFloor ⇒ stale via (ii) where (i) says current. txPower ⇒ nothing fires. supplyVoltage >= 20.0 [V] → >= 200.0 [V] on uav-power-budget ⇒ stale via (iv), where (i), (ii) and (iii) all say current — added to the 8-edit sweep as its ninth member, and it is the row that must never read current; the same run asserts the obligation itself has gone vacuous, so the fixture pins the two halves together. A record with no core ⇒ today's sentence, verbatim. Byte-stability across two processes. api.evidence.test.ts:668 and test/fixtures/agent-authoring/L8-evidence-stale/ re-recorded, deliberately. Probe hygiene, learned expensively: after ~130 check calls in one process the z3 WASM worker aborted with "the application has corrupted its heap memory area"; any sweep judging many variants batches across processes.

Cost, and the one-directional commitment. EvidenceRecord (api/evidence.ts:563-616, 14 fields, 11 required) gains optional core and digest fields, plus the matching schema properties. Keep schema at the const 'sysprose-evidence/1': bumping it makes recordOfCarrier (:740) treat every already-attached carrier in the wild as unreadable. Old records still validate against the new schema because the fields are optional — and they must be optional anyway, since --engine literal --record produces records with no core. A record written after this commit is refused by evidence-attach on any build before it, and that is stated in the commit message and in docs/CONFORMANCE.md as a measured fact. Second commitment: canonicalElement (:414) is private and canonicalElements (:280) returns an unkeyed sorted array behind a comment that deliberately narrows it ("EXPORTED FOR THE GUARD, not for callers"), so a keyed per-element export is required against that comment — the one API-shape argument in this lane. Plus footprintOf and its equality test against relevantAxioms (above), which is the part the draft mis-sized.

Census — and it is per-run, not per-edit, which is the correction. §5's table promised commit 11 would record a "whole-model vs core-scoped vs three-part stale rate over edits". That quantity cannot be a census field under §2.5's own rule — every census is --json-only and lands inside the existing payload object — because a rate over edits is longitudinal and one npm run check -- model.sysml --json sees a single model version and emits {ok, files: CheckReport[]} (sysml-check.ts:141). Left as written, this plan's only one-directional schema commitment would have been spent with no artifact from which "the second digest earns nothing" could ever be read back, so the commitment could neither be justified nor unwound by data. What ships instead: staleEvidence emits, inside the check payload and per evidence record, {wholeModelMoved, coreMoved, footprintMembershipMoved, axiomSetMoved, premisesMoved} — five booleans, no new top-level key. The >90 %-agreement kill measurement is then an aggregation over recorded runs, exactly the way commit 8's trap census turns "three consecutive real models" into a query. §5's row for commit 11 is corrected to match.

3.4a — Inheritance: disclose the clause a child did not write

What it decides. Nothing new. It discloses what the tool already withholds.

The defect, reproduced on a 20-line probe. contracts prints SpecInherit::StrictMassLimit [RequirementDefinition] / subject v : Vehicle (inherited) / require v.topSpeed <= 60 [m/s] — one guarantee — and does not list the inherited v.mass <= 1500 [kg]. verify --engine literal reports the child's own clause and refutes the parent separately (exit 1, so the run is not silently green). clausesInheritedFrom is populated only on the branch clauses.length === 0 ? inheritedClauseOwners(model, el) : [] (contracts.ts:1085). The asymmetry: the same block already prints (inherited) for the subject — the tool owns the disclosure idiom and withholds it from clauses only.

Command and flags. contracts <file> [--element REF] [--json] — unchanged.

The change. Drop the ternary at :1085 so clausesInheritedFrom is populated unconditionally; ContractClause (:193-209 — :193-220 as first written runs into ContractSubject's docstring) gains origin: 'declared' | 'inherited' (the word already exists on ContractSubject at :233); add one renderer line.

Safe at three of four consumers by guard order, measured. obligations.ts:487 (if (withClause.has(contract.id)) continue;) runs before :494's clausesInheritedFrom.length > 0 skip; api/verification.ts:418 tests assumptions.length + guarantees.length === 0 first; scripts/sysprose.ts:1124 emptyClauseLine is called only from :1243 under the same emptiness test. The fourth — diagram/contracts-table.ts:114 → ui/panels/ContractsTable.tsx:84-86 — renders clauses filed on X unconditionally and needs its string split in two. That is the only behaviour change in this commit.

Verdict vocabulary. 2 guarantee(s): 1 declared, 1 inherited from MassLimit when the contract owns clauses and inherits some; today's no clause of its own; clauses filed on MassLimit when it owns none. Reports only — never a truth verdict.

MUST NEVER. Show two clauses without saying where the second came from. Say "redefines" where the names do not mask — effectiveFeatures masks by declaredName (inheritance.ts:70-74) and the shipped idiom require constraint { … } builds an anonymous ConstraintUsage, for which masking never fires. Say "behavioural subtype" — KeY p.220: "Respecting inherited specifications is a good practice, but it does not guarantee behavioral subtyping per se." Change what enters the worklist: nothing does here.

Exit-code contract. report. Nothing moves.

Tests. The probe in both spellings (bare-Real and [kg]), asserting identical obligation digests — measured identical, because obligationDigest is over the SI-lowered normal form. The five tests that pin today's non-inheritance behaviour stay green, unchanged: api.verification.test.ts:274, contracts-table.test.ts:140, ui.contracts-table.test.ts:156, campaign/cli.sysprose.test.ts:1200, property.test.ts:455. Zero of 120 goldens move — measured: no model in every .sysml file in the tree inherits a non-empty clause, and the 37 verification goldens are a field-selected projection carrying no clause-origin field. Plus npm run test:e2e (touches src/ui/**).

Cost. One ternary, one field, one renderer line, one UI string split, one census. Do not build verification/inherited-clause-not-read as the cheap fallback: measured, it fires on 0 of every model in the tree while costing a code bump, a npm run codes regeneration and a docs-counts claim. The disclosure costs less and says more.

Census — this is the deliverable. contracts --json gains {contractsWithInheritedClauses, byEdgeKind: {Subclassification, FeatureTyping}, namedClausesMasked, anonymousClausesInherited}. Measured today across every .sysml file in the tree: 0, 0/0, 0, 0. The one typed usage in the corpus (test/fixtures/agent-authoring/L4-requirement-subject-inherited/input.sysml:8) inherits a subject, not a clause. The byEdgeKind split is the whole gate for 4b.

3.4b — refine --via specialize — HELD

Release condition. 4a's census reports contractsWithInheritedClauses ≥ 1 by Subclassification, with namedClausesMasked ≥ 1, on a real model.

What it would decide. Whether requirement def X :> Y is a contract refinement: parent assumption ⊨ child assumption, child guarantees ⊨ parent guarantees — the two obligations judgeDerivation (refinement.ts:1180, docstring :1156-1179) already computes as A_R ∧ γ ⊨ A_D and A_R ∧ ⋀ nf(C_D) ∧ γ ⊨ G_R.

Command. refine <file> [--element REF] --via specialize — a new value of an existing flag (VIA_VALUES, scripts/sysprose.ts:2072), never a subcommand. It moves the --via doc string (sysprose-spec.ts:707-710), the error message at :2087, the byte-pinned CLI-REFERENCE.md, the family pin at cli-reference.test.ts:181-191, and cli.sysprose.test.ts:2053 whose name says "the four families".

Engine. z3. Orientation is measured, not guessed: requirement def X :> Y stores Subclassification src=X tgt=Y — the child points at the parent.

MAY print. specialization refines: the child assumes no more and guarantees at least as much — over 1 declared clause; 1 inherited clause was not re-checked · not a refinement: StrictMassLimit redefines \massOk` and weakens it — witness v.mass = 1600 kg·not evaluated: both clauses are anonymous, so redefinition cannot be expressed and no weakening could have been detected·vacuous·inconclusive`.

MUST NEVER. "behavioural subtype." · Any verdict over origin === 'inherited' clauses — if the inventory folds the parent's guarantees into the child, the guarantee obligation becomes true by construction wherever masking did not fire: a pass manufactured by the tool's own bookkeeping. · Any claim that the check can refute on the shipped idiom — weakening is inexpressible without a clause name, so on anonymous clauses it can only ever pass, and a check that cannot fail on real input is vacuous. That fact goes on the verdict line, not in a footnote.

Three traps, all measured, and the second is why inherited clauses stay on the display side forever.

• Double-filing. generalizationsOf follows the whole specialization family including FeatureTyping, so requirement massOk : MassLimit; — the OMG's ordinary apply-shape — returns the definition's clauses too. Gate on the edge kind, not on effectiveFeatures alone. A test asserts that shape files exactly one obligation.
• Obligation identity collides. obligationDigest (api/evidence.ts:473-483) is over the SI-lowered normal form and nothing else; the evidence key is clause + obligationDigest (:830); an inherited clause's clause is the parent's qualified name, because the ConstraintUsage lives in the parent's body. evidence-attach would write the child's evidence into the parent's braces. Fixing that by adding the owning requirement to the digest input moves every digest in the tree — all 37 verification goldens and every stored record stale at once.
• Masking is by bare name, with no redefines keyword required. Two clauses sharing a declaredName across a chain mask silently, and effectiveFeatures returns the survivor — which is the weaker one, i.e. the violation to report. Whatever prints must name the masked clause and its owner, not only the survivor.

Exit-code contract. refine, and no clause of REFINE_EXIT_CODES moves for this feature. Every verdict above lands in a bucket that already exists: a refinement counts as refined ⇒ 0; not a refinement is notRefined ⇒ 1 with a witness the tool re-read, which is exactly what the published 1 row promises; not evaluated (both clauses anonymous) and vacuous are inconclusive/vacuous ⇒ 2, and neither is lowerable. This is stated here rather than assumed, because §3.6 shares the --via specialize value and its verdict does not land in an existing bucket (see there).

Tests, if built. The --via family pin and cli.sysprose.test.ts:2053 re-recorded with the fifth value · the FeatureTyping apply-shape files exactly one obligation · the anonymous-clause case prints the could-not-have-been-detected sentence and exits 2, never 0 · a masked named clause names the masked clause and its owner, not the survivor · no obligationDigest in the tree moves, asserted across all 37 verification goldens · a verdict is refused over any origin === 'inherited' clause, asserted by the absence of the parent's qualified name in the obligation list.

Cost. Low code, high blast radius: contractsOf/contractOf has 9 production callers outside contracts.ts and sits under 9 of 22 subcommands; Contract.guarantees/assumptions is read at 16 sites in 6 files. New code: verification/specialization-weakens (error) — which must join VERIFICATION_ERROR_CODES (api/verification.ts:1078) in the same commit or diagnostic-codes.test.ts:71-74 goes red on landing.

3.7a — The signature census

What it decides. Whether there is a dependency template in these models to read at all.

Why the proposed check cannot be built as written. The Dependency Template is intra-procedure: transposed, "this part's in port may be used inside it to obtain that out port". Every candidate source of that relation reads zero on examples/uav-isr.sysml (correction 11), and the connector graph is the composition of the parts' templates across boundaries — never any part's own — which is why its longest directed path is 1 hop with 0 intra-part edges. With DT = ∅ the arithmetic is 16 findings over 15 ports on uav-isr, 4/4 on vehicle, 6/6 on views-tour: 100 % of ports flagged on every model in the tree. A check that fires on everything reports nothing. And the obvious retreat — "a part with an empty export set fails condition 2" — flags 1 pure source (BatteryPack) and 1 pure sink (PropulsionUnit); in the book's setting an export-less procedure is a bug, in SysML a leaf actuator with in ports and no out ports is a correct model.

A validation rule is ruled out outright. All six shipped examples check 0 errors / 0 warnings / 0 info, measured. A condition-1/2 rule emits 26 findings across three of them and breaks that guard on contact. If it ever ships it is a report.

Command and flags. npm run sysprose -- connectivity <file> [--signature] — a mode on the existing command, never a subcommand. The cost comparison is the argument: a flag adds one entry to connectivity's (today empty) flags array, turns backedBy into the fn1 + fn2 (path) form the README parser already accepts (readme.test.ts:280-289), and moves no count guard. A subcommand moves COMMANDS.length 22→23, two docs-counts claims, a README row in order, and the generated exit-contract sentence — and would then have to explain why two commands disagree about what a port is.

What it reports (--json, inside the connectivity object).

census.signature: {
  partsWithBoundaryPortsAndInternalParts,   // uav-isr 0 · vehicle 1 (degenerate)
  sameOwnerPortRelations,                   // 0
  directedFeaturesInPortDefs,               // 0
  partsOwningBehaviour,                     // 0 of 14
  userItemFlows,                            // 0
  nonLibraryBindingClasses,                 // 0
  constraintParametersCountedAsPorts,       // views-tour 4 of 6
  inoutPorts                                // uav-isr 1 (DataLink::antenna)
}

Plus, on the text path, the realised-connection line: 9 of 9 declared connections realised; uav.battery.powerOut → uav.gimbal.powerIn in 1 hop, and — on every verdict, findings or not — structural only — a \connect` is not a guarantee that anything is transported`.

MUST NEVER. Call it verification. Call a port an anomaly. Read a bare connect as value flow — that is refine's standing refusal (refinement.ts:187, :845; measured, all 9 edges file as verification/unsupported-expression … a connection is not an equality), and two commands contradicting each other on the same nine edges is not an option. Read attrs.direction — portFacets (rules-connection.ts:60-70) is the only correct reading in the tree: declared-or-inherited, net conjugation where ~ cancels twice, plus the PortDefinition generalization closure. Present the port inventory as a port inventory: on views-tour, 4 of 6 "ports" are in cap / in p constraint parameters and all four reported unconnected ports are those parameters.

One defect in connectivity's own inventory that this census surfaces, and one that is already fixed and is this section's baseline. analytics.ts reads the graph through CONNECTION_KINDS (8 kinds) while connectors.ts uses CONNECTOR_KINDS (10) — the delta is BindingConnector and ItemFlow — and that one is reported as a census row, not as a finding.

The three false danglers on vehicle.sysml were FIXED at c37eb00, and this section's job is to hold the fix rather than to report the defect. An earlier revision filed them as a --json census row named for the enumeration defect, and that was the wrong instrument: both halves of the contradiction printed on the default text path with no flag — every declared port is wired immediately above an unconnected port usages block listing three ports the connections block two lines earlier showed wired — so a --json census row would have neither removed nor qualified them, and after the census landed connectivity would still have contradicted itself in its default output on a shipped example. The mechanism was the one the mission brief named: the wired side keyed on ${ownerId}\0${liftImplicitEndpoint(model, id)} with the port lifted and the owner raw, while the occurrence side keyed on ${o.part.id}\0${o.port.id} off portOccurrences, which enumerates declaration-level usages. The fix normalised both sides the same way, lifting an implicit part copy back to the declaration exactly as the port already was. Re-executed at dc6662c: connectivity examples/vehicle.sysml prints 4 port(s), 2 connection(s), 4 connected, 0 unconnected, the two connections, every declared port is wired, and 4 endpoint(s) lifted onto the port they redefine; 8 library and 4 re-derived candidate(s) excluded — no unconnected port usages block, exit 0. The report also carries ConnectivityReport.unreconciledPorts, which is the fix's own standing check that the two readings agree; it is [] on the examples. What this section owes it is a baseline, not a census row: §3.7a's tests re-run that behaviour and assert it did not move, §3.7b's condition-2 fixture asserts against the fixed enumeration, and both cite unreconciledPorts by name rather than asserting the absence of a sentence.

Exit-code contract. report, exit 0. Two hard constraints: the default first line stays byte-identical (four docs-counts claims regex it off USER-GUIDE.md:503 — measured 15 port(s), 9 connection(s), 14 connected, 1 unconnected), and the --json top level stays exactly ['connectivity','file','ok'].

Tests. The four docs-counts figures and the campaign JSON key list re-run unchanged. The census values pinned on all six examples. The inout port counted once in each of import and export. The constraint parameters labelled as parameters. The c37eb00 baseline asserted rather than the defect re-reported: on examples/vehicle.sysml, unconnectedPortUsages is empty and unreconciledPorts is empty, and every declared port is wired is asserted never to appear in the same output as an unconnected port usages block — on any example, which is the invariant rather than the instance. All three hold at dc6662c before this commit is written, so each is a regression assertion; a commit that reports them as new findings is reporting somebody else's fix. uav-isr's 15 port(s), 9 connection(s), 14 connected, 1 unconnected first line is asserted byte-identical through this commit.

Cost. ~60 lines, one flag, one ConnectivityReport nested field, one portFacets export.

3.7b — Conditions 1 and 2 — HELD

Release condition. partsWithBoundaryPortsAndInternalParts ≥ 1 and a non-empty dependency template derivable from that part. Measured today: 1, and degenerate — Vehicle has 1 in port, 2 internal parts and no out port at all.

MAY print, if built. condition 2 not satisfied: in port \radio.videoIn` influences no out port of `DataLink`·conditions 1 and 2 not evaluated for DataLink: the model states no dependency inside it` · the structural-only line on every verdict.

MUST NEVER. Say which side is wrong — the book's own triage (p.159): "perhaps the code is correct and only the signature should be adjusted." The finding says the declaration and the structure disagree. Let an inout port satisfy both conditions through itself — DataLink::antenna sits in import and export at once and is simultaneously the one genuinely dangling port connectivity already reports; it will be the first port any implementation gets wrong, in both directions. Mix granularities in one sentence — connectivity keeps unconnectedPorts (per declaration) and unconnectedPortUsages (per occurrence) strictly apart, and the comment block at analytics.ts:1278-1300 exists because collapsing them hid real dangling ends. Claim conditions 3 and 4: both presuppose a procedure activation — an entry at which an out parameter is undefined and a program order over which it becomes defined — and a SysML part is a continuously existing structure with no entry. The nearest analogue is an action def with directed parameters, of which there are 0 across all six examples. docs/CONFORMANCE.md records "3 and 4 not transposed" as a declared limit; silence would read as coverage.

One design axis to state rather than leave to silence — and the warrant for half of it is a page nobody opened. The axis: an author-written dependency annotation (SPARK's DERIVES is the canonical example) versus a template derived from the code. docs/05 puts Sysprose on the derived side and rules out new vocabulary — and on this corpus there is nothing to derive from. Candidate 7 as written cannot be built without either contradicting its own design axis or waiting for models with internal structure behind boundary ports.

What goes in docs/CONFORMANCE.md is the measured half only: "there is no intra-part dependency relation in these models to derive a template from, so conditions 1 and 2 are not evaluated and conditions 3 and 4 are not transposed." The SPARK contrast stays out of the conformance record, because its only warrant in this lane is docs/05 §5 item 5 — book pp.153-154, listed by docs/05's own author as a supporting passage they did not verify — and docs/CONFORMANCE.md is the record readers treat as measured. The axis sentence keeps its place here, in the plan, labelled: SPARK's DERIVES is cited from docs/05 §5 item 5, unverified on the page; the design decision does not rest on it, and the measurement on this tree does not speak to it. The failure direction is conservative either way — no verdict is affected — so the fix is to put the unverified sentence where an unverified sentence belongs, not to re-derive a book page to justify a hold. §0's accounting is corrected to match: item 5 is reused in this plan's prose, with the label, and nowhere in a shipped doc.

Exit-code contract, if built. report, exit 0 with findings, exactly as §3.7a. A structural disagreement between a declared signature and the connector graph is not a refutation and never spends the 1 — which is also why it is a connectivity mode and never a ValidationRule (a rule would break the six examples' 0/0/0 guard on contact, measured).

Tests, if built. The structural-only line on every verdict, findings or not · the inout self-dependency excluded in both directions, on DataLink::antenna, which is simultaneously the one genuinely dangling port connectivity already reports · a bare connect never read as value flow, asserted against refine's census on the same nine edges · per-port and per-occurrence granularities never mixed in one sentence · and the vehicle.sysml regression, against the c37eb00 tree: the three false danglers were an enumeration defect in portOccurrences that c37eb00 fixed (§0.1, §3.7a), so a condition-2 finding built on that enumeration does not inherit it — and the fixture asserts the fixed baseline (unconnectedPortUsages empty, unreconciledPorts empty, no condition-2 finding on any of the three) rather than asserting the absence of something this commit never produced. An earlier revision of this fixture could not have passed: it promised a regression against a defect no commit in §4 fixes, because the fix is not in §4 at all.

3.5a — Liveness on an acyclic graph — HELD

Release condition. Commit 3's census reports ≥1 machine with acyclic === true on a walk where walkIsExact holds — the three-valued field of §2.3, which reads null whenever the gate fails, so neither an unsupported-construct walk over an empty relation nor a machine that is acyclic only because a guard was unbound can flip this gate. Measured today: 0 of 3 shipped; 2 of every .sysml file in the tree, both off -> on fixtures whose terminal configuration is already a verification/deadlock row.

What it would decide. existence and response on a machine whose reachable configuration graph is acyclic, where every run is finite and no fairness assumption is needed.

It is not an acceptance flip. The refusal returns above the const walk = exploreMachine(…) call in checkProperty, so today a liveness row carries configs: 0, exhaustive: false, witness: [], activated: false — no graph is ever built. 5a is walk first, then classify: move the class check below the exploreMachine call and below the unsupported-construct refusal that guards it (the block that refuses when walk.unsupported.length > 0), and decide only when the walk is exhaustive and acyclic === true. The instruction names the two constructs it must sit between and no position; an earlier revision named a line, and the line held a comment.

It must ship a finite-run semantics, because the engine has none. patterns.ts reasons only about finite bad prefixes; existence/response over finite maximal runs is not merely unimplemented, it is undefined here. The commitment, printed on the verdict line and added to the semantic profile as a seventh field — and it defines two run classes, not one, because 5b's fair arm needs the second and the draft's single-class wording would have made 5b's own refutation a sentence about a run its profile says does not exist:

This engine admits two classes of run, and every liveness verdict says which one it is about. A finite maximal run is a finite path from the opening configuration ending at a configuration nothing leaves; it is the only class the acyclic arm (5a) uses. An ω-run is an infinite path, presented as a lasso — a finite prefix plus a named cycle; it is admitted only by the fair arm (5b), only over a declared FairnessAssumption, and only on a cyclic graph. F p is refuted by a finite maximal run on which p never holds, or by a fair lasso whose cycle never holds p; a response is refuted by either class carrying a p with no later s.

The seventh field is named run classes, and adding it moves reach's published output as well — which the draft did not say and which is not free. SEMANTIC_PROFILE is one constant, rendered into both reports — patterns.ts:1416 and explore.ts:916 — so a seventh field changes reach's text and JSON in a commit whose lane is liveness. That is taken here as a deliberate re-record rather than dodged with a behaviour-only profile extension, because a reader who runs reach and check-behaviour on the same machine must not be shown two different readings of it. The price is named in commit 16 rather than discovered on landing — three exact six-element arrays, each becoming the same seven-element array ending …, 'deferred events', 'time', 'run classes':

• test/campaign/cli.sysprose.test.ts — the expect(body.reach.profile.map((f) => f.field)).toEqual([…]) array
• test/campaign/cli.sysprose.test.ts — the expect(body.behaviour.profile.map((f) => f.field)).toEqual([…]) array, a different it(…) some hundreds of lines further down; the two are found by their expression and not by their position, and an earlier revision pointed the second at a --max-configs refusal case that has no profile array in it
• test/unit/semantics.mc.reach.test.ts — the expect(r.profile.map((f) => f.field)).toEqual([…]) array, inside it('carries the semantic profile on the report')

plus the docs/USER-GUIDE.md paragraph whose prose reads "names six things every published formalisation of state machines disagrees about" and then enumerates them — grep for that sentence; it becomes seven, with the run classes spelled out beside time. And reach's text report grows one row under "semantic profile (the reading every figure above holds under)" for a distinction no reach verdict uses — the cost of one constant serving two reports, stated rather than absorbed.

Where the two classes touch the exit contract. BEHAVIOUR_EXIT_CODES' 1 row spends the 1 on "a witness trace of a run this semantics admits", and after this commit that sentence is true of both classes — which is the whole reason the profile field names both rather than committing to finiteness and then contradicting itself two lines later on 5b's lasso row.

Verdict vocabulary.

Evaluated top to bottom, like §3.R's — the precedence is part of the specification.

Why rows 2 and 3 are two rows. bounds.alphabet is machineAlphabet, which contains every after(n) label by design (explore.ts:277), so the draft's single alphabet.length > 0 row would print "this machine names triggers" about a machine whose only labelled transitions are dwells, and then send the author to FairnessAssumption for a hazard §2.4(c) says is not a fairness question at all. Worse downstream: §3.5b's carrier "addresses states and triggers, never transitions" and its census counts fairTriggers, so a dwell label recorded as a fair trigger would inflate Checkpoint B's domainSize — the one number the whole carrier is retired on. The split is by subtraction, and §3.R takes the identical split.

MUST NEVER print, and why.

• A pass on a triggered machine. A10 reads walkIsExact, whose clause (c) is alphabet.length === 0, for exactly the reason the rider's guaranteed does: on a triggered machine the real environment can stall the run wherever it stops offering, and F p can then fail on a run this walk never considered maximal. Making the claim in one lane and refusing it in the other would be the plan contradicting itself. The refutation direction needs no restriction of the ENVIRONMENT, and that asymmetry is sound — but the draft over-generalised it, and this is the correction: any prefix of a p-free run is p-free, so an environment that offers less either admits the same refuting run or stalls earlier on a p-free maximal run of its own. Refutation transfers across withheld triggers; the universal claim does not. It does not transfer across a preempted dwell, and that is a different mechanism entirely: under a dwell the interpreter does not stall, it takes a different edge, and that edge may satisfy the property. Worked, factory-built (correction 22): {trigger:'after(5)'} idle → done declared before {trigger:'after(60)'} idle → stuck, stuck terminal, graph acyclic, walk exhaustive, boundHit 'none' — seenWhole holds and only relationIsTheMachines fails, and existence (state done) globally finds the walk-only maximal run idle → stuck and prints fail — refuted — finite maximal run of 1 step(s) at exit 1, on a design where runStateMachine fires enabled[0] at every advance (execute.ts:1305-1308) and matches tests the dwell only on the timeout branch (config.ts:601-604), so stuck is entered on no run. The existence of a p-free maximal run is monotone-increasing in the edge relation. Hence row 3, hence W4, and hence the same clause on 5b's lasso.

• A fail whose witness run crossed a dwell transition — W4, and row 3 is what prints instead. The fail row is a positive claim over the retained relation, not a bare absence, and the draft's MUST-NEVER list gated it on exhaustiveness alone.

• A fail on a non-exhaustive walk. A refutation of F p asserts that the witness run has no successors, which is an absence claim wearing a witness's clothes: on a truncated walk a configuration whose successors were dropped at a bound is indistinguishable from a terminal one. Both directions of a maximal-run verdict read seenWhole — which is why W4's kind is maximality and why it reads the whole gate rather than the relation half every existential witness reads (§2.3).

• A liveness verdict on a cyclic graph without a declared assumption — that is 5b, and the refusal at :1122-1146 exists to prevent exactly this.

• A verdict that does not name its run class. After this commit the engine admits two, and a refuted line that says only "run" leaves the reader to guess whether the witness is finite or a lasso.

• "every run of this machine terminates" beside a deadlock row without the clause tying them. Measured, on both acyclic machines in this tree the terminal configuration is already reported as "no way out … not marked final". Both are true; printed together without a sentence tying them they read as the tool contradicting itself. The clause is conditional on there being such a row — a machine ending at a properly marked final state has none, and pointing at absent evidence is its own defect.

• "deadlock-free", ever.

Exit-code contract. behaviour. pass ⇒ 0; fail ⇒ 1; both inconclusive rows ⇒ 2, and neither is lowerable by any flag. And BEHAVIOUR_EXIT_CODES moves again here, in both directions (§2.1): the 0 row gains "…or, on an acyclic graph, on every maximal run", because pass here holds over runs and not over configurations and the shipped 0 sentence would otherwise be false of it; and the 2 row's clause "a liveness pattern no bad-prefix search decides" narrows to "a liveness pattern on a graph that is cyclic or was not seen whole", because this commit decides one. Both edits are asserted in cli-reference.test.ts's BEHAVIOUR_EXIT_CODES block at :206-214, and verification/behaviour-unsupported-construct's "not lowerable by --allow-inconclusive" promise must survive both.

Tests. An acyclic mission machine ⇒ pass with the acyclic sentence and the deadlock row asserted in the same output; a variant ending at a marked final state ⇒ pass without the deadlock clause; a dead-ending variant ⇒ fail with the maximal-run witness; the same machine with a trigger ⇒ the environment refusal (row 2); every cyclic machine in the corpus ⇒ today's refusal text asserted byte-identically (row 1); --max-configs 2 on the acyclic fixture ⇒ today's sentence, never a pass and never a fail.

And one already-passing test flips on landing, which the draft did not name. In test/unit/semantics.mc.patterns.test.ts, the it(…) that loops PATTERNS.filter(p => p.kind === 'liveness') over buildChain() — A -a→ B -b→ C -c→ D plus an orphan E — runs on a machine that is acyclic and exhaustive with bounds.alphabet = ['a','b','c'], which is precisely the one shape §3.5a's "byte-identical on every cyclic machine in the corpus" promise does not cover. After the move that row takes row 2 rather than today's refusal. The block is identified by that loop and by buildChain, never by a line: it has moved twice already, and an earlier revision of this table was off by one against it, which mattered because the off-by-one re-recorded a v.code control and left a v.detail assertion in place — a red gate on this commit's own test. Re-measured at dc6662c, the assertions inside the loop, in source order, and what each does:

The rule this table is written under: re-record by the assertion's text, never by its position. An implementer greps for 'liveness not checked in-process' and for the toContain('fairness') beside it, and changes those two.

The two detail re-records are the commit's only assertion movement in that file, and they are named here so the diff reads as a re-record and not a fixup. The three semantic-profile arrays and the USER-GUIDE prose listed above move in the same commit, for the seventh field.

Cost. ~50 lines of engine. The documentation is the work: the refusal sentence is quoted in several places outside the source, and the Files: list is built by grepping for the sentence rather than from this enumeration — measured at dc6662c the sites are docs/CLI-REFERENCE.md (generated, twice), docs/USER-GUIDE.md (the liveness walkthrough and its surrounding prose), docs/CONFORMANCE.md, docs/DIAGNOSTIC-CODES.md (generated, in verification/behaviour-unsupported-construct's entry — not in verification/bound-exhausted's, which an earlier revision pointed at), and docs/AGENT-AUTHORING-CAMPAIGN.md — plus the --pattern help row in sysprose-spec.ts whose text says the last two "report inconclusive", plus the liveness-pair guard in cli-reference.test.ts. Every one becomes conditionally false, and verification/behaviour-unsupported-construct's published entry — explicitly not lowerable by --allow-inconclusive — changes meaning while that promise must survive the edit.

3.5b — A declared, checked fairness assumption, and fair-SCC — HELD

Release condition. 5a has shipped, and a real model carries a cyclic machine with a liveness question and an assumption an author can write that carries information. Measured warning about its own value: bounds.alphabet is [] on every machine in the tree (§5(d)), so environment justice has an empty domain exactly where it is most needed, and the only writable assumption is over choice points — which is the case docs/05 itself flags as possibly carrying none.

And the exactness gate makes that narrowing structural rather than incidental, which sharpens the hold rather than softening it. A11 reads walkIsExact, whose clause (c) requires an empty alphabet, so this arm can only ever run on a machine with no named trigger — and on such a machine fairTriggers is empty by construction and the assumption quantifies over choice points alone. The carrier's strength/fair cells and its splitting reader are unchanged (a future build that gains a carrier for what the environment can supply would release clause (c) and the trigger half with it), but the honest statement of what 5b buys today is strong fairness over declaration-order choice points, and domainSize — the number Checkpoint B retires the carrier on — is now measurably the count of choice points and nothing else. If that reads 0, the carrier is a permanent compatibility commitment bought for nothing, and §7 decision 6's answer is already be prepared to retire it.

The one new definition, and the naming argued. metadata def FairnessAssumption; as a fifth definition in SYSPROSE_VERIFICATION_LIBRARY (verification-vocabulary.ts:160-166), whose doc string opens "Four definitions SysML v2 does not express…" and therefore moves to five — and test/unit/semantics.keywords.test.ts asserts that package text round-trips byte-identically, so text and test move together.

A body carrier, not a tag, by the file's own stated rule: it has a body (a strength and a set), and a bare #FairnessAssumption would be a tag claiming to be an assumption while carrying none — the reasoning already given there for Evidence, PropertyPattern and FaultHypothesis. It belongs in CONFORMANCE.md §8.6's READ table: the tool never authors it, exactly as it never authors a FaultHypothesis.

@SysproseVerification::FairnessAssumption {
    attribute strength = "strong";
    attribute fair = "state autonomous; trigger abort";
}

The set-valued cell is ONE cell holding a delimited list, and the repeated-cell spelling the draft used is rejected on measurement. attribute fair = "state autonomous"; attribute fair = "trigger abort"; parses — the draft measured that, and stopped there, at the parser. The tool's own validator refuses it: validation/duplicate-name (rules.ts:181, severity: 'error' at :183) groups every non-library element by ownerId + declaredName and files an error on each sibling of a repeated name. Executed against this tree: npx tsx scripts/sysml-check.ts on a file carrying exactly that block prints error validation/duplicate-name Duplicate name "fair" within FairProbe::Modes::«MetadataUsage». twice, and the file FAILS the check, rc=1. So the one new model vocabulary lane G commits to could not have appeared in any model that passes npm run check, and §3.5b's "collecting reader" was built to read a shape the tool calls malformed. (#failureMode was measured the same way and is clean; the defect is specific to the repeated-cell spelling.)

Of the three re-spellings available — one delimited cell, indexed cells (fair1, fair2), or a nested usage per constraint — this plan takes the delimited cell, for three stated reasons: sibling names stay unique so validation/duplicate-name is satisfied by construction; propertiesOf's reader is cells.set(name, value), i.e. last-wins, so one name per cell means nothing can be silently dropped (§6.2 trap 28 stops being reachable rather than being worked around); and the tool already owns a delimiter discipline in --pattern, so ; inside a constraint is refused the way --pattern refuses an embedded delimiter, with carrier-unreadable provenance and the offending text quoted. The trade is written down: ; becomes reserved inside a fairness constraint, and that is a compatibility statement in docs/CONFORMANCE.md §8.6 beside the definition.

The measurement, and the layer it was taken at. Parses with zero diagnostics and passes npm run check with 0 errors (the second half is the one the draft omitted, and it is what commit 17's test list now asserts); round-trips idempotently from the second save, with the delimiter and the internal spacing byte-identical.

Rejected names, with reasons. Anything containing realizable — a bare-word ban with no allowance, which is why docs/05 needed a whole-file exemption merely to quote a theorem title. FairScheduling / Scheduler — there is no scheduler; the interpreter concatenates regions. LivenessAssumption — it constrains runs, not properties.

Two reader rules that are load-bearing. (1) Split, do not collect. The set arrives as one cell whose value is a ;-delimited list; the reader splits it, trims, and refuses a member containing a second delimiter. The draft's rule — collect repeated same-named cells, because propertiesOf's reader is last-wins — is retired with the spelling it was written for: with one name per cell there is nothing for last-wins to drop, which is a better outcome than a reader that works around it. An empty member, a duplicate member and an unparseable member are each carrier-unreadable provenance and no verdict, never a silently shortened set. (2) Read both cell spellings (AttributeUsage and the keyword-less ReferenceUsage with attrs.keywordless === true, fault-tree.ts:375-381) and report a seen-but-unreadable carrier as provenance, never as a default.

The set addresses states and triggers, never transitions (correction 8).

Engine. Tarjan plus the fair-SCC procedure, whose recursion depth is the number of constraints (1–3 here). Not nested depth-first search: that is the on-the-fly answer to a product you cannot store, and this walk stores four configurations.

Verdict vocabulary.

MUST NEVER. A liveness verdict without the assumption on the same line — CONFORMANCE.md §8.5 already promises this. The reserved word, for this condition or anything else. A fairness assumption applied to a safety verdict without re-running the four safety patterns under it and reporting any change — the theorem that makes fairness irrelevant to safety holds only for assumptions with a fair continuation from every reachable state, and the counter-example in the same source shows a non-conforming assumption changing the verdict on "never a". The check is the same SCC pass, so it is free. no fair cycle from a non-exhaustive walk — A11. A holds under fairness that quantified over fair cycles only — the idle → parked machine above; the pass line names both run classes or it is a claim about one of the two the profile admits, which is the shape §3.5a's "a verdict that does not name its run class" forbids one section earlier. A refuted under fairness whose lasso runs on dwell edges — W5; the refutation is a positive claim over the retained relation and spends the 1, so it carries the same clause as 5a's fail. A dwell label counted as a fairTrigger — the census field feeds Checkpoint B's domainSize, and machineAlphabet puts every after(n) label in the alphabet, so fairTriggers is computed over alphabet ∖ timedLabels or the number that retires the carrier is inflated by labels no environment schedules.

Exit-code contract — the subsection this section did not have, and its first version routed a verdict under a sentence that means something else. behaviour. holds under fairness {…} counts as pass ⇒ 0; refuted under fairness {…} is a fail ⇒ 1, and the 1 row's "a witness trace of a run this semantics admits" is satisfied by the ω-run class §3.5a's profile defines — that is the whole reason the profile names two classes. Both inconclusive rows ⇒ 2, neither lowerable.

But the 0 row does NOT already cover the fair pass, and the draft said it did. After commit 16 that row publishes three discharge shapes — "every ASSERTION … shown to hold on every reachable configuration, over a graph this walk saw whole", "every cover … witnessed on a run this walk saw", and "or, on an acyclic graph, on every maximal run" — and 5b's pass is none of them: it is run-wise rather than configuration-wise, it is not a cover, and this arm runs only on cyclic graphs (§3.5a row 1 refuses whenever acyclic !== true) over the ω-run class the profile invents for it. Left as the draft had it, check-behaviour <cyclic fair model> exits 0 while its own --help and the byte-pinned docs/CLI-REFERENCE.md, rendered from this constant by exitCodesFor, publish a sentence asserting something the run did not establish — the exact laundering §2.2 forbids and the third instance of the defect §2.1 was rewritten to close.

So BEHAVIOUR_EXIT_CODES moves a third time, in commit 18 — the commit that creates the shape, per §2.1's rule that the edit lands in the commit that changes what the code means. The 0 row gains "…or, under a declared FairnessAssumption named on the verdict line, on every fair run of a graph this walk saw whole", asserted in cli-reference.test.ts's BEHAVIOUR_EXIT_CODES block at :206-214 in the same commit, exactly as §2.1 requires of the other four edits. And commit 18's byte-identity assertion is narrowed to what it was actually for: it asserted the constant did not move between commits 17 and 18, which — with this edit — would be red on landing and would then be "fixed" by deleting the clause. It becomes an assertion over commits 16 and 17 (the constant does not move in the carrier commit), plus, in commit 18, an assertion that only the 0 row moved and the 1 and 2 rows are byte-identical. That keeps the trip-wire — nobody re-opens the constant quietly — without pinning the omission.

Census — the field that decides Checkpoint B, and it did not exist. docs/05 candidate 5's kill measurement has two halves, and the draft instrumented only the first: "If most machines carrying a liveness question turn out acyclic, the fairness machinery has no customer. If most are cyclic and the assumption a user would write is always 'everything is strongly fair', the assumption carries no information." Commit 3's acyclic census answers the first. Nothing answered the second — no Census subsection here, no census in commits 17 or 18, no row in §5's table — so after commit 18 shipped a permanent compatibility commitment, Checkpoint B's instruction to "re-read the fairness census" would have pointed at nothing, and the retirement decision would have been taken on an argument rather than on a number, which is exactly what §2.5's rule forbids. What ships, inside the behaviour payload, per run: {strength, fairStates, fairTriggers, domainSize, continuable, safetyVerdictsMoved}. domainSize is the number of choice points and triggers the declared set actually quantifies over on this machine — 0 is the measurement that retires the carrier, and it is a recorded number rather than a judgement. safetyVerdictsMoved is free: the four-pattern re-check runs anyway. §5's table gains a row for commit 18 naming these fields, and Checkpoint B cites domainSize by name.

Tests. An acyclic / cyclic-fair / cyclic-unfair-lasso trio, the third asserting the ω-run wording and the run class named; a fourth member, idle → busy, busy → idle, busy → done, idle → parked with parked a dead end, under a strong-fairness assumption on the choice point busy — every fair lasso reaches done and idle → parked does not, so the test asserts the verdict is a refutation over the finite-maximal-run class and names holds under fairness {…} — no fair cycle avoids \state done` at exit 0 as the wrong answer (R3-12); a **non-conforming** assumption ⇒ the no-fair-continuation row **and** an assertion that no liveness verdict was printed; a fixture where a safety verdict moves ⇒ the change named. Carrier: package text byte-identical; **npm run checkon the fixture asserts 0 errors** — the assertion whose absence let the repeated-cell spelling through — and a second fixture carrying the **repeated same-named cells is asserted to FAIL withvalidation/duplicate-name**, so the rejected spelling has a name in the suite; the delimited list splits into both members; an embedded second delimiter ⇒ carrier-unreadableand no verdict; an unknown field ⇒carrier-unreadableand no verdict; missingimport SysproseVerification::*;⇒verification/keyword-names-nothing(measured — so every shipped example carries the import or it documents a broken model). The census fields asserted on all three trio members,domainSize: 0` asserted on a machine with no choice point and no trigger.

Cost. The largest behaviour-lane item: a carrier (a compatibility commitment), a splitting reader, the fair-SCC procedure, the fair-continuation precondition, the safety re-check and the census. Two codes: verification/fairness-not-continuable (info), verification/safety-verdict-moved (warning) — and the warning is raised from patterns.ts, not explore.ts, so it has no existing set to join: commit 18 adds PATTERN_WARNING_CODES in patterns.ts and feeds VERIFICATION_WARNING_CODES (api/verification.ts:1061) from both it and BEHAVIOUR_WARNING_CODES, or diagnostic-codes.test.ts:86-89's set equality goes red on landing.

3.6 — Stutter-simulation between an abstract machine and its refinement — HELD

Release condition. A census reports ≥1 pair of state machines related by Refine or Subclassification on a real model. Measured today: 0 across every .sysml file in the tree (correction 10).

What it would decide. Does the detailed machine do only what the abstract one allows? Simulation, not bisimulation and not trace inclusion.

Command. refine <file> [--element REF] --via specialize — the same --via value 4b adds, dispatching on the metaclass of the two ends. One flag value, two features.

No new vocabulary, and that is the finding. Both carriers already exist and both were measured; what is missing is a reader, because derivationsOf iterates contracts. Ship the reader off model.relationshipsTo, exactly as contracts.ts:1074 does for requirements, and make the report state which orientation was read.

Labelling is this tool's own choice and must say so. The rule: the state X atoms whose names both machines declare. On the measured probe pair that is {idle, active} with warmup unlabelled — so the stutter rule for an unlabelled intermediate state decides the verdict on the very example that motivates the feature, and it is written down before the first fixture is recorded. The book's remark that would license comparing over common atomic propositions is docs/05 §5 item 2, flagged unverified by its own author; it is not cited.

MAY print. Detailed is simulated by Abstract — simulation relation of 7 pairs, over graphs of 3 and 2 configurations, both exhaustive; labels {idle, active}; \warmup` carries no common label and was read as a stutter step·no simulation relation exists over the common labels {idle, active}: the pair (Detailed::warmup, Abstract::idle) fails — `warmup → active` has no matching step` · and four refusal sentences, one per clause of the gate, because a verdict refused on three of them had no sentence to print at all — the draft's MAY-print list offered only the first, while §5(b) and commit 20 both said the refusal covers "any of its four clauses":

• inconclusive: \Abstract` was not walked to exhaustion— clause (a),!seenWhole`, on either machine, and the machine is named.
• inconclusive: \Detailed` carries `after(n)` dwell transitions this walk takes without advancing a clock, so a step it matched may be one the interpreter never takes+ §2.4(c) —failedClause === 'time'` on either machine.
• inconclusive: \Detailed` names triggers this walk offers wherever it can decide that the interpreter takes its next event, so a step it matched may be one the environment never supplies+ §2.4(a) —failedClause === 'environment'` on either machine.
• inconclusive: a transition of \Detailed` is guarded by an attribute with no declared value, so this walk never offered an edge the model states and the pair that would have broken the relation may be one it could not see+ the store sentence —failedClause === 'store'` on either machine.

Each names which machine failed and which clause, exactly as §3.2a, §3.2b, §3.R, §3.5a and §3.8 do; one Exactness is computed per walk and the sentence is a failedClause switch over the pair.

MUST NEVER. "equivalent" — simulation is a pre-order. "Detailed does not implement Abstract" from a failed search — the method is sound but incomplete for trace inclusion, so the only honest sentence names the pair that broke it. Any verdict when either walk fails walkIsExact, on any of its four clauses (A12) — and the sentence printed is the clause-named one above, naming which of the two machines failed. An earlier revision spelled this MUST-NEVER as "either walk fails the first three publishability conditions", which is strictly weaker than the register in the direction that matters: that conjunction is seenWhole and nothing else, and it contains none of the time, environment or guard clauses, so a probe pair that fails clause (b), (c) or (d) would have published a simulation verdict over a relation that is not either machine's — while §5(b) and commit 20 both already said "any of its four clauses". The numbered-condition vocabulary is retired for exactly this reason (§2.3): a MUST-NEVER that names conditions by number is a MUST-NEVER that goes stale the moment the gate gains a clause, and this section was the last one still carrying it. Two sections stating different gates for one claim is this plan's own trap 62, committed in the last section still carrying the draft's conjunction. A verdict without saying which reading of the child machine was used: measured, the walk is containment-only (regionTransitions is model.descendants; directStates is model.children), so a specialized machine inherits nothing behavioural today, while effectiveFeatures(Detailed) returns 3 states (masked correctly) but five TransitionUsages, because name-masking is vacuous for anonymous features and every transition in this corpus is anonymous. A check using effectiveFeatures would compare a machine nobody wrote and that reach never walked.

Exit-code contract — and this is the one held feature whose verdict has no bucket today. refine. A refinement found ⇒ refined ⇒ 0. inconclusive: \Abstract` was not walked to exhaustion⇒inconclusive⇒ **2**, correctly. But *"no simulation relation exists over the common labels {idle, active}: the pair (Detailed::warmup, Abstract::idle) fails"* on the measured probe pair is a **DECIDED negative**, andrefinementExitCode (api/verification.ts:2273-2288) has nowhere to put it: it buckets runs into refined/notRefined/vacuous/inconclusive and returns **2** when refined + notRefined === 0(:2280), whileREFINE_EXIT_CODES (sysprose-spec.ts:154) publishes 2 as *"a model that states no decomposition or derivation chain the --via` family can read, or ANY undecided group"*. So the run would print a decided answer under a sentence saying nothing was read and nothing was decided.

The decision, and the alternative that was rejected. This plan takes option (a): the result counts as inconclusive for the arithmetic and REFINE_EXIT_CODES' 2 row gains one clause in commit 20 — "…or a simulation search that decided no relation exists over the common labels, which names the pair that broke it and refutes no obligation" — exactly the shape §2.1 writes for cover's not covered, and verification/no-simulation-relation stays info. Option (b) — count it in notRefined for exit 1 — is rejected because it contradicts this section's own MUST-NEVER (never say Detailed does not implement Abstract from a failed search, the method being sound but incomplete for trace inclusion) and because verification.ts:2290-2298 documents 1 as "one ERROR per decomposition that does not refine" with REFINE_EXIT_CODES' 1 reading "at least one obligation refuted, with a counterexample this tool re-read and confirmed". There is no obligation here and nothing was re-read. Taking (b) would require rewriting the MUST-NEVER and re-grading the code to error, and this plan does neither.

Tests, if built. The probe pair with the measured orientation and the unlabelled-intermediate rule asserted byte-identically — it decides the verdict on the very example that motivates the feature, so it is the fixture, not a footnote · the pair (Detailed::warmup, Abstract::idle) named in the failure sentence · exit 2 with the new REFINE_EXIT_CODES clause asserted in cli-reference.test.ts's refine block, and verification/no-simulation-relation emitted at info · a verdict refused when either walk fails walkIsExact — asserted once per clause, with the latch machine as the child (environment), the trapguard machine as the child (store) and a factory-built dwell machine as the child (time) — A12: extra edges in the child make the search fail more easily, so this is an increasing claim on the child's side and a decreasing one on the parent's, and the gate is required on both rather than reasoned about per side · the verdict line naming which reading of the child machine was used (walked, not effectiveFeatures) · the words "equivalent" and "does not implement" absent from every string this feature can print · refine --via refine on a requirement chain unchanged, and no obligationDigest moved.

Cost. A genuinely new algorithm plus one new relationship reading — the highest-value item here that needs real machinery rather than a re-use, and the one with the clearest measured absence of a customer. New code: verification/no-simulation-relation (info) — info, so it joins neither VERIFICATION_ERROR_CODES nor VERIFICATION_WARNING_CODES, and diagnostic-codes.test.ts's third assertion (every remaining verification/* entry is info) covers it with no constant to edit.

3.8 — Behavioural fault tree by failure-mode injection — HELD

Release condition. The behavioural-lane census (commit 21) reports a real model whose hazard is a mode rather than a broken contract — i.e. a machine carrying an #exceptional state that a contract-level fault tree cannot reach.

What it would decide. Which combinations of component failure modes drive this machine into the hazard state. A cut set is an EF query — candidate 1's engine — run once per fault configuration.

Command. npm run sysprose -- fault-tree <file> --element <StateDefinition|StateUsage> [--max-order N]. fault-tree stops refusing a machine, which is also what finally deletes the dead pointer rather than building a flag to satisfy it: commit 5 makes the message name a command that exists, commit 21 replaces the refusal with a measured "no subject here" answer, and this commit gives the input a lane.

One new name, two reuses. metadata def <failureMode> FailureMode; in the same package, applied as a keyword on a Boolean attribute of the machine:

#failureMode attribute navFail : Boolean = false;

A tag, not a body carrier, because the model can already declare the thing — the failure mode is the store Boolean the guards read, and a body carrier would invent a second name and then join the two by string. This is the specification's own tag case: "a metadata definition with no nested features simply acts as a user-defined syntactic tag", and it says one thing by being present: this Boolean is a fault variable the analysis may set, not a design parameter. Measured: parses, stores attrs.metadata = ["failureMode"] beside attrs.value = false, round-trips idempotently, coexists with #exceptional and a FaultHypothesis carrier, and is inventoried by contracts --keywords as sysprose vocabulary once the package is imported. Reuse #exceptional for the top-level event and FaultHypothesis { maxOrder } for the order bound, read off the machine. So candidate 8 ships one new name, halving the compatibility commitment.

Rejected: Fault / Failure alone (collides with FaultHypothesis and with #exceptional's outcome sense) · FailureModeVariable (jargon) · @FailureMode { name = …; effect = …; } (re-invents addressing for a declared attribute).

Engine. In-process TypeScript downstream of cover, over a seeded store, not a new engine: guards read the same store seedStore fills from the model's literal values. Measured, with transition first nominal if navFail then hazard, seeding false leaves hazard unreachable and 3 transitions dead; seeding true makes 3 of 3 states reachable.

The enumeration discipline is judgeTarget's, parameterised rather than transcribed (fault-tree.ts:624-827): order-0 baseline first (an already-open hazard ⇒ top-event-open, the empty set is the cut set, no enumeration); then the order loop over lexicographic combinations (model order, for byte-identical JSON), skipping supersets of found cut sets; undecidedSets tracked separately so a cut set with an undecided proper subset publishes minimal: false and "MINIMALITY NOT ESTABLISHED"; singlePointOfFailure three-valued, null the moment one order-1 check is undecided; maxOrder clamped and reported back. Every group gains lane: 'contract' | 'behavioural' and every verdict line says which.

MAY print. 3 failure mode(s); minimal cut sets up to order 2: {navFail}, {radioFail, gpsFail}; 7 cover queries, all decided · no cut set up to order 2 — higher orders not explored (A13) · inconclusive: a bound stopped the walk under fault set {navFail} — no absence is claimed for it · inconclusive: this machine's edges include \after(n)` labels offered as named events, so a cut set found here may rest on a dwell the interpreter never grants — no cut set is published and no absence is claimed (**walkIsExactfails on clause (b)**) + §2.4(c) · the same row for the other two clauses, with the injected machine's failed clause named —…names triggers this walk offers wherever it can decide that the interpreter takes its next event…+ §2.4(a), and…is guarded by an attribute with no declared value, so an edge the model states was never offered and `no cut set` would be an absence over a graph this walk did not have…+ the store sentence, the last being the one that matters most here because **the injection substrate IS the store** ·top event already open with every failure mode cleared· and, on **every** verdict:cut sets are computed under a PERMANENCE assumption: each flag is set at the opening configuration and never cleared·no temporal ordering between failures is captured·the absence rows above are about the INJECTED machine; `reach`'s unreachable and dead rows on this file are about the nominal one`.

Why the gate holds the whole report and not one sentence (A13's mixed polarity). no cut set is monotone-decreasing in edges — extra edges make the hazard easier to reach, so they can only add cut sets — and would survive the two over-approximating mechanisms on its own. Every published cut set is the opposite: {navFail} is an existential reachability claim over the injected machine, and a hazard reachable only through a preempted timing edge, or only through a trigger the walk supplied, yields a cut set no run of the interpreter realises. And the store cuts the other way and catches the half that would otherwise have been safe: an edge the model states and the walk never offered makes the hazard harder to reach, so it manufactures no cut set — the decreasing half — directly, on a machine whose guards read exactly the store this feature injects into. So all four clauses hold the report, both halves together, and they are not split — for the same reason §3.2b does not split its arm: a reader cannot be asked to know which half of a report a qualification applies to.

MUST NEVER. no cut set with any order-≤N query undecided (A13). "No single point of failure" when any order-1 query was undecided — singlePointOfFailure stays null. Either of the two stated limits omitted. A permanence claim it did not check: guards read the same store assign effects write, so an effect can clear a #failureMode flag mid-run. The plan refuses such a model, naming the effect, rather than printing "permanence assumed and not checked" — the second is a claim nobody can act on. A behavioural cut set mixed into a contract-level group. An empty cut-set list over a machine the command did not walk — the refusal's own docstring: "'0 cut sets' reads as 'no combination of failures breaks this', which about a behaviour this command never looked at is the loudest false statement it could make."

Exit-code contract. fault-tree, and this commit does not touch FAULT_TREE_EXIT_CODES at all — the 2 row's state-machine clause was replaced in commit 21, in the commit that changed the behaviour it publishes (§2.1). A single point of failure ⇒ 1; undecided ⇒ 2; the no---free and no---allow-inconclusive rules apply to both lanes.

Tests. A three-mode machine with an #exceptional hazard ⇒ {navFail} and {radioFail, gpsFail}, exit 1, 7 queries. A redundant variant ⇒ order-2 only, exit 0. An assign navFail = false variant ⇒ refused by name. A --max-configs 2 variant ⇒ inconclusive with the absence suppressed. A timed variant whose hazard is reachable only across a preempted dwell ⇒ the clause-(b) row — the one §3.8's MAY-print list spells "walkIsExact fails on clause (b)" — with no cut set published and no no cut set printed either, and minimal cut sets up to order 2: {navFail} named as the wrong answer. That variant is built through the API and injected in-process, not added to the example this commit ships: accept after(n) does not parse (correction 22), so a timed .sysml fixture would fail the corpus gate with parse errors and then assert a failed time clause over a walk that never ran. A second timed variant carries its dwells as numeric attrs.after with no trigger (§2.3's fourth reading) and asserts the same row, because that is the shape an alphabet-scoped clause (b) reads clean. Both limit sentences on every verdict. The two-world sentence wherever a reach row is printed beside it. Round-trip and import tests as above.

Cost. One new module (injection.ts), judgeTarget parameterised over a query function rather than transcribed, one lane field on every group, one example model carrying #failureMode, one code — verification/failure-mode-cleared (info), so it joins neither VERIFICATION_ERROR_CODES nor VERIFICATION_WARNING_CODES — and one prose figure in CONFORMANCE.md:29 (6 shipped example models → 7; docs-counts' exampleCount is derived and moves by itself, §4 commit 23). No exit-code contract moves here: commit 21 already replaced the FAULT_TREE_EXIT_CODES 2-row clause, and a test asserts the constant is byte-identical across commits 21 and 23. The compute is cover run once per fault configuration, bounded by maxOrder, and the report is the one place in this plan where the gate holds a whole report rather than a sentence.

Census. fault-tree --json records, per behavioural group: {failureModeFlags, exceptionalStates, ordersExplored, queriesDecided, queriesUndecided, cutSetsByOrder, singlePointOfFailure, refusedByGate} — the last carrying the injected walk's failedClause, or null. The kill measurement is commit 21's census read a second time, after the vocabulary exists: if machinesWithFailureModeFlags stays 0 on recorded runs, the #failureMode tag is a permanent compatibility commitment nobody applied and the lane retires with it. The second, sharper measurement is refusedByGate, and §5(d) is its baseline: the injection substrate is the store, so clause (d) is the clause most likely to fire here — on a model whose guards read any unbound attribute that is not one of the flags — and the only machine in the corpus that fires it today is the guard-undetermined fixture. If queriesUndecided is non-zero on most recorded runs, singlePointOfFailure is null on most of them and the report answers nothing an engineer can act on. The measured baseline, from §5(d): of the eleven machines in the tree exactly one is refused by the gate (GuardProbe::Ctrl, clause (d)) and none carries a #failureMode flag or an #exceptional state, so nothing in this repository exercises the second number and the fixtures are the whole of the evidence for it.

4. Commit plan

Per-commit convention, unchanged from docs/04 §4: implement → adversarial review → fix → full gate.

npm run codes && npm run commands && npm run typecheck && npm run lint && npm test && npm run build

plus npm run test:e2e on any commit touching src/ui/**, src/diagram/** or vite.config.ts — commits 12 and 24. The draft's parenthetical said "commit 12 only", and commit 24's own Files: list is src/ui/panels/Properties.tsx and diagram/contracts-table.ts: both paths exist, both are inside the rule's own scope, and taken literally the closing commit shipped two UI changes with the e2e suite never run — with the parenthetical as the reason an implementer would skip it. npm run campaign is inside npm test.

Standing rules.

• Anything §3 calls an in-process API is re-exported from src/api/index.ts in the commit that adds it — and the same rule runs in the removal direction, which is what the draft's version did not say and what commit 21 needed: a commit that deletes an exported symbol names every barrel that re-exports it, every test that imports it and every test or document that asserts a sentence it composed, in its own Files: list. behaviourLaneRefusal is the measured case (commit 21), and it has one site of each kind.
• Every commit adding a code runs npm run codes — the **N catalogue codes** figure is generated, so it can never be the thing that fails.
• No absolute catalogue count appears anywhere in this plan. Every guard line states a delta (+1, +2) and nothing else. The draft stated absolutes — commit 6's "99 → 101", commit 8's "101 → 102" — which are only correct under one lane ordering: commit 8's own dependency line is 3, 4, so a build that runs lane C before lane B makes the real move 99 → 100, and an implementer following the written number lands a DIAGNOSTIC-CODES.md regen that disagrees with docs-counts.test.ts. The re-order licence below and an absolute count cannot both be right.
• A new flag is never a new subcommand: COMMANDS.length stays 22 through the whole plan, and RULES.length stays 25.
• A commit that deletes or replaces a printed sentence names every campaign case that asserts that sentence THROUGH THE CLI, not only the ones that import the function which composed it. A symbol grep finds the second kind and misses the first; commit 21 is the measured case (cli.sysprose.test.ts's fault-tree refuses a state machine… block asserts two substrings of a refusal it never imports), and a hand-pasted transcript in docs/USER-GUIDE.md is the same class of site with no test at all behind it. The check is a string grep for the sentence across test/ and docs/, run in the commit that changes it.
• Every commit that budgets time, or that adds a case to test/campaign/cli.sysprose.test.ts, assumes the restructured campaign file, which is what the tree already has (§0.1, 189fc6d). The gate is 548.74 s measured at dc6662c, not the 790 s an earlier revision budgeted against, and that file is still the longest pole. A new case picks its invoker, and the choice is part of the Tests: line: run(…) in-process for anything asserting the TEXT a command prints, spawnCli(…) for anything only a process can be wrong about — exit status, - on stdin, an oversized payload, an unknown flag, an unreadable file, --help — and for every solver-bearing subcommand, because z3's WASM module carries process-global state and driving it many times in one worker aborts the module. The failure mode of choosing wrong in that last case is a green run, not a red one, which is why it is written down. A position in the file is anchored by it(...) title, never by line number.
• A commit's Files: list never names a line. It names a file, a symbol inside it, and — where a sentence moves — the sentence. §0.0 is the contract; §4 is where it is easiest to break.

Lane A is the spine and is mandatory. Lane B is a SECOND spine, and the draft's "B…I are independent of one another" was wrong on its own dependency lines. Measured against §4's own text: commit 9 (lane C) Depends on: 6, 8; commit 16 (lane G) Depends on: 3, 6; commit 19 (lane H) Depends on: 13; commit 23 (lane I) Depends on: 22, 6. Commit 6 is lane B and commit 13 is lane E. Drop lane B and commit 9's recovery arm has no cover dispatch to sit beside, commit 16 has no first BEHAVIOUR_EXIT_CODES edit to be "the second pair of edits" to, and commit 23's engine — "patterns.ts (the cover query over a seeded store)" — has no query function at all. So the rule is stated as it actually is:

A is the spine. B is a second spine: C, G and I depend on it. H depends on E. Given A and B, lanes C, D, E, F and G may be re-ordered or dropped whole; H and I may not be dropped independently of the lanes they name.

Each lane's row says what it retires, and the two columns after it say what it needs and what needs it.

Lane H's gate is a conjunction, and the draft presented it as a single census that its own text predicts will not open. §3.6's command is refine <file> [--element REF] --via specialize — "the same --via value 4b adds. One flag value, two features." That value is created only by commit 13, and commit 13 is HELD, gated on 12's census by Subclassification — while commit 12's own Gate proves: line says that census "reads 0 on all six examples and every corpus file." A gate that reads 0 means 13 is not built, means the --via specialize value does not exist, means commit 20 has no flag to dispatch on and commit 20's stated REFINE_EXIT_CODES guard move is unreachable. So:

Lane H opens only if BOTH: commit 12's census reads contractsWithInheritedClauses ≥ 1 by Subclassification (so commit 13 ships and the --via specialize value exists), AND commit 19's machine-pair census reads ≥ 1 (so there is a pair to compare). Measured today both read 0, so lane H is held behind two gates and not one, and it is not an independently droppable lane. The alternative — give §3.6 its own --via value so it stops inheriting lane E's gate — is available and costs one more VIA_VALUES member plus a second family pin; it is not taken here, because two values for one dispatch would then have to explain why the tool has two names for "read a specialization", and because the honest reading of both zeros is that neither feature has a customer.

Lane A — the spine

Commit 0 — docs: land the model-checking implementation plan (doc-only) Status (measured at 510793c, 2026-09-16): 96d68be. Files: ADD docs/06-model-checking-implementation-plan.md. CHANGE README.md — add its row to the Reference-docs index (readme.test.ts > links every document in docs/ walks the directory and fails on any unlinked file). CHANGE test/unit/claims.test.ts SKIP_FILES beside docs/04 and docs/05, for the same stated reason: the MUST-NEVER lists are the list of sentences the guard exists to catch, and they quote deadlock-free and the reserved word verbatim in order to ban them. CHANGE docs/04:§3.8 — one sentence: checkProperty is patterns.ts, not mc/check.ts, which does not exist. CHANGE the ledger. Tests: none. The gate is the point. Gate proves: the document does not itself turn the repository red. Depends on: —

Commit 1 — refactor(mc): one publishability predicate, and the absence-claim register Status (measured at 510793c, 2026-09-16): e64f0d1. Files: ADD src/semantics/mc/publishable.ts (§2.3: Publishability with decreasingOk and no bare ok; the Exactness predicate walkIsExact with its two named halves seenWhole and relationIsTheMachines, the conjunction field named walkIsExact to match every register cell and verdict row that reads it, its failedClause and its sentence; publishabilityOf; ABSENCE_CLAIMS as data — {id, claim, feature, polarity, polarityNote, walkRequires, alsoRequires, otherwise, producedBy} where walkRequires is one of exactly four values ('decreasingOk' | 'walkIsExact' | 'relationIsTheMachines' | null), polarity is one of exactly four ('decreasing' | 'increasing' | 'mixed' | 'not-a-walk') with polarityNote carrying the per-mechanism detail, and alsoRequires holds the non-walk conjuncts; and WITNESS_CLAIMS in the same shape plus kind: 'existential' | 'maximality' and ridesOn: ClaimId | null, for the six positive witnesses of §2.3 — register row A0 included, which is the shipped verification/deadlock claim neither register had — and it registers machinery that already exists: c929278 gates that array on the guards alone, so A0's producedBy points at the shipped gate and this commit adds no code for it). CHANGE the two duplicated conjunctions to call it — const publishable in reachOne (explore.ts), four conjuncts at dc6662c including guardsDecided, not the three it had before c929278, and const exhaustive in checkProperty (patterns.ts), which adds the product-search conjunct — both read decreasingOk, which is what keeps them byte-identical on every model, timed or not; transcribe guardsDetermined as walk.undeterminedGuards.length === 0 and not as a narrower store test, or this refactor silently regresses a withholding that shipped and its own byte-equality gate cannot see it (none of the six examples carries a guard, §5(d)) — src/api/index.ts, docs/CONFORMANCE.md. Two of Exactness's producers do not exist yet — timedTransitions and timedLabels arrive in commit 2 — while the other two already do: bounds.alphabet has always been there and walk.undeterminedGuards shipped at c929278. So the predicate ships here as a pure function over an ExploreResult-shaped argument and is wired in commit 3; nothing reads it before then, which is what makes commit 1 a refactor with a byte-equality gate. Tests: NEW test/unit/semantics.mc.publishable.test.ts — the two existing conjunctions are byte-equal to decreasingOk on all six examples, against the post-c929278 golden (§0.1); every ABSENCE_CLAIMS and WITNESS_CLAIMS row names a producer that exists and a walkRequires that is one of the four admissible values, with null only where the polarity column says not a walk; no 'increasing' or 'mixed' absence row reads decreasingOk unless its alsoRequires names a conjunct covering the mechanism its polarityNote identifies — A0 is the one row that uses that escape and it is asserted to be the only one; no alsoRequires entry on any row names a member of the bound family (seenWhole, decreasingOk, Publishability.searchComplete) — the assertion that stops a bound condition being re-added one conjunct at a time; every WITNESS_CLAIMS row whose kind is 'existential' reads relationIsTheMachines and names no bound, and every row whose kind is 'maximality' reads walkIsExact (§2.3 — W3 and W4 are the two, and the draft's unscoped version of this assertion was red against its own register, which is the shape that lands commit 6's bound-frontier test and the reflection test mutually unsatisfiable); every ridesOn resolves to a row that exists and whose own gate is no weaker; reachReport and the behaviour report are deep-equal before and after on all six examples. Plus a factory-built timed machine in the differential, because the six examples cannot exercise the difference (measured, §5's census: zero after( in any of the six machine files, and correction 22 says no .sysml file can ever contain one): on a {trigger:'after(5)'} machine decreasingOk is asserted true and reachReport's unreachable/dead lists asserted non-empty and unchanged — the assertion that would have gone red under the draft's single ok, which flipped publishable false and emptied a sound finding out of a shipped command. Gate proves: there is now exactly one definition of "may this absence be stated" and exactly one gate on the increasing side; adding a claim without a condition, wiring an increasing claim to the decreasing conjunction, or wiring a witness to a bound is a red test rather than a review comment. Guards moved: none. Zero goldens. Depends on: 0

Commit 2 — feat(mc): exploreMachine retains the successor relation — §3.P Status (measured at 510793c, 2026-09-16): eb36d71. Files: CHANGE explore.ts per §3.P's table — exploreMachine's seen declaration, its opening queue.push, the revisit prune, the admission point, and the walk's result assembly — and ExploreResult (+ successors, configStates, configLeaves, openFrontier, timedTransitions, timedLabels — six fields, and timedTransitions is the one clause (b) reads: the transition set, not the alphabet subset, §2.3); Frontier (+ index). NOT config.ts, and not guardHoldsStore or its callers: clause (d)'s producer already ships. ExploreResult.undeterminedGuards exists at dc6662c (c929278), is populated by stepCandidates, and is what the gate reads; adding a second, narrower field beside it is the duplication the fifth review found, and it would read empty on not mode over a fully valued mode. ADD the fixture models this plan drives through argv, since this is the first commit that reads them: test/fixtures/verification/models/latch.sysml, trapguard.sysml, trapguard-true.sysml, trapguard-false.sysml and trapguard-typed.sysml (the not mode machine) — measured, none of them is in the tree today (grep -rl 'resetOk' --include=*.sysml returns nothing), so a commit that drives them without adding them fails on a missing file. CHANGE src/api/index.ts, docs/CONFORMANCE.md (the relation is retained, is over innermost-level steps only, is interned to integers and is never published as hashes). NOT boundsSentence — the store clause lands in commit 3 (§3.P), because it moves every qualification string in every lane and cannot land in the one commit whose gate is "reach's output did not move". Tests: NEW test/unit/semantics.mc.successors.test.ts — the 5-edge relation, the named spanning-tree negative test, the bound test, the unsupported-construct fixture asserting openFrontier === !walk.exhaustive (the second named negative test; openFrontier === (boundHit !== 'none') is the spelling that pins the bug), timedTransitions and timedLabels both non-empty on the two-dwell fixture — built through ModelFactory in this file, never as a corpus .sysml, because accept after(n) is a parse error (correction 22) — and both empty on every machine in the tree, the numeric-attrs.after fixture asserting timedTransitions non-empty with timedLabels EMPTY and bounds.alphabet === [] (written with model.create, since ModelFactory.transition drops the field — factory.ts — and this is the fixture the draft's alphabet-scoped clause (b) read clean), the parse fact itself asserted (a .sysml source carrying accept after(5) fails the parse at the (; accept 'after(5)' yields attrs.trigger === "'after(5)'" and afterDuration → undefined), walk.undeterminedGuards — the SHIPPED field, characterised rather than built — holding exactly the if resetOk transition on trapguard.sysml, empty on both literal variants, empty on the ten machines in the tree whose guards all decide (GuardProbe::Ctrl is the eleventh, and is asserted NON-EMPTY as the corpus witness clause (d) gained at c929278), and NON-EMPTY on trapguard-typed.sysml (attribute mode : Integer = 3; with transition degradedA if not mode then nominal, measured "guard": "not mode", "unresolved": []) — that last row is the one fixture in this plan that separates the shipped predicate from a narrower "no declared value" reading, and without it commit 1's transcription of guardsDetermined is untested in the direction it can go wrong; bounds.alphabet non-empty on latch.sysml and [] on every machine in the tree; walk.census.counts.unaccounted === 0 on all eleven machines and on every fixture this commit adds — the shipped element-set check, asserted here because §2.3 leans on it and a fixture that quietly refuses would make every other assertion in this file vacuous; the configStates-is-the-stack and configLeaves-is-the-leaf pair on the composite fixture with both asserted to agree with atomHolds; and the differential on all six examples plus the factory-built timed machine. test/unit/semantics.mc.reach.test.ts and the campaign's reach block re-run untouched — including its exact diagnostics array, which is this commit's trip-wire and is named by its it(...) title, not by a line. Gate proves: reach's published output is byte-identical, and the retained relation is the one reachability was computed from. Guards moved: none. That is the commit's entire claim. Depends on: 1

Commit 3 — feat(mc): Tarjan components, acyclicity, and the census Status (measured at 510793c, 2026-09-16): 63d228b. Files: ADD src/semantics/mc/scc.ts — iterative Tarjan over successors, plus bottomComponents, acyclic, reverseReachable. CHANGE explore.ts (acyclic computed three-valued, true | false | null, null whenever walkIsExact is false — not merely whenever openFrontier, because an undecided guard is a cycle-closing edge the walk never had and the field is what lane G's release gate reads — and recorded in reach --json's census, not in the text report; timedTransitions.size, timedLabels.size, alphabet.length and undeterminedGuards.length recorded beside it as the exactness census; the deadlocks return in reachOne STRENGTHENED per register row A0 — it already reads guardsDecided ? walk.deadlocks : [] (c929278), which is walk-wise; A0 adds the leaf-wise conjunct on top of it, so the expression becomes walk-wise ∧ no outgoing transition of the deadlocked leaf is in walk.undeterminedGuards, and the store sentence prints in place of a withheld row. This is a strengthening of availability, not a relaxation of the shipped gate: written as a replacement it would regress c929278, and the commit message says which of the two it is (§2.3, A0); and boundsSentence gains the store clause, appended AFTER the alphabet … clause so the campaign's prefix assertion and its separate alphabet no named trigger substring both stay green — a deliberate re-record moving every qualification string in every lane, held out of commit 2 so that commit's differential stays meaningful), publishable.ts (walkIsExact wired to its producers — walk.timedTransitions, bounds.alphabet, walk.undeterminedGuards, with walk.timedLabels feeding only the failedClause split — plus both registers' walkRequires/alsoRequires columns, kind, ridesOn, and the reflection assertions), src/api/index.ts, docs/CONFORMANCE.md, docs/USER-GUIDE.md — every hand-pasted transcript that prints boundsSentence's output in full, found by grepping the guide for exhaustive under {maxConfigs (measured at dc6662c: two, one under the reach walkthrough and one under check-behaviour) and machine-checked by nothing. The campaign stops its prefix substring before alphabet and checks alphabet no named trigger separately, so an appended store clause keeps both green and leaves both transcripts silently stale; they are added to the claims list in the same commit. Tests: NEW test/unit/semantics.mc.scc.test.ts — FlightModes is one SCC of 4 and its own bottom component; vehicle one of 3; views-tour one of 2; all three cyclic; the two off -> on fixtures acyclic; the trap probe has a bottom component of 2 with 4 configurations unable to reach standby (both numbers, separately asserted); reverse reachability is reflexive; a 5 000-configuration chain does not overflow the stack (iterative, asserted). And the unsupported-construct fixture reads acyclic: null, never true — the commit's named negative test, because the early return at explore.ts gives an empty relation with no cycle and a naive boolean would publish acyclic: true about a graph that was never built, flipping lane G's gate. The second named negative test for the same field is the two-state trapguard file — transition nominal then degraded; transition degraded if resetOk then nominal;, re-measured at dc6662c as undetermined under {…} — 1 guard(s) the walk could not evaluate, boundHit none, 1 of 2 transition(s) fired, dead withheld — asserting acyclic: null with acyclic: true pinned as the wrong answer, and its = true variant asserting acyclic: false; without it lane G can be released by a machine that is acyclic only because a guard was unbound. And A0's assertion, which needs a fixture no earlier revision named. On the trapguard family the shipped walk-wise gate and A0's leaf-wise conjunct agree — deadlocks is already [] there at dc6662c, measured, with verification/guard-undetermined in its place — so asserting A0 on that file proves nothing. The fixture that separates them is a machine with an undetermined guard in one region and a real, fully-decided sink in another: today the whole array is emptied and the sink's row is lost; after A0 the sink's row survives and only the undecided leaf is withheld. That machine is ADDed here. The two fixture machines that carry a real deadlock — on and running, §5(d) — keep their rows byte-identically, because neither carries a guard, and no shipped example carries a deadlock row at all. In semantics.mc.publishable.test.ts: every increasing absence row reads the exactness gate, every existential witness row reads relationIsTheMachines and names no bound, and every maximality witness row reads walkIsExact — asserted by reflection over ABSENCE_CLAIMS and WITNESS_CLAIMS; walkIsExact asserted machine by machine over §5(d)'s eleven — true on nine, false on the unresolved-endpoint fixture with failedClause: 'unsupported', and false on GuardProbe::Ctrl with failedClause: 'store', which is the corpus witness clause (d) did not have when this list was first written (§5's census, re-measured in the suite rather than quoted); walk.census.counts.unaccounted === 0 on all eleven, asserted as the element-set half the gate does not re-check — the one clause of exactness the corpus can actually exercise; failedClause asserted to read 'environment' on the latch file, 'store' on the trapguard file, 'time' on the factory-built dwell machine and 'time' on the numeric-attrs.after machine whose alphabet is empty — one fixture per clause plus the second spelling of clause (b), which is the only coverage those branches will ever get; and the 'environment'-before-'time' order asserted on a machine carrying both, which is the order §3.R's row-precedence test reads (§5: no shipped model has a dwell, a trigger or a guard, so this is fixture-only coverage); and the A1/A2 non-regression on the factory-built timed machine is re-run here, now that the gate is live — reachReport's unreachable and dead lists are asserted unchanged and non-empty on a {trigger:'after(5)'} machine, which is the assertion that fails the moment anyone points the decreasing side at the gate. Gate proves: the algorithm is right on graphs whose answer is known by construction, before any sentence is printed from it — the acyclicity census that gates lane G is installed here, already reading 0 of 3 — the polarity rule and the collapse are machine-checked rather than reviewed, and the gate going live does not move a single shipped reach finding. Guards moved: the bounds line in every lane, for the store clause — a deliberate re-record with the reason in the diff, and the reason it is not in commit 2 — plus every USER-GUIDE.md transcript that prints it in full and that no gate protects, found by grepping the guide for exhaustive under {maxConfigs, and reach's deadlocks output on a machine with an undetermined guard on one leaf and a decided sink on another (A0's strengthening), which moves no shipped golden because no example has a deadlock row and neither fixture machine that does carries a guard. Depends on: 2

Commit 4 — test(guards): the vocabulary ratchet, and the claims guard widened to this plan's sentences Status (measured at 510793c, 2026-09-16): 863ac05, one hash with commit 10. Files: CHANGE test/unit/semantics.keywords.test.ts — generalise the byte-identity round-trip from the four hand-listed definitions to every definition parsed out of SYSPROSE_VERIFICATION_LIBRARY; assert a set-valued cell holding a ;-delimited list round-trips with the delimiter and spacing byte-identical and splits into its members, and assert that a carrier with repeated same-named cells FAILS npm run check with validation/duplicate-name — the shape §3.5b's draft used, named here so it cannot come back; assert a keyword-less { maxOrder = 2; } cell is read; assert a seen-but-unreadable carrier yields provenance and never a default; assert the package doc string's count word matches the definition count. CHANGE test/unit/claims.test.ts — widen SUBJECT with machines?|designs?|state machines?|runs? (measured: 0 additional hits on all three subject-scoped forms that ship today); add the negativeIsTheClaim?: true field to the RESERVED_FORMS entry shape and change the negated(before, m[0]) call site to skip the in-span defusal for those entries, keeping the look-back half for every form (§2.6 — without this, no cut set, no simulation relation and not covered cannot be reserved at all: measured 0 hits each); then add the five scoped forms of §2.6's table — not the bare phrases the draft promised. The scoping is the decision this commit records, and the measurement is why. Executed against the tree with the negated() change in place, the bare phrases read no cut set 23, not covered 3, recoverable 2, no simulation relation 0 — 28 violations on landing, nine of the 23 inside src/semantics/fault-tree.ts and two of those the command's own honest bounded verdict strings at /. The five forms that ship instead are subject- or shape-scoped, carry two allowances between them (/up to order/i, /over the common labels/i), and are measured at 0 pre-existing hits each; the bare-phrase counts and the file list go in the commit message as the record of what was scoped away and why. CHANGE docs/CONFORMANCE.md §8.6. Tests: the above, plus: a definition added to the package with no reader still round-trips; "Four definitions" going to five is a red test, not a review catch; each of the five new forms asserted at 0 hits over the tree AND asserted to fire on its planted sentence — the pairs of §2.6's table, both halves executed, including the three the guard must leave alone (CONFORMANCE.md's "what is and is not covered", analytics.ts's "recoverable from", and fault-tree.ts's bounded no cut set); and the widened SUBJECT asserted to cost 0 additional hits on the three existing subject-scoped forms, the way the GAP widening was. Gate proves: both compatibility commitments (commits 17, 22) and every new verdict sentence land against guards that already exist and that actually fire — this is the commit where the plan's coverage claim in §5(c) becomes true rather than assumed, in the narrowed and honest form §2.6 states: the guard reserves the prose sentence a reader would quote, and the verdict strings themselves are pinned by mechanism (b). Guards moved: negated()'s behaviour for forms flagged negativeIsTheClaim — a deliberate widening of the guard, with the bare-phrase hit counts (23 / 3 / 2 / 0) and the scoping decision in the commit message. No definition and no feature is added here. Note for commits 17 and 22: the library text has three sites that move together, not two — the export, semantics.keywords.test.ts's round-trip, and the verbatim paste in docs/USER-GUIDE.md that user-guide.test.ts pins with the message "paste the export, do not retype it". Depends on: 0

Commit 5 — fix(cli): every command a refusal names exists Status (measured at 510793c, 2026-09-16): 8ea181d. Files: CHANGE src/semantics/fault-tree.ts behaviourLaneRefusal — the pointer names check-behaviour … --pattern, which exists, instead of --from-keywords, which does not. CHANGE test/campaign/verification.test.ts, which is not optional and which the draft's "Files: fault-tree.ts alone / Guards moved: none" would have discovered on landing: that line reads expect(withCommand).toContain('check-behaviour <file> --element P::FlightModes --from-keywords');, driven from behaviourLaneRefusal('P::FlightModes', 'check-behaviour') in the case above it, and the substring is composed at fault-tree.ts. Replacing --from-keywords with --pattern makes that toContain fail, so the one commit in lane A whose entire purpose is proving the tool never names a command that does not exist would land red on the very assertion that recorded the defect. Tests: NEW assertion, and it is the point of the commit: every command any refusal message names resolves through findCommand, and every flag it names is in that command's spec row. That kills the class, not the instance. Plus the one-line re-record above; the rest of the surrounding it(...) is unaffected and stays green unchanged — it also asserts findCommand('check-behaviour') is defined and that withCommand.startsWith(fallback), and both survive the edit, so exactly one line moves. Gate proves: the tool does not send a user to a command that does not exist. Commit 21 deletes the refusal entirely. Guards moved: test/campaign/verification.test.ts — a deliberate re-record, --from-keywords → --pattern, with the reason in the diff. Nothing else. Depends on: 0

Lane B — the guarantee class

Commit 6 — feat(behaviour): cover — an existential reachability property with a witness — §3.1 Status (measured at 510793c, 2026-09-16): b97f391. Files: CHANGE patterns.ts (PatternClass += 'guarantee'; PATTERNS += cover before existence; PropertyClaim → six words; monitorStep += one case; the verdict tail ; PropertyVerdict += machineConfigs, because base sets configs: found.configs unconditionally and no row may publish two unlabelled counts; the findings loop — a dedicated not-covered branch under --cover-required emitting at severity: 'error', mirroring --strict-vacuity's own branch, because the loop's own severity: expression derives it from the CLAIM and a not-covered row is not fail; counts; exitCode; the §2.4(a) and §2.4(c) constants). CHANGE src/api/verification.ts — add verification/cover-required to VERIFICATION_ERROR_CODES, or diagnostic-codes.test.ts's set equality goes red on landing. CHANGE sysprose-spec.ts (PATTERN_NAMES, --cover-required, BEHAVIOUR_EXIT_CODES — the 0-row rewrite AND the 2-row clause, both quoted in §2.1, the --pattern help row, **and CommandSpec.question, today "Does this safety pattern hold on every reachable configuration?", which after this commit is false: it becomes "Does this behaviour pattern hold on every reachable configuration, and can this design reach the situation I name?"**), scripts/sysprose.ts (judgeBehaviour, the summary line, **the four-words sentence at **), src/text/langium/diagnostic-codes.ts (+ verification/not-covered info, verification/cover-required error, **and an amendment to verification/malformed-property's published when, which enumerates its causes exhaustively and spells the catalogue as six pattern names — "a pattern outside the catalogue (absence, universality, bounded-existence, precedence, existence, response) …". The moment cover is in the catalogue that parenthesis is wrong, and a user who mistypes a field on a cover property reads in the generated DIAGNOSTIC-CODES.md that cover is a pattern outside the catalogue — plus the hint beside it telling them to write pattern=absence. The when sources its pattern list from PATTERNS rather than spelling names, and the hint follows**), publishable.ts (register A5 and witness row W1), src/api/index.ts; REGEN CLI-REFERENCE.md (the question renders twice — the per-command headline at gen-cli-reference.ts and the summary table at ), DIAGNOSTIC-CODES.md; CHANGE CONFORMANCE.md (and the forward-compat row for the persisted pattern = "cover" value), docs/USER-GUIDE.md — the pattern table with its Decided here? column, and, in a different guide section, the transcript line carrying the four-words sentence verbatim ("…pass, fail, vacuous, inconclusive are the four words this command reaches"), which becomes a false transcript the moment covered/not covered exist and which no gate protects; both are found by grepping the guide for the sentence, not by line. docs/04-formal-verification-plan.md — the ONE copy of the CommandSpec.question string it carries (measured at dc6662c: grep -n 'Does this safety pattern hold on every reachable configuration' returns exactly four sites outside the spec — docs/CLI-REFERENCE.md twice, both generated and both covered by the REGEN; docs/04; and README.md. An earlier revision also listed two other docs/04 positions, which carry the safety-pattern list and a Files: line and not the question, so the "fourth copy" arithmetic double-counted) — edited beside the others, or declared in commit 0's docs/04 correction as a historical record; silence is what leaves it wrong. AGENT-AUTHORING-CAMPAIGN.md's two copies of the refusal, README.md's capability row, which hand-copies the same question string. And THREE docstrings inside patterns.ts, a file already in this list, which are where the old arity and the old question survive an edit to the code beneath them: "The four words this command may reach" directly above PropertyClaim; "Does this safety pattern hold on every reachable configuration (plan §3.8)?" above behaviourReport; and /** The six patterns, split by what a bad-prefix search can decide. */ above PATTERNS, which an earlier revision left unnamed while naming the other two. None of the three reddens a gate, which is why a Files-list-driven implementation leaves them. Tests: the §3.1 list in full, including the polarity regression, the counts-sum guard, the bound frontier asserted from both sides (--max-configs <depth> keeps covered, <depth−1> gives inconclusive — measured, a witness at depth d needs maxConfigs ≥ d), the two-dwell fixture (walk-admits wording, never a bare covered) and the row-1 disjunction fixture — both ModelFactory-built and driven through checkProperty in-process, never through argv, because accept after(n) is a parse error (correction 22) — the unset-guard fixture (correction 23: the store named on the not covered line, and --cover-required refusing to spend the 1, asserted exit 2), and the emitted-severity assertion the plan assumed existed: for every diagnostic any behaviour fixture emits, severity equals the catalogue's severity for its code — with a --cover-required run asserted to print error verification/cover-required and not info. Plus npm run codes green with the amended when, and a test asserting the when names no pattern the catalogue does not contain. Gate proves: a positive reachability intent gets a claim word, a witness and an exit code of its own; its negative answer is decided rather than undecided; it does not spend the 1 unless asked; and exit 0 still means what the command's own --help says it means. Guards moved: DIAGNOSTIC_CODES.length +2 (npm run codes regenerates the figure; no absolute count is written here, per the standing rule) · in test/unit/cli-reference.test.ts: the PATTERN_NAMES ORDER assertion, the per-command byte-pin, the every-question-verbatim assertion, and the BEHAVIOUR_EXIT_CODES block for the 0-row and 2-row edits. NOT the liveness-pair guard — expect(PATTERNS.filter(p => p.kind === 'liveness').map(p => p.name)).toEqual(PATTERN_NAMES.slice(-2)), whose message is "the liveness pair moved": inserting cover before existence keeps [existence, response] as the last two, so it stays green by construction. It belongs in an asserted unchanged line and is named here as one, because that guard is the whole reason cover inserts where it does · diagnostic-codes.test.ts's error-set equality · CONFORMANCE.md's "four words" · README.md · every check-behaviour transcript. Not COMMANDS.length, not RULES.length. Depends on: 1, 2, 3, 4. Correction 2's finding survives and is narrowed to what it actually measured: cover reads no successor relation — search does its own product walk and never touches ExploreResult.successors, so this commit ships off the spine and not off P's graph. But the exactness gate's producers include ExploreResult.timedTransitions, which commit 2 adds and commit 3 wires into walkIsExact (ExploreResult.undeterminedGuards, the other producer this feature's rows lean on, already ships — c929278), and §3.1's covered rows and W1 both read relationIsTheMachines. The draft's explicitly not 2 was written before the gate existed and was never updated: at commit 6 alone walk.timedTransitions is a type error and Exactness is unwired, so an implementer following the dependency line drops the conjunct and the first affirmative claim this lane ever publishes ships ungated — on the two-dwell machine, cover (state B) prints covered — witness trace of 1 step(s), a run this semantics admits at exit 0, which is verbatim the sentence the MUST-NEVER list bans. The dependency moves; the feature does not.

Commit 7 — feat(behaviour): guaranteed vs potential on a refutation — §3.R Status (measured at 510793c, 2026-09-16): 0872666, landed after 8. Files: CHANGE patterns.ts (one PropertyVerdict field; ~35 lines at the fail block, reading walk and scc.ts; the nine-row dispatch of §3.R in its stated order, including the expression refusal at row 4, the trigger/dwell split at rows 5–6 and the store refusal at row 7 — rows 1, 5, 6 and 7 are one Exactness.failedClause switch and not four bespoke conditions), scripts/sysprose.ts (one clause plus the §2.4(d) simulator sentence on rows 8 and 9), publishable.ts (register A8 with walkRequires: 'walkIsExact', and witness row W3 with kind: 'maximality' and walkRequires: 'walkIsExact' — potential names a cycle with no exit, which is an absence wearing a witness's clothes, and the draft registered nothing for it), CONFORMANCE.md §8.5. Tests: the §3.R four machines including the latch regression, the cycle-not-tie-break assertion, the expression-atom refusal with potential — some run avoids it: the cycle … named as the wrong answer, the factory-built dwell-cycle fixture ⇒ row 6 with FairnessAssumption asserted absent from the string, the trapguard .sysml fixture ⇒ row 7, driven through argv and in-process, with potential — some run avoids it: the cycle degradedA → degradedB → degradedA named as the wrong answer and both its literal variants asserting the modality is decided, = true and = false alike, the row-precedence test (a machine satisfying rows 5, 6, 7 and 8 at once asserts row 5), and byte-identity of claim/code/severity/witness/exit with and without the field. Gate proves: neither modality value is ever made from a partial walk, from a triggered machine, from a dwell the walk over-approximates, from a guard the walk read as false because nobody bound the attribute, from an atom the walk cannot observe, or from the simulator's tie-break — and the two values are gated together and by one predicate, which the draft did for the universal one only and with its own conjunction. Guards moved: none. Depends on: 3, 4

Lane C — recovery

Commit 8 — feat(reach): report configurations no run leaves — §3.2a Status (measured at 510793c, 2026-09-16): faf61e1. Files: CHANGE explore.ts (MachineReach += traps, gated on walkIsExact — NOT on the publishable the unreachable and dead lists use, which is decreasingOk and which register row A6, polarity increasing, may not read; the three exemptions reusing recordDeadlock's predicates verbatim; reachReport emits the row; BEHAVIOUR_CODES and BEHAVIOUR_WARNING_CODES each += one member), src/text/langium/diagnostic-codes.ts (+ verification/unrecoverable-mode, warning), scripts/sysprose.ts machineLines, publishable.ts (register A6 with polarity increasing and walkRequires: 'walkIsExact', and witness row W2 for the trap's entry path — kind: 'existential', ridesOn: 'A6'), src/api/index.ts, README.md, docs/USER-GUIDE.md's reach walkthrough including its hand-pasted transcript, found by grepping the guide for configuration(s) explored, CONFORMANCE.md; REGEN DIAGNOSTIC-CODES.md. src/api/verification.ts is not needed here — VERIFICATION_WARNING_CODES is fed from BEHAVIOUR_WARNING_CODES, which this commit already edits; that is why this commit gets it right and 6, 13 and 18 have to be told. Tests: the §3.2a list. The four exemption tests are half the commit: the mission DAG produces no row and prints the no-trap sentence byte-identically naming 1 ending exempted, the sink produces verification/deadlock and the same sentence naming 1 deadlock exempted, in one output, which is the self-contradiction the draft's wording would have shipped, all three shipped machines are silent with cli.sysprose.test.ts's exact array unchanged. The three gate fixtures are the other half, one per mechanism, and two of them are ordinary .sysml files (§3.2a): the preempted-dwell machine — ModelFactory-built, driven through reachReport in-process, no .sysml file and no argv (correction 22) — suppresses the list on clause (b) with recoverable/no-trap named as the wrong answer; the latch file (transition locked accept unlatch then nominal;, measured alphabet unlatch, one whole-graph SCC, rc=0 with no findings today) suppresses it on clause (c) with no component of this walk is inescapable beyond its endings … 1 whole-graph component was exempted named as the wrong answer; the trapguard file (attribute resetOk : Boolean;, re-measured at dc6662c as 3 of 4 transition(s) fired, dead withheld, undetermined under {…} — 1 guard(s) the walk could not evaluate, rc=0) suppresses it on clause (d) with trap — 2 configuration(s) form a set nothing leaves: {degradedA, degradedB} named as the wrong answer; its = false variant asserts the trap row IS published (measured 3 of 4 transition(s) fired, 1 dead, exhaustive under {…} — the guard is present and decided, so the gate holds and the component is a genuine bottom SCC); and its = true variant asserts the exemption-3 no-trap sentence, because with the escape edge retained the relation is one SCC containing the opening. Putting = true in the positive slot — which an earlier revision did — lands this test red and invites weakening exemption 3. The draft's second positive fixture is deleted, deliberately: the latch machine was listed as "one trap naming {locked}" and is now a refusal, which is the feature's real narrowing and is recorded in the commit message rather than absorbed. Gate proves: condition (2) is answered where it has an answer, and an ending, a deadlock, a whole-graph component, a bound, a dwell, a trigger nobody may send, and a guard nobody bound each produce no trap row — the last three by one predicate rather than three conditions. Guards moved: test/unit/semantics.mc.reach.test.ts's code-set guard, it('names the seven codes this engine can raise') — an exact sorted array holding SEVEN entries at dc6662c (c929278 added verification/guard-undetermined), which goes to EIGHT, and the it(...) TITLE STRING moves with it. An earlier revision said six → seven and pointed at the profile-provenance loop above it, which has no code list in it; following that line an implementer edits the wrong block and then writes a seven-element array where eight are required, and npm test reddens on this commit's own gate. explore.ts's docstring above BEHAVIOUR_WARNING_CODES — "The five this engine raises as WARNINGS, and none of the seven as an error" — becomes six of eight and is in the Files: list for it. · diagnostic-codes.test.ts warning-set equality · DIAGNOSTIC_CODES.length +1 (delta, not an absolute: this commit's own dependency line is 3, 4, so the base depends on whether lane B ran first) · the USER-GUIDE transcript added to the claims list. Depends on: 3, 4

Commit 9 — feat(behaviour): the recovery pattern — §3.2b Status (measured at 510793c, 2026-09-16): 510793c. Files: CHANGE patterns.ts (PatternClass += 'branching'; one PATTERNS entry before existence; **a third dispatch arm placed AFTER the unsupported-construct refusal — the block that refuses when walk.unsupported.length > 0 — and BEFORE the const found = search(…) call; by anchor, never by number — an earlier revision pointed at a line that holds a COMMENT, two lines above the const walk = exploreMachine(…) call, and an arm placed there would have no walk at all; plus the atom-kind gate: state and node accepted, trigger/fires/expression refused as verification/malformed-property; and p read through atomHolds's own selection — configStates[i].includes(p) for state, configLeaves[i] === p for node — never one hand-written predicate for both, which measured flips both the verdict and the exit code on any composite state (§3.2b)), sysprose-spec.ts (PATTERN_NAMES, the --pattern help; re-check CommandSpec.question — commit 6's replacement already covers the branching case, and a test asserts it did not need a second edit), publishable.ts (register A7 with polarity increasing, walkRequires: 'walkIsExact' and an empty alsoRequires — no product-search condition, which the gate has no field for, so Publishability.searchComplete is absent rather than false), src/text/langium/diagnostic-codes.ts — verification/malformed-property's published when enumerates its causes exhaustively, and a well-formed pattern=recovery, scope=globally, p=fires T is none of them; the entry gains the atom-kind cause ("…or a p whose atom kind this pattern cannot observe") on top of commit 6's pattern-list amendment, USER-GUIDE.md, CONFORMANCE.md §8.5 (and the forward-compat row for the persisted pattern = "recovery" value); REGEN both generated docs, npm run codes included. Tests: the §3.2b list. The dispatch test is the one that matters: a recovery row never reaches search, asserted by a spy, plus a fixture with an unsupported construct asserting the unsupported refusal wins and the recovery arm is never entered. Plus the 4-vs-2 test, the reflexivity test, the composite PAIR — p = state degraded matches every configuration inside it and p = node degraded matches none, both asserted against atomHolds on every configuration of the same walk, with the shipped absence answers (node degraded PASS / state degraded FAIL, measured today) asserted in the same test; recovery p = node degraded answering recoverable at exit 0 is named as the wrong answer, the unreachable-p test asserting fail and not vacuous, searchComplete asserted absent on a recoverable row, the three atom-kind refusals each asserting verification/malformed-property and never verification/refuted, with the expression reason asserted byte-identical to §3.R's row 4, and the three gate fixtures, one per mechanism, each with its wrong answer named: the preempted-dwell machine (factory-built, in-process, correction 22) ⇒ the time row, never recoverable; the latch .sysml file with p = state nominal ⇒ the environment row, with recoverable, exit 0 named as the wrong answer (measured: the draft's A7 held on that walk and published it); the trapguard .sysml file with p = state nominal ⇒ the store row, with not recoverable: 2 configuration(s) cannot reach \state nominal`, verification/refuted`, exit 1 named as the wrong answer — the one whose wrong answer is a refutation, and the reason the arm gates both directions. Gate proves: a branching-time question is answered by a branching-time algorithm, at the one position in checkProperty where the walk exists and the unsupported clause of seenWhole has been enforced; p is read through the same observation function absence reads it through, so one atom never means two things inside one command; the two numbers of §3.2 are never printed under each other's question; no atom kind the engine cannot observe can earn exit 1; and neither direction of the claim is made over a relation that is not the machine's. Guards moved: PATTERN_NAMES order, the liveness-pair guard, the catalogue prose in four documents, and verification/malformed-property's generated entry in docs/DIAGNOSTIC-CODES.md. No new catalogue ENTRY — verification/malformed-property, verification/refuted and verification/bound-exhausted all ship today, so DIAGNOSTIC_CODES.length does not move — but the draft's flat "no new code" was wrong about the file: an entry's published when is a contract a user reads after a refusal, and this commit adds a cause to it. src/text/langium/diagnostic-codes.ts and npm run codes are in the Files list for that reason. Depends on: 6, 8

Checkpoint A. The behaviour lane now answers can it?, can it get back? and every run or some run? Re-read the cover atom/scope census and the trap census with the user before anything else in this lane is built, and decide whether --cover-required should be default-on for a cover over an #exceptional state.

Lane D — the proof footprint

Commit 10 — feat(verify): --why prints the axioms z3's core named — §3.3a Status (measured at 510793c, 2026-09-16): 863ac05, one hash with commit 4. Files: CHANGE smt.ts (SmtJudgement += core, sorted through coreSentence; the proved return reads negation.core, the field the verify path already has in hand and discards), api/verification.ts (ObligationVerdict), sysprose-spec.ts (--why on verify), scripts/sysprose.ts, src/api/index.ts, USER-GUIDE.md, CONFORMANCE.md; REGEN CLI-REFERENCE.md. No schema change (§3.3a). Tests: the §3.3a list, including the six-label core with the side: member deduped, the uav-power-budget 24 → 9 narrowing, the three-reasons fixture, and two-process byte-stability. Three proved fixture details re-recorded. Gate proves: the value the verify path has had in hand since the lane shipped reaches a reader, with the two things that make it honest — the side condition kept, and the sufficiency caveat printed. Guards moved: three verification goldens · CLI-REFERENCE.md. Not the evidence schema. Depends on: 0

Commit 11 — feat(evidence): staleness scoped to the core, the footprint and the axiom set — §3.3b · gated on 10's census Status (measured at 510793c, 2026-09-16): 3ec6c01 — the gate opened: {modelAxioms 10, footprintAxioms, scriptAxioms, coreAxioms} = (4,4,4) (5,5,1) (1,1,1) (6,6,1) (6,6,1) (2,2,1) over six proved rows — Σ footprint 24 → Σ core 9. Files: CHANGE api/evidence.ts (a keyed per-element canonical export against the narrowing comment at ; optional core and digest fields on EvidenceRecord), docs/schemas/evidence-record.schema.json (optional properties; schema const unchanged), src/validation/rules.ts (staleEvidence, its message, and the five per-record census booleans {wholeModelMoved, coreMoved, footprintMembershipMoved, axiomSetMoved, premisesMoved} inside the check payload), ADD footprintOf(model, obligation) — the model-level read-closure part (ii) actually needs, exported from src/api/index.ts. ADD the part-(iv) premise digest — a canonical digest over the obligation's premise rows, the ones premisesByRequirement (smt.ts) hands STEP 2. It is per-requirement, so unlike (iii) it does not fire on every numeric edit anywhere, and it is the only one of the four that reaches the check separating proved from vacuous: measured, assume constraint { fc.supplyVoltage >= 20.0 [V] } → >= 200.0 [V] on uav-power-budget moves the obligation from proved to vacuous while moving no axiom, no core member and no symbol — so under the three-part design the stored evidence reads current within this proof's scope over a proof the tool itself now calls vacuous. NOT smt.ts: the draft's "export relevantAxioms" gives rules.ts nothing constructible — the function is typed over EncodedRow (, not exported) and encodeRow (, not exported), and exporting those would run the encode pipeline synchronously inside ValidationRule.run on every npm run check and pull the SMT encoder into the browser bundle through src/ui/store.ts's reach into RULES. CHANGE USER-GUIDE.md, CONFORMANCE.md. Tests: the §3.3b list, including the STEP-0 case (powerCap ⇒ MassRequirement stale, not current), the STEP-2 case (supplyVoltage >= 200.0 [V] ⇒ stale via (iv) where (i), (ii) and (iii) all read current, asserted in the same run as the obligation going vacuous; current within this proof's scope is named as the wrong answer), the no-core fallback, footprintOf asserted set-equal to relevantAxioms' membership on all 38 verification fixtures, and the five census booleans asserted on one run of each sweep member — the goldens are the pre-build measurement, the census is the instrumentation, and §5's row is corrected to the per-record form because a "rate over edits" cannot be a field in a payload that sees one model version. The uav-power-budget sweep goes from 8 edits to 9, the ninth being the premise edit. api.evidence.test.ts and the L8 stale fixture re-recorded, deliberately. Sweeps batched across processes. Gate proves: a proof survives an edit that provably cannot affect it, and does not survive one that voids it through a mechanism the core does not see. Guards moved: the evidence schema — a one-directional forward incompatibility, stated in the commit message and in CONFORMANCE.md. RULES.length stays 25. Depends on: 10

Lane E — inheritance

Commit 12 — feat(contracts): disclose an inherited clause, and count who writes one — §3.4a Status (measured at 510793c, 2026-09-16): c6b46ab — clauseInheritance on uav-isr {contractsWithInheritedClauses 0, byEdgeKind {Subclassification 0, FeatureTyping 0}, namedClausesMasked 0, anonymousClausesInherited 0}. Files: CHANGE contracts.ts and its ContractClause interface, scripts/sysprose.ts, diagram/contracts-table.ts, ui/panels/ContractsTable.tsx (the one behaviour change), api/verification.ts (the census), src/api/index.ts, USER-GUIDE.md, CONFORMANCE.md. Tests: the §3.4a list; the five pinning tests green and unchanged; the census reads 0 on all six examples and every corpus file. Plus npm run test:e2e. Gate proves: a reader shown two clauses having written one sees where the second came from, and nothing enters the worklist — no digest, no evidence record, no obligation, and zero of 120 goldens move. Depends on: 0

Commit 13 — feat(refine): --via specialize — §3.4b · gated on 12's census by Subclassification Status (measured at 510793c, 2026-09-16): HELD — 12's census reads 0 on all six examples and the corpus. Files: CHANGE refinement.ts (a specialize arm over origin === 'declared' clauses, gated on the edge kind), contracts.ts, scripts/sysprose.ts, sysprose-spec.ts, diagnostic-codes.ts (+ verification/specialization-weakens, error), src/api/verification.ts — add the new code to VERIFICATION_ERROR_CODES, or diagnostic-codes.test.ts goes red on landing; REGEN both generated docs. REFINE_EXIT_CODES does not move here (§3.4b) — every verdict lands in a bucket that exists. Tests: the §3.4b list, including no obligationDigest moves, the FeatureTyping apply-shape filing exactly one obligation, and the anonymous-clause case printing the could-not-have-been-detected sentence. Guards moved: the --via family pins at cli-reference.test.ts and cli.sysprose.test.ts, whose name says "the four families" · diagnostic-codes.test.ts's error-set equality · DIAGNOSTIC_CODES.length +1 (delta). Depends on: 12

Lane F — signature

Commit 14 — feat(connectivity): --signature, and the measurement that would justify more — §3.7a Status (measured at 510793c, 2026-09-16): 570d077 — census.signature on uav-isr partsWithBoundaryPortsAndInternalParts 0 (parts 14, sameOwnerPortRelations 0, directedFeaturesInPortDefs 0, partsOwningBehaviour 0, userItemFlows 0, nonLibraryBindingClasses 0, connectorKindsOutsideTheWalk [BindingConnector, ItemFlow], connectionsBetweenCountedPorts 9, portGraphAcyclic true). Files: CHANGE analytics.ts (the census, reading direction through portFacets only), rules-connection.ts (export portFacets), sysprose-spec.ts (one flag; backedBy → the two-function form), scripts/sysprose.ts, src/api/index.ts, README.md (the In-process cell), CONFORMANCE.md (conditions 3 and 4 declared not transposed; the measured half of the dependency-template sentence only — the SPARK DERIVES contrast does NOT ship into the conformance record, because its sole warrant is docs/05 §5 item 5, a page its own author did not open, and CONFORMANCE is the doc readers treat as measured; see §3.7b; the per-port vs per-feature reading declared as this tool's); REGEN CLI-REFERENCE.md. Tests: the §3.7a list — the four docs-counts figures and the --json key list unchanged, the census pinned on all six examples, the constraint parameters labelled as parameters, the inout port counted once each way, and the post-c37eb00 baseline asserted rather than the defect re-reported: unconnectedPortUsages empty on examples/vehicle.sysml, every declared port is wired never printed in the same output as an unconnected port usages block on any example, and uav-isr's 15 port(s), 9 connection(s), 14 connected, 1 unconnected first line byte-identical. Gate proves: the question is measured before it is answered, and the one remaining defect in connectivity's own inventory — the CONNECTION_KINDS/CONNECTOR_KINDS 8-vs-10 delta — is surfaced as a census row rather than inherited. The other, the three false danglers, is not this commit's to surface: it printed on the default text path with no flag, so a --json census row would have left connectivity contradicting itself on a shipped example, and it is fixed ahead of this lane as c37eb00 (§0.1) with this commit asserting its baseline. Depends on: 0. The c37eb00 inventory is a PRECONDITION, not a dependency, and it is already met (§0.1): the census is measured on the normalised inventory, and a commit 14 built on the pre-c37eb00 tree would pin three numbers that changed underneath it. Re-verify before writing the fixture — connectivity examples/vehicle.sysml must print 0 unconnected and no unconnected port usages block — rather than taking this line's word for it.

Commit 15 — feat(connectivity): conditions 1 and 2 — §3.7b · gated; measured 1 and degenerate today Status (measured at 510793c, 2026-09-16): HELD — 14's census: 0 on uav-isr, degenerate on vehicle.sysml. Files: CHANGE analytics.ts, scripts/sysprose.ts, diagnostic-codes.ts (+ verification/signature-disagreement, info), CONFORMANCE.md. Never src/validation/rules.ts. Tests: the structural-only line on every verdict; the inout self-dependency excluded in both directions; a bare connect never read as value flow, asserted against refine's census on the same nine edges; and the vehicle.sysml regression asserted against the c37eb00 enumeration — no condition-2 finding on the three ports that were false danglers, plus unreconciledPorts empty, which is a property of the normalised inventory this commit builds on and not something this commit's own Files list produces (§3.7b). Depends on: 14. As with 14, the c37eb00 inventory is a met precondition and not an unbuilt dependency (§0.1): condition 2 is computed off portOccurrences and inherits that enumeration verbatim, so its fixture asserts the fixed baseline rather than the absence of a defect.

Lane G — liveness

Commit 16 — feat(behaviour): a finite-run semantics, and liveness on an acyclic graph — §3.5a · gated on commit 3's census (0 of 3 today) Status (measured at 510793c, 2026-09-16): HELD — exactness.acyclic false on 3 of 3 shipped machines (edges 5 / 4 / 2, walkIsExact true, failedClause null, alphabet 0, timedTransitions 0, undeterminedGuards 0). Files: CHANGE patterns.ts (move the class check out of its position ahead of the walk and down to below the const walk = exploreMachine(…) call and below the unsupported-construct refusal that guards it — by anchor, never by number — an earlier revision named a line that holds a comment; the six verdict branches of §3.5a's dispatch, in its stated order, including the trigger/dwell split at rows 2–3 and the store refusal at row 3b, which the draft had no row for; the seventh semantic-profile field, named run classes and defining BOTH of them), src/semantics/mc/profile.ts, publishable.ts (register A10 — polarity decreasing in edges, walkRequires: 'walkIsExact' with alsoRequires: ['acyclic === true'], and the "decreasing row reading the gate" justification in its Otherwise cell so the reflection test does not read it as a mis-wiring — and witness row W4 for the fail, kind: 'maximality', walkRequires: 'walkIsExact', alsoRequires: ['acyclic === true']. W4 reads the WHOLE gate and W1 reads only the relation half because a refutation of F p asserts the witness run has no successors, which a bound and an undecided guard both manufacture, while a bound can only ever hide the existential witness W1 publishes. Writing a numbered publishability condition into this row — which an earlier revision did — reddens §5(a)'s reflection test on this commit's own edit, since walkRequires admits exactly four values and no numbered one is among them), sysprose-spec.ts and BEHAVIOUR_EXIT_CODES — the second pair of edits: the 0 row gains the maximal-run shape, the 2 row's liveness clause narrows (§2.1), and the nine documents quoting the refusal, plus docs/CONFORMANCE.md's two prose statements of the profile's arity (six-field → seven-field), which are protected by no test at all and were in neither list; REGEN CLI-REFERENCE.md, DIAGNOSTIC-CODES.md. And the seventh profile field moves reach, not only check-behaviour — SEMANTIC_PROFILE is one constant rendered from patterns.ts AND explore.ts. Three exact six-element arrays become the same seven-element array ending …, 'time', 'run classes': in test/campaign/cli.sysprose.test.ts the body.reach.profile.map((f) => f.field) array and the body.behaviour.profile.map((f) => f.field) array — two different it(…)s, found by those expressions — and in test/unit/semantics.mc.reach.test.ts the r.profile.map((f) => f.field) array inside it('carries the semantic profile on the report'). The guide's "names six things" prose goes to seven with the new item spelled out. All four are deliberate re-records with the reason in the diff, and this commit says out loud that a liveness commit changes reach's published payload. Tests: the §3.5a list, including the final-state variant with no deadlock clause, the triggered variant refused at row 2, the factory-built dwell variant refused at row 3 with FairnessAssumption asserted absent, the factory-built after(5) → done before after(60) → stuck machine asserting row 3 and NOT fail — the W4 regression, with refuted — finite maximal run of 1 step(s) at exit 1 named as the wrong answer, the refusal text asserted byte-identically on every cyclic machine in the corpus, every verdict line asserted to name its run class, and cli-reference.test.ts asserting both contract-row edits. Plus test/unit/semantics.mc.patterns.test.ts over buildChain() — the already-passing test this move flips, with §3.5a's table as the record of what changes and what does not: the two v.detail assertions re-recorded to toContain('names triggers') and toContain('FairnessAssumption') — found by their present text, 'liveness not checked in-process' and 'fairness' — and the v.claim, both v.code, v.patternClass, v.configs and v.exhaustive assertions asserted UNCHANGED, because configs/exhaustive are the product-search fields and a refused liveness row still runs no product search. Gate proves: liveness is decided only where every run is finite and the environment is not a party to the claim; the refusal is unchanged everywhere else; and the exit contract says what the verdict established rather than what the safety lane established. Guards moved: nine doc quotations · BEHAVIOUR_EXIT_CODES' 0 and 2 rows (second edit; the first was commit 6) · the verification/behaviour-unsupported-construct catalogue entry's meaning, whose "not lowerable" promise must survive · the three exact semantic-profile arrays, six elements → seven — the two profile.map((f) => f.field) arrays in cli.sysprose.test.ts and the one in semantics.mc.reach.test.ts's it('carries the semantic profile on the report'), each found by its expression · the guide's "names six things" prose · docs/CONFORMANCE.md's two prose statements of the profile's arity — "every verdict it prints carries the six-field semantic profile" and, in the behaviour lane's conformance record, "every verdict prints the six-field profile it holds under" — both false after this commit, both absent from the draft's list, and neither protected by any test or docs-counts claim, which is exactly why a Guards-moved list is where they have to appear. The second of the two also names the run-class distinction the way the other profile facets are named there. Optionally, and recommended, a docs-counts CLAIM /carries the (\S+)-field semantic profile/ mapped to SEMANTIC_PROFILE.length spelled as a word, so the next field addition is a red test rather than a review catch — which is the discipline every other count in this plan already has · semantics.mc.patterns.test.ts's two v.detail assertions on the buildChain() liveness loop, re-recorded; the v.configs/v.exhaustive pair beside them explicitly NOT moved. Depends on: 3, 6