Formal verification for Sysprose — obligations, proofs and evidence, command line first

Summary

You get a verification lane that starts with the cheapest honest answer and only then reaches for a solver. contracts reads every requirement as the assume/guarantee pair the standard defines and the bundled library carries structurally (Requirements::RequirementCheck owns an assumptions and a constraints ConstraintUsage; the body allTrue(assumptions()) implies allTrue(constraints()) is the shipped library's wording (Systems Library/Requirements.sysml); Part 1 §9.2.14.2.8 spells it without the call parentheses — the shipped graph carries no expression for it, so contracts reads the two features, not that formula). obligations turns that into a worklist: what must be shown, over which axioms, and — the part that matters — which relations the existing unit gates refuse and why. verify --engine literal then discharges what it can with no solver installed at all, saying only "holds at the model's values". Adding z3-solver upgrades the same command to --engine smt, where a discharge means the negation came back UNSAT and a refutation comes with a witness that has been re-evaluated in-process before it is printed.

Verdicts are written back through two channels, both tool-local: a verdict string on the unbound metadata RequirementMetadata carrier this tool defines (src/semantics/requirements.ts:23), and an evidence record as §7.27 metadata in a @SysproseVerification::Evidence carrier naming the tool, its version, the bound, and a digest of the model it was computed over. The one standard slot this lane writes is @VerificationMethod { kind = analyze; } on the case. Later phases add requirement-set consistency with a named conflicting subset, compositional refinement in Cimatti's normal form, exact bounds, bounded state-machine reachability, minimal cut sets from contract-failure injection, and export/import for z3, cvc5, OCRA, nuXmv and Lean.

The order is deliberate: six commits to a running obligations + verify --engine literal on examples/uav-isr.sysml and examples/vehicle.sysml — three of them paying off prerequisite defects in the mapper, the serializer and the validation rules, and one shipping the keyword reader, before anything reads what they produce; three more to the SMT engine behind the same unit gates that checkConstraints already applies, pinned by a differential test and a relation census that together make the word "proved" safe to print. What this can say: proved (negation UNSAT under a satisfiable axiom set, non-vacuous), refuted with witness, design-admitted (a refutation obtained by freeing a value the model states), holds at the model's values, holds structurally, holds within bound, vacuous, inconclusive.

What it can never say — the MUST-NEVER list, in one place.

1. Never verified, correct, safe, deadlock-free or realizable, anywhere, about anything.
2. Never proved from a bounded run, a point evaluation, or a solver that was not installed.
3. Never proved when the axiom set was not shown satisfiable, when the solver returned unknown, or when any relation in the obligation's own body was refused by the unit gates.
4. Never proved or refuted for an obligation carrying a free variable unbounded on either side — the tool derives no domain axioms from ISQ quantity kinds and does not know that a power or a mass is non-negative, so a witness outside the physical domain is not a counterexample and the obligation is inconclusive.
5. Never refined while any obligation is undecided, and never refined when the antecedent of obligation (3) or (4) is unsatisfiable — that is vacuous.
6. Never verdict = "pass" in the file for a claim that is not proved; refuted writes fail, and every other claim writes inconclusive, with the finer claim in the evidence carrier.
7. Never "the standard's own vocabulary" for the verdict facet: RequirementMetadata occurs 0 times in the specification, and the standard's own slot — VerificationCase::verdict : VerdictKind {redefines result} — is one this tool does not bind.
8. Never a green build under --engine auto or --engine smt when the solver was absent.
9. Never a pass on a partial exploration, and never a liveness verdict without a named fairness assumption.
10. Never no cut set over a contract set whose baseline obligation was vacuous, and never absence of a single point of failure when any order-1 check was undecided.
11. Never a third-party #keyword described as standard, and never an absent annotation read as a fact.

The exit contract is stated once, exhaustively, in VERIFY_EXIT_CODES (§2), and this is the single most important design decision here: a missing solver never produces a proof, and never a green build under --engine auto or --engine smt.

1. What Sysprose has and lacks today

Measured on main @ f1cd587 (2026-09-05).

Has, and this plan builds on it:

Current counts to register against: 24 validation rules, 56 diagnostic codes, 82 fixture directories, 8 subcommands, 2 examples. The fixture figure was 81 when this plan was written and every other mention of 81 fixtures below is that plan-time reading; commit 2b adds L4-requirement-subject-inherited, and test/unit/docs-counts.test.ts holds the live count in docs/AGENT-AUTHORING-CAMPAIGN.md — this line is a baseline, so re-read it there before registering against it.

On campaign levels, corrected. test/fixtures/agent-authoring/ holds fixture levels L0–L5 only (8 / 3 / 17 / 24 / 23 / 6 = 81). L6 (invariants.test.ts), L7 (cli.test.ts, cli.sysprose.test.ts) and L9 (npm run bench) are suite levels with their own runners and no fixture directories at all. L8 is therefore a suite level, not a fixture level: this plan claims it as test/campaign/verification.test.ts, a golden-verdict runner beside L7's CLI suites. Only one L8 case belongs in the fixture corpus — L8-evidence-stale, because validation/stale-evidence is a real npm run check rule the existing harness can score. Every other verification case is a golden verdict, which the checker harness (which knows only CheckReport diagnostics) cannot produce.

Lacks:

1. No decision procedure — nothing says "unsatisfiable" or "holds for all admitted values".
2. No temporal/property language; no reachability, deadlock or invariant question on a state machine.
3. Simulation walks one deterministic path; no exhaustive exploration.
4. assume/require are parsed but never composed; no refinement check across derive/refine.
5. No requirement-set consistency, no vacuity check.
6. verification def / verify are parsed and traced but no verdict is ever computed and written back.
7. No export to external provers, no import of their results.
8. No evidence record: nothing says what was shown, by which tool, over which version of the model.
9. No generic keyword reader: a user-defined #keyword vocabulary is parsed and preserved but cannot be resolved, inventoried or reasoned about.

1.1 Four prerequisite defect families, each measured, not assumed

These are behaviour changes to shipped round-trip semantics. D1, D2 and D4 are paid off first, in their own commits, because everything downstream reads what they produce. D3 is not fixed at all — ids stay fresh per load, no commit in this plan touches src/core/ids.ts, and every digest and every SMT assertion name canonicalises to qualified names instead (commit 3). So this is three prerequisite fixes plus one worked-around defect, and the keyword reader of commit 2d is a gap (§1 Lacks item 9), not a defect payment.

• D1 — clause-body drop. mapRequirementClause (src/text/langium/map-to-model.ts:2089) reads node.kind, node.name, node.specializations and node.expr — never node.body or node.members, for any clause kind. Probed: objective { doc /* … */ assume constraint { armed == true } require constraint { altitude > 0.0 } } maps to a ConstraintUsage with attrs.requirementRole = 'objective' and zero children, and serialises as objective;. The doc, the assumption and the guarantee are destroyed, and the deletion is idempotent, so nothing downstream notices. It is wider than the nested verify the first draft reported: actor a { doc }, stakeholder h { doc } and frame f { doc } lose their bodies too, and require constraint bound { doc /* keep me */ s.x < 10.0 } loses both the doc and the constraint keyword. What goes with them is the standard's own home for a behaviour precondition and postcondition — CaseBodyItem → ObjectiveMember → ObjectiveRequirementUsage : RequirementUsage, typed by Cases::Case::obj : RequirementCheck[1].
• D2 — the serializer omits constraint. requirementClauseLine (src/text/serializer.ts:701) drops the keyword, emitting require bound { x < 10.0 } and assume { … }. Under the published grammar (spec line 12009), RequirementConstraintUsage's first alternative is an OwnedReferenceSubsetting — a reference to an existing bound, not a declaration of one — and require { … }, with neither constraint nor a #keyword, matches no alternative at all; AssertConstraintUsage is the same shape. Sysprose round-trips its own output only because its own grammar makes constraint optional — sysml.langium:285, verbatim: | kind=('require' | 'assume' | 'assert') ('constraint' | 'requirement')? (name=Name)?. (Line 282 is the actor / stakeholder / objective / frame / verify alternative, which carries no constraint at all.) This is a conformance defect in the writer, with a corpus-wide byte diff.
• D3 — fresh UUIDs on every load. src/core/ids.ts → crypto.randomUUID; verified, two loads of the same text give different ids. Any digest or named SMT assertion keyed on element ids is unstable across runs. Ids must be canonicalised to qualified names before hashing or naming.
• D4 — validation/requirement-subject fires on an inherited subject. requirement r : Def; warns even where the subject comes from the definition. It must resolve through effectiveFeatures.

D1 and D2 must not be split from each other: the round-trip test that proves either one needs the other. Together with D4's behaviour change and the vocabulary package, that is why commit 2 becomes four commits — mandatory, not stylistic.

2. The verification story

A requirement enters as prose plus an assume/require pair on a subject. It leaves as a verdict facet in the file with an evidence record beside it. Between those two points sit three engines and one agent loop.

The engines.

• Structural / SMT (z3 WASM, in-process). Decides quantifier-free arithmetic over feature values: is this requirement set satisfiable at all (unsat core when not); does this require hold for every value the model admits (negation UNSAT); what is the tightest bound on a measure. It sits behind the existing unit gates, so what z3 sees is already dimensionally sound and every relation the gates refuse is listed, never dropped.
• Contracts / composition (same solver, different obligations). Do the component contracts, together with the equalities the model actually states, entail the system contract; is every component assumption discharged by its siblings; does a derived requirement refine the one it derives from; which combinations of contract failures break the top requirement.
• Behavioural / bounded model checking (pure TS, plus optional z3 and nuXmv). Which states are reachable; which transitions can never fire; where does the simulator silently pick one of several enabled transitions; do the safety patterns hold on every reachable configuration.

The agent loop around them. contracts and obligations say what exists and what must be shown. prompts --element R surfaces the #prompt guidance the engineer wrote. property-draft returns a FRETish skeleton plus a data dictionary of every name, type and unit legal in the subject's scope. property-check refuses a clause outside the encodable fragment, or one that does not parse, does not resolve, clashes dimensionally or is trivially true on its own — and prints a back-translation with a fixed line saying the tool did not check that the clause means what the prose meant. verify --record produces the evidence; evidence-attach writes it into the file; evidence-status says which records went stale after an edit.

   requirement (doc + assume/require + subject)        #prompt guidance
              │                                              │
              ▼                                              ▼
      ┌──────────────┐                          ┌────────────────────────┐
      │  contracts   │  inventory: A, G, subject│ property-draft/-check  │
      └──────┬───────┘  satisfier, fragment     └───────────┬────────────┘
             │                                              │ gate 0 + 4 gates
             ▼                                              ▼  + back-translation
      ┌──────────────┐   the worklist: what must be shown, over which axioms,
      │ obligations  │   and which relations the unit gates refuse, with the reason
      └──────┬───────┘
             │
   ┌─────────┼──────────────┬──────────────────┬───────────────────┐
   ▼         ▼              ▼                  ▼                   ▼
┌────────┐ ┌──────────┐ ┌──────────────┐ ┌───────────────┐ ┌──────────────┐
│literal │ │ SMT (z3) │ │ consistency  │ │ contracts /   │ │ behaviour /  │
│evaluate│ │ A ∧ ¬G   │ │ + unsat core │ │ refine (nf)   │ │ explicit     │
│        │ │ UNSAT?   │ │              │ │ fault-tree    │ │ state walk   │
└───┬────┘ └────┬─────┘ └──────┬───────┘ └───────┬───────┘ └──────┬───────┘
    │           │              │                 │                │
 holds-at-   proved /      consistent /      refined /         holds-
 values      refuted       inconsistent      not refined       structurally
    │           │              │                 │                │
    └───────────┴──────┬───────┴─────────────────┴────────────────┘
                       ▼
          ┌──────────────────────────────┐
          │       evidence record        │  claim · engine · tool+version
          │   (canonical model digest)   │  bound · witness · obligation digest
          └───────────────┬──────────────┘
                          │
            ┌─────────────┴──────────────┐
            ▼                            ▼
   evidence-attach                 export ──▶ z3 · cvc5 · OCRA · nuXmv · Lean
   verdict facet (tool-local)              ◀── certificate-import
   + @SysproseVerification::Evidence           (strict parser; a bounded run
   (§7.27) in the file                          never imports as "proved")

The exit contract, stated once and exhaustively

Single-sourced in VERIFY_EXIT_CODES in scripts/lib/sysprose-spec.ts, beside EXIT_CODES:20 and CHECK_EXIT_CODES:34, with the same style of comment explaining why it is a third contract. CommandSpec gains an exitContract: 'report' | 'verify' field so renderCommandUsage and the reference generator quote the right one.

--engine auto resolves to smt when loadZ3() returns a backend, and otherwise emits verification/tool-absent for every obligation ⇒ inconclusive ⇒ exit 2. It never silently downgrades to literal. A point evaluation is only ever green when it was asked for by name.

--allow-inconclusive is scoped. It lowers 2 → 0 only for obligations that are undecided — verification/timeout and verification/unsupported-construct. It never lowers verification/tool-absent, never lowers verification/vacuous, never lowers verification/method-not-performed, never lowers design-admitted, and never wins over a violation: exit 1 beats it. The scope is stated over codes, not over prose, so every commit gate in §4 can be read against this list. The summary line still prints the inconclusive count first, and names which inconclusives were forgiven. There is no --allow-unperformed: forgiving an unjudged verification method would be a separate flag and a separate decision, and this plan does not ship one (§8 decision 1).

vacuous is an inconclusive under every exitContract: 'verify' command, and it always exits 2. That holds for verify, consistency, refine, bounds, check-behaviour and fault-tree alike — one claim word, one exit code, no per-command exception. --strict-vacuity does not change the exit code; it promotes the vacuity row from an info line to verification/vacuous-property as an error in the report and in npm run check, so a vacuity that was previously easy to scroll past becomes a finding. Vacuity is this plan's one declared deviation from the standard (§6, §8.4.17), and no flag launders it back to green.

2.1 The annotation vocabulary — what the standard already says, and the one gap this plan ships

A practitioner's four-keyword vocabulary — #precondition, #postcondition, #Exception, #Observable — was put to this plan as a possible source of proof obligations. Three of the four questions it asks are good ones. Only two of the four keywords survive contact with the specification, and only one of those ships here.

The rule this section applies. If SysML v2 already expresses a facet, the plan uses the standard construct and ships no keyword. A keyword is warranted only where the specification is silent, and then it ships exactly as #prompt does — a metadata def in a package Sysprose ships as text, plus a user-defined keyword (§7.27.1, §7.27.4). Nothing is invented, and no third-party vocabulary is ever described as standard.

Why #observable is held. A shipped metadata def that the tool writes into user files is a compatibility commitment: withdrawing it later turns a user's file into verification/keyword-names-nothing. #observable discharges no obligation — its whole output would be one info verdict and an atom filter — and nothing in this plan depends on it. So commit 2d ships the reader, the resolver and the foreign-alias table, which are what make any vocabulary legible, and ships exactly one keyword through them: #exceptional, which earns its keep because the obligation it synthesises is absence × globally, one of the four patterns the bad-prefix engine can actually decide (§3.8). #observable is revisited at Checkpoint B, when a shipped example either needs it or does not.

On preconditions for a plain behaviour, the standard has an idiom and it is not a keyword. ActionBodyItem admits no RequirementConstraintMember, so assume / require are not legal in an action def body. What the specification does instead is name an invariant: inv precondition { … } appears five times in the KerML Kernel Function Library — for example VectorFunctions: inv precondition { v.dimension == w.dimension } — and the single occurrence of the word anywhere in SysML Part 1 is the abstract-syntax constraint name positionTimePrecondition. In SysML notation that idiom is assert constraint precondition { … }, which parses in Sysprose today with zero diagnostics. The three standard answers for a behaviour precondition are therefore a named assert constraint as an axiom, a guard on the incoming transition, or a requirement whose subject is the behaviour, tied by satisfy — and contracts reads all three.

Why this changes the plan at all: the standard construct is unreadable today. That is defect family D1 (§1.1). Before commit 2a, objective { … } is silently deleted on save — which is both why no keyword is needed for BEFORE/AFTER and why nothing downstream could have read one anyway.

What the mechanism costs, measured. #precondition, #postcondition, #Exception, #Observable, a qualified #SysproseVerification::exceptional and even a misspelt #precondtion all parse with zero diagnostics on an action def, an action usage, a use case def, a state usage, a port usage and an attribute usage; each lands in attrs.metadata as written; each round-trips. A model annotated with somebody else's vocabulary is therefore already read and preserved losslessly, and nothing in this plan may break that. A plain package SysproseVerification { metadata def <exceptional> ExceptionalOutcome; } round-trips too, so STATEMENT_KIND_LIBRARY's shape is the one to copy. Do not use the SemanticMetadata shape ParametersOfInterestMetadata uses for <moe>/<mop>: :>> baseType = xs meta SysML::Usage; produces three ref/unresolved-specialization warnings today and the serializer rewrites SysML::Usage to SysML::Systems::Usage. Do not use metadata X about Y; — it does not parse. @Def { attribute … = "…"; } inside a body does round-trip, and is the carrier §3.10 depends on.

One caveat on round-tripping, corrected. The keyword round trip is idempotent from the second save, not byte-identical from arbitrary input: measured, #exceptional\n part def Abort; comes back as #exceptional part def Abort;. Every test in this plan asserts idempotence from the second save, and the interoperability ratchet (§5) is written against that, not against byte-identity.

3. Tools and features

3.0 How the table is read: subcommand names, and how a REF resolves

Subcommand names are single tokens. findCommand (scripts/lib/sysprose-spec.ts:221) matches argv[0] against COMMANDS by exact name, which is why the eight shipped names are single tokens and where-used is hyphenated. Every new row here is therefore hyphenated too — property-draft, property-check, evidence-status, evidence-attach, evidence-detach, certificate-import, check-behaviour, fault-tree — and the CLI column above quotes what a reader can actually type. Nothing in this plan adds two-token group dispatch.

How a REF resolves, stated once because six new commands take one. --element, --subject, --case and --measure all accept either a qualified name (P::uav::endurance) or a short id (R-UAV-001), resolved by the same resolver prompts --element and where-used --element already use — one resolver, extended, never a second. Resolution order: exact qualified name, then exact declaredShortName, then an exact declaredName that is unique in the model. On multiple matches the command exits 2 and prints every match with its qualified name; it never picks one. On no match it exits 2 with the nearest-name suggestions the property gates already compute. A REF naming a library element is refused. The behaviour is pinned by an L7 CLI case per new command, because six commands sharing an undefined convention is how two of them end up with different ones.

3.1 contracts — the inventory

In-process API. contractsOf(model): Contract[] and contractOf(model, reqId) in src/semantics/contracts.ts; contractReport(model) in src/api/verification.ts, alongside obligationsReport and re-exported from src/api/index.ts — it is the sibling of constraintReport (src/api/analytics.ts:1718) in shape, not in location. Each contract: {id, qualifiedName, shortId, subject:{name, typeRef}, assumptions[], guarantees[], satisfiedBy[], derivedFrom[], refinedBy[], verifiedBy[], variables:[{path, featureId, role:'input'|'output'|'parameter'|'derived', unit, siFactor}], fragment:'qf-lra'|'qf-nra'|'temporal'|'unsupported', unsupported:[{expression, reason}], keywords[]}.

The fragment rule, stated because the flagship example turns on it. fragment is qf-lra only when every relation is linear after literal substitution. Freeing any feature that appears as a divisor or inside a product promotes the obligation to qf-nra, and the report names the free variable that caused the promotion. On examples/uav-isr.sysml, freeing cruisePower makes endurance = battery.capacity * usableEnergyFraction / cruisePower a division by a variable, so the endurance obligation is QF_NRA, not QF_LRA — z3 5.0.0 rejects it outright under (set-logic QF_LRA).

Constructs read. RequirementDefinition/RequirementUsage; owned children with attrs.requirementRole ∈ {subject, assume, require, objective} and attrs.expression; case objectives — a CaseDefinition/CaseUsage, UseCaseDefinition/UseCaseUsage or VerificationCaseDefinition/VerificationCaseUsage whose objective clause carries assume/require children is a contract on a behaviour, with the subject defaulting to Case::result per Cases.sysml (subject subj default Case::result;) and bound to the case subject per VerificationCases.sysml (subject subj = VerificationCase::subj; — a binding, not a default, per §3.2's own rule) (readable only after commit 2a); Satisfy (source = part, target = requirement), Derive (source = original, target = derived), Refine, Verify (source = case, target = requirement). Port attrs.direction classifies variables as inputs vs outputs. Library rows and #prose/#prompt statements are dropped the way constraintReport does (which filters attrs.isLibrary); contracts uses the stronger isUserElement, which also drops implicit elements and elements whose owner is implicit — and the digest of §3.10 must therefore be written model.toJSONWhere((el) => isUserElement(model, el)), since toJSONWhere takes a one-argument predicate.

Where the four orientations were measured, and where they were not. Satisfy is measured on both shipped examples (examples/uav-isr.sysml:140-141, examples/vehicle.sysml:62). Neither shipped example declares a verify, a derive, a refine or an objective — examples/uav-isr.sysml contains none of them — so the Verify, Derive and Refine orientations are measured on hand-built probe models, and commit 2c re-measures each against its own case. Any statement in this document that an orientation was "measured by probe" means exactly that, and never that it was read off a model the reader has in front of them.

Written back. Nothing. New diagnostics under the single new DiagnosticSource 'verification': verification/unsupported-expression (info), verification/contract-no-guarantee (info — assumptions with nothing to prove), verification/nonstandard-clause-location (info — assume/require in an action def body, which Sysprose accepts and the standard's ActionBodyItem does not admit), verification/foreign-keyword (info), verification/keyword-names-nothing (info).

Verdict semantics. MAY say: "N contract(s) on M subject(s); K guarantee(s) in QF_LRA, J in QF_NRA, U unsupported"; and, for a requirement with prose but no constraint body, "no formal clause". MUST NEVER say satisfied, proved, consistent or anything about truth — this command reports structure. An empty inventory on a model that has requirements is stated explicitly, never rendered as zero problems. MUST NEVER present an objective assumption as a system requirement, and MUST NEVER report an objective as empty when the mapper is the reason — the pre-2a behaviour is an L8 case so it cannot regress silently.

Literature. benveniste-2015-theory (what a contract is), cofer-2012 (contracts on an architecture — target AADL/Lustre, see §7), westman-2013 (ISO 26262 safety goals and FSRs as contracts), almeida-2024 (which KerML feature/value readings are settled and which are not), omg-sysml-2.0-part1-2026 §7.20–§7.21 (the constructs themselves).

App affordance. A Contracts table view, added in the closing commit; the CLI ships first.

3.2 obligations — the worklist

In-process API. obligationsOf(model, {scopeId?}): Obligation[] in src/semantics/obligations.ts; obligationsReport(model) in src/api/verification.ts. Each obligation: {requirement, shortId, subject, role:'axiom'|'premise'|'obligation', node: ExprNode (unit literals lowered to SI), vars, sortPerVar:'Real'|'Int'|'Bool', encodable: true | {reason, detail}, nonlinear: boolean, verifiedBy[], method, evidence[], status, provenance?}.

The role map, complete. require → obligation. assume → premise. assert constraint → axiom (this maps to a ConstraintUsage with attrs.requirementRole = 'assert', not a distinct metaclass). Feature-value expressions and bind edges → axioms; a = feature value is a binding in KerML, not a default. And the row the first draft was missing: a plain constraint c { … } — no role, not assert — is an OBLIGATION, not an axiom. It is what checkConstraints judges, so it must be what the SMT engine judges, or the two surfaces cannot be compared at all. Filing it as an axiom would make one false plain constraint turn check(A) UNSAT and downgrade every genuine violation in the run to inconclusive — exit 2 by default, and exit 0 under an unscoped --allow-inconclusive.

Therefore the axiom set is exactly: feature-value bindings, bind equalities, and assert constraint bodies. Nothing else.

Encodability is the same gate the numeric surface applies, because it calls the same functions: parseRelationBody, lowerUnitLiterals, substituteLiterals, relationScope, scaleOfRelation, relationRefused, storageScaleOf, nodeDimension — today module-private in src/semantics/solver.ts at lines 385–1249, lifted in commit 1.

--from-keywords (off by default). A clause read through a foreign keyword — somebody else's #precondition or #postcondition — contributes a premise or a guarantee only under this flag. Every such row prints the keyword it came from and the words "third-party spelling; not SysML v2, not a Sysprose keyword", and the flag is recorded in the evidence record so a proof that leaned on a vocabulary Sysprose did not define cannot be replayed as though the model had said it.

This command reports storage state, never truth. open, no-formal-clause and not-encodable are structural readings; discharged and stale are read back from an attached evidence record, never computed here — discharged means a record exists whose claim is proved and whose modelVersion.graph still matches, stale means one exists and it does not. There is no vacuous row: vacuity is an SMT decision (§3.4 step (2)), and no TypeScript mechanism in this command could produce it, so claiming it here would be exactly the defect this plan exists to prevent — a verdict word its declared engine cannot decide.

--missing — defined here because §6 calls it the deliverable that measures encodability. It restricts the worklist to the obligations that have no current evidence record and no formal clause to encode — the no-formal-clause and not-encodable rows — and prints their histogram. It is the "what would this lane not decide on your model?" mode, and it needs no solver.

Written back. Nothing. This is the standard's RequirementCheck decomposition made visible.

Verdict semantics. MAY say per relation: "encodable (linear real arithmetic)", "encodable (nonlinear — NRA, may time out)", "not encodable: dT == t2 - t1 on °C is offset-scale arithmetic". MUST NEVER say anything about truth. A relation the gates refuse is listed with its reason, never omitted — the checkConstraintsNumeric rule (src/semantics/solver.ts:2447), carried forward. A requirement carrying a hand-written verdict = "pass" facet with no evidence record is reported as "claimed pass, no evidence". MUST NEVER contribute a keyword-derived premise or guarantee without printing the keyword on that line.

Literature. cofer-miller-2014 (objective-by-objective evidence), rushby-1993 ch. 2–3 (what a proof certifies, and that its assumptions must be listed with it), mavridou-2020 (verdicts mapped back to the requirements they concern), almeida-2024.

3.3 property-draft / property-check — authoring under gates

In-process API. src/api/property.ts. propertyDraft(model, reqId) emits the three mandatory FRETish fields — component, shall, response — as the encodable skeleton, plus a data dictionary from featureIdsFor(model, subjectId) (src/semantics/evaluate-model.ts:67) giving every legal name with its type, unit, dimension claim and literal value, plus every #prompt that reaches the requirement or its subject type, verbatim, plus example clause shapes generated from the dictionary. The other three fields — scope, condition, timing — are emitted as commented guidance marked fragment: temporal — not encodable by any in-process engine; export-only (§3.11), with the reason printed. mavridou-2026 is explicit that only three of the six are mandatory and that an omitted timing defaults to eventually, which is a liveness reading no engine in phases 0–3 can discharge.

propertyCheck(model, reqId, clause) runs gate 0 and then four judging gates:

• (0) encodable fragment. A clause whose scope is not global or whose timing is not the default is refused at gate 0, naming the field — verification/temporal-field-unencodable. It is not "accepted with a gap": nothing downstream can decide it.
• (1) parseExpr succeeds.
• (2) every ref path resolves in the subject scope, with nearest-name suggestions in expected.
• (3) dimensions agree via evaluateConstraintQuantityDetailed on a transient constraint over model.clone() — never on the caller's model.
• (4) syntactic non-triviality — the clause is neither valid nor unsatisfiable on its own: clause SAT and ¬clause SAT under z3, with no axioms asserted; with no solver, the gate reports "non-triviality not checked: z3 absent". Note the scope: a clause that is trivially true once the model's feature values are pinned is not caught here — uav.mtow <= 25.0 [kg] passes gate 4 even though uav.mtow = 18.5 [kg] is a literal in the file. That is what verify's tautology check (step 3) and the vacuity report are for, and the limit is recorded in the §6 limits register.

It returns a back-translation of the AST into structured English and the insertion range inside the requirement body.

Constructs read. #prompt statements via promptsFor (src/api/analytics.ts:1059), the requirement doc via requirementStatement, the subject clause, ISQ typing and unit literals, existing assume clauses.

Written back. Nothing — the tool tells, the agent edits, the existing write → npm run check → repair loop applies. Optionally the FRETish fields travel with the clause as a @SysproseVerification::Property { … } carrier (§7.27), so the structured English that produced the formula stays beside it.

Verdict semantics. MAY say: "accepted: parses, resolves 3/3 names, dimensionally consistent, non-trivial on its own"; "refused at gate 0: scope = after is temporal — no in-process engine decides it; export it (§3.11) or restate the clause globally"; "refused: endurance does not resolve in the scope of uav — did you mean uav.endurance?"; "accepted with a gap: non-triviality not checked (z3 absent)". MUST NEVER say the clause is a correct formalisation of the prose. Every report ends with the same fixed line: "meaning is not checked; read the back-translation."

Literature. mavridou-2026 + fret-fretish-semantics-2019 (the six fields, and which three are mandatory), ma-2026 (data dictionary and template before the LLM), cosler-2023 (sub-translation traceability → the back-translation, and why p/q/r/s stay separate attributes), danso-2026 (syntax is easy, semantics is hard — the gates are the answer to that bar), andresel-2026 (lightweight consistency check on generated properties), post-menzel-2011 (pattern-grammar expressiveness on industrial requirements).

App affordance. A "Draft property" action on a requirement in the Properties panel; deferred.

3.4 verify — discharge, and verification cases get a computed verdict

In-process API. verifyModel(model, opts): Promise<VerifyReport> in src/api/verification.ts, over two engines.

src/semantics/engines/literal.ts wraps checkConstraints and evaluateConstraintQuantityDetailed: it evaluates the assumptions first, so a pass is either "assumptions hold at these values" or, if an assumption is false, vacuous at values → inconclusive. checkConstraints has a third status — 'unknown' (src/semantics/evaluate-model.ts:184) — and it is neither a pass nor a fail: it maps to inconclusive: not evaluable at the model's values, exit 2. It is handled explicitly in the differential gate (§5), because it is exactly where two engines are most likely to differ and exactly the case §1's own warning is about — a constraint that silently disappears reads as one that holds.

src/semantics/engines/smt.ts runs, per obligation O with premises P under axioms A: (0) once per run, check(A) — if UNSAT, every obligation is inconclusive: axioms inconsistent (core …), because a proof from a contradiction is void; (1) check(A ∧ P ∧ ¬O) — UNSAT ⇒ proved, SAT ⇒ refuted with witness; (2) check(A ∧ P) — UNSAT ⇒ vacuous; (3) check(¬O) alone — UNSAT ⇒ tautology: true, still proved but flagged.

Free variables must be two-sided. verification/free-variable-unbounded is emitted and BLOCKING: an obligation with a free variable unbounded on either side is inconclusive: freed feature X is unbounded below/above; a witness outside the physical domain is not a counterexample, never refuted. This is not a hint. It is the rule that stops the flagship example printing a fabricated counterexample: encoded exactly as §3.2 and commit 4 specify, with cruisePower freed and only an upper premise, z3 returns sat with cruisePower = -1 W and endurance = -1843200 s, and the in-process re-evaluation gate of §5 confirms that arithmetic — so it would print as a genuine refutation of a requirement nothing is wrong with. The premise must be two-sided (uav.cruisePower >= 100.0 [W] and uav.cruisePower <= 600.0 [W]) before "proved" is available.

--engine auto. Resolves to smt when loadZ3() returns a backend; otherwise every obligation is verification/tool-absent ⇒ inconclusive ⇒ exit 2. There is no silent fallback to literal.

runVerificationCases(model, opts) in src/semantics/verify.ts dispatches each VerificationCaseDefinition/VerificationCaseUsage, resolving verified requirements through Verify relationships and — after commit 2a — through objective { verify R; } members. The verdict follows the library's PassIf: pass iff every verified obligation is proved and non-vacuous; fail iff one is refuted at the model's values; inconclusive otherwise; error when the backend threw.

Method gating is the honesty rule. VerificationMethod carries kind : VerificationMethodKind [1..*], so a case may legitimately say kind = (analyze, test). A case whose kind list contains analyze, or which specifies no method, is judged on the analyze part; any other kind present is reported not performed: method is test/demo/inspect. A case with no analyze in its list is not judged: "inconclusive: method is test — this tool performs analysis only", exit 2, never exit 1 — an unjudged case is not a refutation.

Constructs read. Everything obligations gathers, plus verification def/verification usages, subject clauses, objective { verify R; }, verify R by V;, and @VerificationCases::VerificationMethod { kind = …; } metadata.

Written back (with --record then evidence-attach) — two channels, both TOOL-LOCAL, and the report says so.

• The verdict string goes on the existing metadata RequirementMetadata carrier via setRequirementAttr. That carrier is an unbound tag this tool defines, not a standard element: RequirementMetadata has 0 occurrences in the specification, which has only DerivedRequirementMetadata / OriginalRequirementMetadata, and src/semantics/requirements.ts:23 states plainly that the identifier resolves to nothing and that the value is stored as a quoted string. Its value list mirrors the library VerdictKind literals; it is not a VerdictKind reference.
• The evidence goes in a @SysproseVerification::Evidence §7.27 carrier, one per obligation.
• The standard's own verdict slot is VerificationCase::verdict : VerdictKind {redefines result}, and this tool does not bind it. That is recorded in docs/CONFORMANCE.md, not glossed here.
• @VerificationMethod { kind = analyze; } on the case is standard.

The verdict facet is written only for two claims. proved ⇒ pass; refuted at the model's values ⇒ fail. holds-at-values, holds-structurally, holds-within-bound, design-admitted, vacuous and inconclusive all write verdict = "inconclusive", never pass; the finer claim lives in the evidence carrier and is what the Requirements table displays. A verdict = "pass" facet whose carrier's claim is not proved is verification/verdict-overstates-evidence.

Verdict semantics. MAY say: "proved: A ∧ ¬G unsat in z3-solver 5.2.0, QF_NRA (nlsat), 4 fixed / 1 free, seed 0, timeout 5000 ms; assumptions satisfiable (witness cruisePower = 600 W)"; "refuted: witness cruisePower = 700 W ⇒ endurance 43.9 min (confirmed by re-evaluation)"; "design admitted by the model, not a violation of it: under --free uav.cruisePower, witness …"; "holds at the model's values (literal evaluation, 0 free variables)"; "vacuous: premises unsatisfiable under the axioms"; "inconclusive: unknown after 5000 ms"; "inconclusive: solver absent"; "inconclusive: not evaluable at the model's values". MUST NEVER say "verified", "correct" or "safe"; never "proved" from the literal engine; never "proved" when step (0) was not SAT, when z3 returned unknown, when any relation in the obligation's own body was refused, or when a free variable is unbounded on either side; never a pass without a satisfiable-assumptions witness; never a verdict for a verification method the tool did not perform; never call a refutation obtained under --free a violation of the model.

Literature. dania-clavel-2016 (satisfiability checking of a constraint set in a solver — the negation-UNSAT formulation actually used here, and the many-sorted encoding that keeps undefinedness explicit), cofer-2012 (the compositional obligations and why the system guarantee must follow from the component contracts; note its verification conditions are LTL goals discharged by k-induction over Lustre, not an SMT negation check), kupferman-vardi-2003 (vacuity — steps 2 and 3), filipovikj-2018 (SMT versus a model checker for requirement checks: same verdicts, far less model-building — the reason this engine comes first), barbau-bock-2020 (SMT-LIB encoding conventions — for SysML v1 blocks under the OBM stereotype; only the sort mapping and naming convention transfer), cofer-miller-2014 (which verification objectives an analysis may claim credit for), omg-sysml-2.0-part1-2026 §7.24 and §9.2.17 (VerificationCase, VerdictKind, PassIf, VerificationMethodKind).

App affordance. No solver in the browser in this plan (see §6); the Check panel shows a "prove in the terminal" hint with the exact command.

3.5 consistency — requirement-set satisfiability with a named conflicting subset

In-process API. checkConsistency(model, opts) in src/semantics/consistency.ts. Groups contracts by subject type via conforms, releases every feature that carries a literal value — keeping only the structural axioms, because a consistency question about a requirement set must not be answered by the values that happen to be in the file — asserts each requirement under a named tracking literal, and on UNSAT returns z3's unsat core as the conflicting requirement set with short ids. --with-values re-pins those literals as axioms, which is the mode the illustrative witness below was computed under. On SAT it returns a witness design point, re-evaluated in-process before it is printed.

Written back. verification/inconsistent-requirements (error, naming the core by element id and qualified name). No model mutation.

Verdict semantics. MAY say: "consistent (--with-values): witness mtow = 18.5 kg, cruisePower = 650 W (2 requirements, QF_LRA, 0 relations refused)"; "inconsistent: conflicting subset {R-UAV-002, L8-consistency-conflict::mtowFloor}"; "inconclusive: timeout". MUST NEVER say "consistent" without the refused count beside it; never call a core minimal unless --minimize ran its deletion loop to completion; never say realizable — that is reactive realizability and a different question, and the word is reserved by the claims guard. Note that the shipped example declares R-UAV-001 and R-UAV-002 only; any illustrative core naming a third id names the L8 case it comes from.

Literature. post-hoenicke-2012 and langenfeld-2019 (consistency of a requirement set as an engineering deliverable, at industrial scale), filipovikj-2018, wu-farrell-2021 (MaxUSE: naming the conflicting constraints, and core minimisation — a UML/OCL target), katis-2022 and larraz-tinelli-2022 (realizability and unrealisable cores — cited as the boundary this stops at).

3.6 refine — composition and derivation as contract refinement

In-process API. checkRefinement(model, opts) in src/semantics/refinement.ts. For a system contract C = ⟨A, G⟩ on subject S with sub-contracts C' on the parts that satisfy them, the obligations are Cimatti's Theorem 1, in normal form, with nf(C) = ¬A ∨ G, preceded by a satisfiability precondition:

• (0) check(A ∧ ⋀ nf(C′) ∧ γ) — UNSAT ⇒ every refinement obligation is vacuous: the sub-contracts, the connections and the system assumption cannot hold together (core …), never refined.
• (3) ⋀ nf(C′) ∧ γ ⊨ nf(C)
• (4) for each component U: A ∧ ⋀_{S′≠U} nf(C′) ∧ γ ⊨ A_U

Step (0) is not decoration. Sub-contracts C₁ = ⟨true, x > 10⟩ and C₂ = ⟨true, x < 5⟩ over one bind class, against a system contract ⟨true, x > 1000000⟩, make the antecedent of obligation (3) unsatisfiable, so (3) holds vacuously — without step (0) the tool prints "obligation (3) proved" for an architecture whose components cannot coexist and whose system guarantee is absurd. fault-tree inherits the same hole, and §3.9 closes it there.

The normal form is load-bearing too. With bare guarantees the static check is unsound under mutual support: take A₁ = G₂ = p and A₂ = G₁ = p with system contract ⟨true, p⟩; both obligations pass, yet an implementation with p false satisfies each component contract and breaks the system guarantee. cimatti-2015 reduces to normal form precisely for the refinement checks, and so does this.

γ — the connection assertion — comes from bind/BindingConnector edges AND from the directional item flows propagateValues already carries (src/semantics/connectors.ts, step (b): "carry the source value forward to the target"), encoded as target = source. This is not a taste question: a γ that diverges from propagateValues would break commit 1's own stated gate, because checkConstraints, the app and every existing report already honour those flows, and an unencoded flow produces exactly the false negative §3.6's own worked example shows — "assumption of flightComputer not discharged: witness battery.powerOut.voltage = 0 V" is what you get when a flow that does carry the voltage was not encoded.

Only a bare connection with no flow and no bind is refused. It is listed under notEncoded with the hint "a connection is not an equality; bind the attributes if they are one quantity." An opt-in --connections-as-equalities exists for the OCRA reading, and when it is used the fact is printed on every verdict line. Counter-evidence, recorded rather than buried: cristoforetti-2026 §4.1 — the one published SysML v2 → OCRA path — translates connect and bind alike into OCRA ports and connections, and Cimatti's γ is by definition the connection-and-delegation assertion. So the refusal here is a stricter reading than the published path takes, not a consensus. See §8 decision 2.

--via derive|refine reuses the same checker over Derive/Refine edges with the measured orientation: A_R ⊨ ⋀ A_D (the derived set assumes no more) and A_R ∧ ⋀ nf(G_D) ⊨ G_R.

Written back. verification/refinement-failed (warning, with witness), verification/unconnected-assumption (a part assumption over a port no connection reaches), verification/derivation-not-refinement, verification/refinement-undecided, verification/contract-set-vacuous. Verdicts and evidence through evidence-attach.

Verdict semantics. MAY say: "obligation (3) proved (negation unsat) over 4 sub-contracts, 6 bind equalities and 2 item flows; 9 connections not encoded as equalities"; "assumption of flightComputer not discharged: witness battery.powerOut.voltage = 0 V"; "derivation refines: both obligations proved"; "vacuous: the sub-contracts and γ cannot hold together". MUST NEVER say "the architecture satisfies its requirements"; never anything about ordering or time — this is the propositional/numeric shape, not OCRA's temporal refinement; never treat a bare connect as a value equality without the opt-in flag; never say "refined" while any obligation is undecided; never say "refined" when the antecedent of (3) or (4) is unsatisfiable.

Literature. cimatti-2015 (Theorem 1, obligations (3) and (4), and nf(C) = ¬A ∨ G), cofer-2012 (AGREE's obligations and the well-founded-circularity argument that a static check does not get for free — AADL/Lustre target), benveniste-2015-theory and benveniste-2015-methodology (the contract algebra), abadi-lamport-1993 (assume/guarantee composition and the circularity caveat), westman-2013 (safety goal → FSR refinement as contract refinement), sun-2025 (decomposition with a correctness guarantee), cimatti-2013, cristoforetti-2026 §4.1 and fbk-ocra-2.1.0-2021 (the temporal version this deliberately is not, and the γ counter-evidence).

3.7 bounds — the tightest value the model admits

The question, stated precisely. What is the tightest value this measure can take under the model's axioms — feature values, bind equalities and assert constraint bodies — with require clauses excluded, because a requirement is what is being checked, not a fact? This is why --measure uav.mtow --free all answers unbounded above even though require constraint { uav.mtow <= 25.0 [kg] } sits in the file. The exclusion is repeated on every verdict line, not only here; --with-requirements folds the require bodies in and says so.

In-process API. boundsReport(model, {measure, sense, free, timeoutMs, withRequirements}) over z3's Optimize; objective in SI, result converted back to the feature's declared unit.

Verdict semantics. MAY say: "max mtow: unbounded above under the model's axioms (require clauses excluded)"; "max mtow = 25 kg exactly (linear optimum, --with-requirements), witness …"; "bound found: 47.3 min, optimality not established (nonlinear)". MUST NEVER present a non-optimal bound as the optimum; never fold a require body into the axiom set without saying so on the line. The report names both this and the heuristic coordinate-descent optimize in src/semantics/solver.ts, and says which is which.

Literature. wu-farrell-2021 (the MaxSMT/νZ machinery; its own target is UML/OCL). khelifati-2025 is not cited here — see §7.

3.8 reach and check-behaviour — bounded behaviour

In-process API. src/semantics/mc/config.ts exposes the pure one-step relation enabledTransitions(model, cfg, input) and stepConfig(model, cfg, choice), factored out of the fire / enterCascade / exitTo / chaseHierCompletion closures inside runHierRegion (src/semantics/execute.ts). exploreMachine in src/semantics/mc/explore.ts does breadth-first exploration over hashed configurations, exploring every enabled transition where the interpreter takes the first. checkProperty in src/semantics/mc/patterns.ts decides safety patterns by bad-prefix search on that graph. (This sentence named mc/check.ts until docs/06 was written; that file does not exist and never did.) The engine is pure TypeScript throughout: no solver is in this lane. z3 BMC / k-induction over guarded machines is a Checkpoint-D decision, not a capability this plan builds — the §3 table's Engine cell says TS for that reason, the way §3.12 handles #observable: designed, named, explicitly not shipped.

The catalogue is split by class, because a bad-prefix search cannot refute a liveness property.

• Safety, decided by bad-prefix search: absence, universality, bounded-existence, precedence.
• Liveness, not decided in-process: existence, response. Both report inconclusive: liveness not checked in-process until a lasso search lands and a fairness assumption is named. vogel-2022 — this plan's own citation for the catalogue — is explicit that response is the path-formula exception, which is why it needs observer automata for it at all. A bad-prefix search over a finite configuration graph returns no bad prefix for response, and under a naïve "pass — holds on every reachable configuration" rule that would print a pass nothing earned.

The demonstration on the shipped example is the nondeterminism finding, not a reachability count. FlightModes in examples/uav-isr.sysml has four states and five trigger-less transitions — every one is a completion transition, and autonomous has two of them enabled at once (→ manual and → failsafe). The interpreter's declaration-order tie-break means failsafe is never entered in simulation; verification/nondeterministic-choice is exactly the row that says so. Any report on this machine that shows trigger labels is fabricating them.

Written back. verification/unreachable-state, verification/dead-transition, verification/deadlock, verification/nondeterministic-choice, verification/bound-exhausted, verification/behaviour-unsupported-construct, verification/vacuous-property, verification/malformed-property, verification/unknown-atom. Properties live in the model as @SysproseVerification::PropertyPattern { attribute pattern = "absence"; attribute scope = "globally"; attribute p = "state failsafe"; } — §7.27 metadata, one attribute per field so the phrase-to-atom trace survives.

Every behaviour report carries the semantic profile — run-to-completion (chasing bounded at 64), priority (innermost substate first), history (shallow, by parent map), regions (interpreter concatenates, checker interleaves), deferred events (none — triggerEquals is an exact match, there is no event pool), time (discrete after(n)) — each with its provenance in execute.ts. attrs.parallel and attrs.history are reachable only through the API: sysml.langium has no keyword for them, so a machine using them is verification/behaviour-unsupported-construct with exhaustive: false, never reported as exhaustively explored.

Unreachability may be stated unqualified only when four things hold at once: the exploration was exhaustive, no completion-chase bound was hit, every trigger the machine names was offered, and no unsupported construct was raised. Otherwise it is unreachable under {maxConfigs, maxDepth, maxCompletion 64, alphabet = the triggers the machine names}, or, on any bound hit, suppressed entirely. Implementation note: chaseHierCompletion (src/semantics/execute.ts:1418) today exhausts its 64-step budget indistinguishably from reaching quiescence — no flag, no return value; commit 13 makes it return its budget state, and a budget hit sets exhaustive:false and empties the unreachable and dead lists exactly as a config-bound hit does.

[Superseded in part, O1 behaviour-sound, 2026-10-15 — docs/06 §8.5.] The completion-chase budget is semantics, not a bound. runStateMachine takes the next event wherever a chase spends its 64 steps, and the walk now does the same, so a state that only a chase past the budget would enter is published as unreachable, exhaustive under the printed maxCompletion 64 (chain65: c66…c70 unreachable, t66…t69 dead), and a spent budget neither sets exhaustive:false nor empties the unreachable and dead lists. The second of the four conditions above is gone with it; maxCompletion 64 stays among the printed bounds as the semantics every absence holds under. The one completion-related refusal left is the check-behaviour search that does not carry the chase position (a counting monitor round a trigger-less cycle): it reports verification/bound-exhausted, with no --max-configs advice, because no flag decides it.

--from-keywords. One absence × globally obligation per #exceptional element inside the machine named by --element, over the same configuration graph — see §3.12.

Verdict semantics. MAY say: "explored 41 configurations, exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64}"; "state failsafe unreachable (exhaustive)" — only under the four conditions above; "nondeterministic choice at autonomous: 2 completion transitions enabled, the simulator takes the first"; "pass — holds on every reachable configuration"; "fail — witness trace of 3 steps"; "bound exhausted after 10000 configurations: partial — the unreachable and dead lists are lower bounds and are NOT reported as findings"; "inconclusive: liveness not checked in-process". Reachability is always qualified "structurally" or "exhaustive under {bounds}". MUST NEVER say "verified", "deadlock-free", or "proved"; never a pass when exhaustive is false; never a liveness verdict without naming the fairness assumption.

Literature. andre-2023 §2.6 (run-to-completion, substate priority, region conflicts — the profile's field list, and the survey's point that every published formalisation differs on exactly these), omg-pssm-1.0-2019 Clause 9 (a UML/fUML oracle for the conformance scorecard), vogel-2022 (the pattern × scope catalogue and the safety/liveness split — targeting UPPAAL timed automata), kupferman-vardi-2003, peres-ghazel-2023 (what a trustworthy translation must establish), chrszon-2025 (explicit-state scaling on a mode machine), graics-2020, bouwman-2023 (fairness stated explicitly in an industrial case).

3.9 fault-tree — cut sets from contract-failure injection

In-process API. computeFaultTree(model, opts) in src/semantics/fault-tree.ts. Basic events are "sub-contract i not honoured". A set F is a cut set iff the normal-form obligation (3) fails when the guarantees in F are dropped. A cut-set enumeration whose baseline obligation (3) was vacuous reports inconclusive: contract set vacuous, never no cut set — obligation (3) can never fail from an UNSAT antecedent, so without this the tool prints "no cut set up to order 2" for a contract set that entails everything. Minimal cut sets are enumerated by increasing order up to --max-order (default 2), with supersets pruned; the count of checks run is reported. A @SysproseVerification::FaultHypothesis { maxOrder = 2; } carrier pins the bound in the model.

The two safety lanes stay apart. A StateUsage passed as --element is refused with a pointer to check-behaviour --from-keywords, never answered with an empty cut-set list; a contract-level top event whose requirement carries #exceptional is labelled as such and its cut sets are unchanged.

Verdict semantics. MAY say: "3 basic events; minimal cut sets up to order 2: {battery}, {radio, flightComputer}; 7 checks, all decided"; "no cut set up to order 2 — higher orders not explored"; "inconclusive: contract set vacuous". MUST NEVER claim absence of a single point of failure when any order-1 check was undecided; never call this a behavioural safety analysis — it is contract-level FTA, and the report says so.

Literature. bozzano-2014 (fault trees from contract refinement; intermediate events are contract failures), stewart-2021 (AGREE + Safety Annex + JKind over AADL: minimal cut sets by fault injection into contracts), joshi-2006 (the founding MBSA statement), sun-2022 (what counts as MBSA), rauzy-2019 (why the safety model stays separate and synchronised — FaultHypothesis is that sync handle).

3.10 evidence — records bound to a model version and a tool version

In-process API. src/api/evidence.ts. modelVersionOf(model, sourceText?) returns {graph, source?, library, sysprose} where graph is SHA-256 over a canonical JSON of model.toJSONWhere((el) => isUserElement(model, el)) with elements sorted by qualified name and element ids replaced by qualified names — because ids are fresh UUIDs on every load (D3), a digest over raw SerializedModel would change on a no-op reparse. library records the standard-library manifest count; sysprose records the package version plus the git sha when git rev-parse succeeds and omits it otherwise, never inventing one.

obligationDigest is SHA-256 over the canonical ExprNode of the obligation after unit lowering and literal substitution, with names canonicalised to qualified names — the same normal form the SMT-LIB exporter serialises. It is therefore defined and required from commit 3, before any SMT-LIB text exists, and is stable across engines.

EvidenceRecord = {schema:'sysprose-evidence/1', obligation:{requirement, shortId, clause, obligationDigest}, verdict, claim, engine, tool:{name, version}, bound, witness?, certificate?, modelVersion, producedBy, flags} with claim ∈ {'proved', 'holds-at-values', 'holds-structurally', 'holds-within-bound', 'refuted', 'design-admitted', 'vacuous', 'inconclusive'}, validated against docs/schemas/evidence-record.schema.json with ajv (already a dependency). flags records any option that changed what was proved — --free, --connections-as-equalities, --from-keywords, --with-values, --with-requirements — so a proof cannot be replayed as though the model had said something it did not.

attachEvidence writes a @SysproseVerification::Evidence { … } carrier under the requirement or the verification case, using the same MetadataUsage + AttributeUsage shape setRequirementAttr uses — a shape that parses today with zero diagnostics (probed) and round-trips through the serializer. The SysproseVerification package is the one created at commit 2d; commit 7 extends it with Evidence rather than declaring a second package. Evidence accumulates: a second run appends a record, a fail is never silently overwritten by a pass, and the diff of verdicts is printed.

New validation rule stale-evidence (warning, code validation/stale-evidence, rules 24 → 25) fires when a record's modelVersion.graph no longer matches, naming the changed slice via impactClosure(model, reqId, 2). Attaching refuses under a faulted declaration, reusing FAULTED_DECLARATION_REFUSAL, and refuses to write a degraded model at all.

What an external tool makes of this, stated because interoperability is the goal. The verdict facet is metadata RequirementMetadata { attribute verdict = "pass"; } — an unbound tag holding a quoted string, where the standard has an enumeration on a different metaclass. A conforming SysML v2 reader is entitled to treat that line as an untyped annotation and ignore it; nothing obliges it to interpret the string. The round trip that matters is Sysprose → someone else's tool, and it is untested: this plan tests the write path only inside Sysprose. Commit 16 adds an interop probe through scripts/pilot-write-roundtrip.ts against SYSMLV2_PILOT_URL — the Intercax OMG pilot at http://sysml2.intercax.com:9000 whose genuine cross-implementation exchange is already recorded in docs/CONFORMANCE.md:192-206 — pushing a model that carries a verdict facet and an @SysproseVerification::Evidence carrier, not buildSampleModel. It is emphatically not scripts/pilot-roundtrip.ts, which boots our own createServer() by default and is therefore the self round-trip, i.e. the very thing this paragraph says is not enough. The probe answers the API/JSON path only: what a foreign textual parser makes of the .sysml bytes is a different question and stays untested by this plan. The result is recorded in docs/CONFORMANCE.md as a measured fact, whatever it turns out to be. Until then no claim is made about what another tool reads.

Verdict semantics. MAY say: "current — model sha256:ab12… matches"; "stale — recorded at sha256:9f3c…, 3 elements changed in the requirement's slice — re-run verify --record"; "unrecorded — verdict facet present, no evidence". MUST NEVER upgrade a claim on display: a record whose claim is holds-at-values is never shown as proved; a stale record is never counted as discharged; a verdict = "pass" facet is never written for a claim that is not proved.

Literature. clariso-2020 (incremental verification of UML/OCL: keep the witness and re-check it against the edited model before re-running the solver — that is what the stored witness is for, and what the digest indexes), cofer-miller-2014 and rushby-1993 (evidence must name tool, version and assumptions to be arguable), newcombe-2014. On seidewitz-2020, corrected: it is the metasemantic protocol for language extension, and measured, the words "metadata" and "annotation" occur 0 times in it — so it does not support "tool-specific data belongs in metadata". That sentence is the specification's, and its citation is omg-sysml-2.0-part1-2026 §7.27. seidewitz-2020 is kept only for the extension discipline.

App affordance. The Requirements table gains verdict and evidence columns showing current / stale / none; a stale chip links to the changed slice. Read-only.

3.11 export and certificate-import

In-process API. src/semantics/export/smt2.ts emits the exact assertions the in-process solver saw, with (set-info :source "sysprose <version> <digest>"), :named assertions keyed on qualified names, not element ids, and one (push) (assert (not G)) (check-sat) (get-unsat-core) (pop) block per obligation. export/ocra.ts emits Othello (COMPONENT / INTERFACE INPUT PORT / CONTRACT … assume: … guarantee: / REFINEMENT SUB / CONNECTION / CONTRACT c REFINEDBY …). export/smv.ts emits one MODULE per machine with the state as an enumerated VAR and next(state) as a case over transitions. export/lean.ts emits a theorem skeleton with #print axioms; it imports Mathlib.Data.Real.Basic because core Lean has no ℝ — a "mathlib-free theorem over the reals" does not exist. scripts/lib/external-tools.ts (in scripts/, never in src/, so the browser bundle can never import child_process) discovers z3, cvc5, ocra, nuXmv, lake on PATH with a version probe.

importCertificate maps outcomes strictly: SMT-LIB unsat ⇒ proved; Lean requires build exit 0, no sorry, and #print axioms ⊆ {propext, Classical.choice, Quot.sound}; nuXmv -bmc imports as "no violation within k", never as proved; a TLC or bounded run likewise. The obligation digest in the result must equal the one in the exported file or the import is refused (verification/certificate-mismatch).

Verdict semantics. MAY say: "exported 3 obligations, logic QF_NRA"; "cross-check: z3 5.0.0 (binary) agrees on 3/3"; "cross-check: DISAGREEMENT on R-UAV-001 (z3 unsat, cvc5 sat) — inconclusive, report it"; "inconclusive: cvc5 not installed; files written to out/ — run cvc5 out/R-UAV-001.smt2". MUST NEVER pick a winner on a disagreement; never translate a tool's log into "proved" unless the parsed line is that tool's own success verdict with the axiom set checked; never export an equality the model does not state; never silently truncate a model the exporter cannot express — it aborts naming the element.

Literature. fbk-ocra-2.1.0-2021 (Othello grammar and commands), cimatti-2013, cristoforetti-2026 (the one published SysML v2 → nuXmv/OCRA path, whose component mapping this follows), barbau-bock-2020 (SMT-LIB as the interchange), kausch-2025 (the deductive end), lamport-2002 and newcombe-2014 (what a bounded TLC run does and does not buy), champion-2016 and larraz-tinelli-2022 (CoCoSpec / Kind 2 for the reactive case), gleirscher-marmsoler-2020 (tool trust and reproducibility as adoption blockers).

3.12 #exceptional and the keyword reader — the one facet the standard does not express that this plan ships

The shipped vocabulary. SYSPROSE_VERIFICATION_LIBRARY in src/semantics/verification-vocabulary.ts, written in the serializer's canonical shape so pasting it into a file and saving gives the bytes back unchanged:

package SysproseVerification {
    doc /* One annotation SysML v2 does not express, carried as a user-defined keyword over a metadata definition (SysML v2 7.27.1, 7.27.4). #exceptional says an outcome is a failure rather than an equally valid result. It is a Sysprose extension, not standard vocabulary. */
    metadata def <exceptional> ExceptionalOutcome;
}

Commit 7 extends this same package with Evidence, commit 12 with FaultHypothesis and commit 14 with PropertyPattern, rather than declaring more packages — so a model carrying a keyword and an evidence record declares one Sysprose package with one doc string.

In-process API. src/semantics/keywords.ts: keywordsOf(model, id): Keyword[] — the generalisation of the module-private reader at src/semantics/statement-kind.ts:135, which now consumes it — resolveKeyword(model, keyword) against MetadataDefinitions in scope, hasKeyword(model, id, def), and FOREIGN_KEYWORD_ALIASES, a read-only table mapping Exception/exception → exceptional, precondition → the assumption role and postcondition → the guarantee role, each carrying the provenance string that gets printed.

#exceptional — valence, and the obligation it creates. On a StateUsage, ActionUsage, UseCaseDefinition or requirement it says: this outcome is a failure, not an equally valid result. Under check-behaviour --from-keywords each tagged element inside the machine named by --element becomes one absence × globally obligation — one of the four patterns the bad-prefix engine can actually decide (§3.8) — discharged by the same explicit-state explorer commit 13 builds, with no new engine. reach upgrades a tagged reachable state from an information row to verification/exceptional-reachable. It does not feed fault-tree (§3.9).

Verdict semantics. MAY say: "fail — #exceptional state failsafe is reachable; witness trace of 3 steps (exhaustive under {maxConfigs 10000, maxDepth 200, maxCompletion 64})"; "pass — no #exceptional configuration reachable, exhaustive under {…}"; "inconclusive: bound exhausted after 10000 configurations — the absence claim is not made"; "vacuous: the tagged state has no incoming transition". MUST NEVER say safe, deadlock-free or verified; never a pass when exhaustive is false; never count a tagged element outside the machine under --element as anything but an info row.

Reading somebody else's vocabulary. contracts --keywords inventories every prefix keyword with what it resolves to. A third-party #Exception produces the #exceptional obligation with verification/foreign-keyword (info) and the provenance printed on every line that used it. A third-party #precondition / #postcondition is read, listed, and contributes a premise or a guarantee only under obligations --from-keywords, which is off by default and recorded in the evidence record's flags. A keyword that names no MetadataDefinition in scope gets verification/keyword-names-nothing (info), emitted by contracts --keywords and not by npm run check — so the 24 validation rules, the check exit contract and the 81 fixtures are untouched.

Verdict semantics for the inventory. MAY say: "sysprose vocabulary: #exceptional on 1 element"; "third-party spelling: #Exception read as SysproseVerification::exceptional on P::Abort — not SysML v2, not a Sysprose keyword"; "names nothing: #precondtion on P::Launch resolves to no metadata definition in scope". MUST NEVER call a third-party keyword standard; never report a keyword as resolved when no MetadataDefinition in scope carries that name; never change an obligation set — this row is an inventory.

#observable is HELD, and this is what holding means. The gap is real — "observable" is a narrative word in Part 1, not a construct — and the design for it is written: a fifth, report-only gate on property-check that names the atoms a demo or test method could not witness, plus --observable-only on the data dictionary, plus a verification/unobservable-atom info row from the method gate. It is not shipped, because a metadata def the tool writes into user files is a compatibility commitment and this one discharges no obligation. Nothing in this plan depends on it. It is revisited at Checkpoint B; if a shipped example needs it, it is one commit against the reader that already exists.

CLI additions.

Literature. omg-sysml-2.0-part1-2026 §7.27.1 and §7.27.4 (the metadata channel and the #situation occurrence def Failure; example that sanctions a user-defined failure marker); joshi-2006, sun-2022, bozzano-2014 (failure states as model-authored input to safety analysis); vogel-2022 (the absence × scope catalogue); kupferman-vardi-2003 (vacuity on a tagged state with no incoming transition); cofer-miller-2014; seidewitz-2020 (extension discipline only — see the correction in §3.10); almeida-2024.

App affordance. The Contracts table gains a keyword column; the Properties panel shows the keywords on the selected element with what each resolves to. Read-only, deferred to the closing commit.

4. Implementation plan

Twenty-one commits: 0, 1, 2a–2d, 3–14, 14b, 15, 16 — of which commit 0 is doc-only (it lands this document and the two guard entries it needs), so twenty commits change code. The numbering of 3–16 is unchanged from the first draft so external cross-references still land; commit 2 splits four ways because D1+D2+D4 are behaviour changes to shipped round-trip semantics across five clause kinds with a corpus-wide serializer diff, and 2d creates the vocabulary package every later commit extends.

Per-commit convention throughout. 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 4, 7 and 16 here). npm run campaign is part of npm test. npm run build is in the gate because a browser-bundle failure is build-only and commits 4 and 16 are exactly where one lives.

A new spec-table row is FIVE edits, not one:

1. the row in scripts/lib/sysprose-spec.ts (and the dispatch arm in scripts/sysprose.ts);
2. the APP_DOORS entry in test/unit/readme.test.ts with controls: [] for a CLI-only command, and a README row whose In the app cell reads — no view yet and carries NO dagger. The guard asserts exactly that, and the two shipped CLI-only rows (orphans, prompts, README.md:119-120) follow it: readme.test.ts:226 pins APP_DOORS.length === COMMANDS.length + 1; :250-257 pins that an empty-control row's cell must match /no view yet/; the dagger test at :288-303 computes expect(marked).toBe(door.controls.length > 0 && !same), so for controls: [] a dagger fails the test. Commit 16's Contracts view is the one place a dagger may ever be needed here, and only if contracts runs a different function in the app than in the terminal;
3. the README capability-table row (readme.test.ts:315 asserts the table shows every subcommand and no others);
4. the docs/USER-GUIDE.md section (user-guide.test.ts:226 asserts the guide points at every subcommand);
5. npm run commands to regenerate docs/CLI-REFERENCE.md.

And one standing rule that covers phases 0–5 at once: anything §3 calls an in-process API is re-exported from src/api/index.ts in the commit that adds it, so src/api/index.ts belongs in that commit's Files: — it is the public surface (src/api/index.ts:12-89, explicit named re-export blocks per module) and a report nobody can import is not an API.

Every commit that adds a test file re-measures docs/CONFORMANCE.md — the suite-file count in both places and the N passed + M E2E = T green arithmetic that docs-counts.test.ts checks — so docs/CONFORMANCE.md appears in the Files: of commits 1–16, not only 16. Every commit that adds a diagnostic code runs npm run codes. Fifteen commits in this plan add codes, and a blanket rule that fifteen Files: lists silently owe an edit to one prose figure is how a gate goes red on the third commit — test/unit/docs-counts.test.ts pins **N catalogue codes** in docs/AGENT-AUTHORING-CAMPAIGN.md:136 against DIAGNOSTIC_CODES.length (56 today). So the figure becomes generated, not hand-edited: commit 2c extends scripts/gen-diagnostic-codes.ts to rewrite the **N catalogue codes** figure in that file the same way it regenerates docs/DIAGNOSTIC-CODES.md, and the per-commit gate already runs npm run codes first, so the count can never be the thing that fails. The fixture-directory count in the same file stays a hand edit — it is named explicitly in the Files: of the two commits that move it (2b and 7).

L8 is a SUITE level. Commit 3 adds test/campaign/verification.test.ts — a golden-verdict runner beside L7's CLI suites, with its cases carried as data in the suite, not as test/fixtures/agent-authoring/ directories. The existing checker harness (test/campaign/harness.ts, authoring-campaign.test.ts) scores CheckReport diagnostics only and is left alone. The one L8 case that belongs in the fixture corpus is L8-evidence-stale, because validation/stale-evidence is a real npm run check rule; it lands in commit 7 and moves the fixture count by exactly one.

Working-tree precondition, before commit 0. Delete scripts/probe1.ts — the probe file this document's measurements were taken with, untracked at f1cd587. Then confirm npm test is green: vitestFileCount must read 129, matching both places docs/CONFORMANCE.md quotes it (:28, :244). Leaving a probe spec behind is worse than leaving a script behind, because specFiles('test') counts it and a guarded number moves; the only probe left in the tree is the script, and it goes too.

Commit 0 — docs: land the formal-verification plan (doc-only; no src/ change) Files: ADD docs/04-formal-verification-plan.md (this document). CHANGE README.md — add its row to the "Reference docs" index, next to docs/03-architecture-and-plan.md, because test/unit/readme.test.ts > the README documentation index > links every document in docs/ walks docs/ and fails on any file the README never links. CHANGE test/unit/claims.test.ts — add docs/04-formal-verification-plan.md to SKIP_FILES, alongside test/unit/claims.test.ts and CLAUDE.md, for the same reason those two are there: this document has to quote the banned forms verbatim in order to ban them. CHANGE the ledger. Tests: no new test. The gate is the existing one, and it is the point of the commit. Gate proves: the document does not itself break the repository gate. Measured at f1cd587 with this file untracked and neither entry made, npx vitest run returns Test Files 1 failed | 128 passed (129); Tests 1 failed | 2244 passed (2245) — the failure being "documents the README never links: 04-formal-verification-plan.md". A plan whose own landing turns the build red is not a plan an engineer can start from, so this is commit 0 rather than a footnote. Depends on: —

Phase 0 — the prerequisites, the worklist, and an answer with no solver (commits 1, 2a–2d, 3) · FIRST DELIVERABLE

Commit 1 — refactor(semantics): lift the relation layer so a second engine stands behind the same unit gates Files: CHANGE src/semantics/solver.ts — export parseRelationBody, lowerUnitLiterals, substituteLiterals, relationScope, idScopeFor, scaleOfRelation, relationRefused, storageScaleOf, nodeDimension, the value NO_MARKERS:1055 and the types UnitScale, ScaleMap, LoweredBody, LoweredLiteral, MarkerDimensions:471 and OperandDimension:652 (or move them to src/semantics/relations.ts which solver.ts re-imports; no behaviour change). The three type names are not optional decoration: scaleOfRelation:445-453 and relationRefused:626-634 take a markers: MarkerDimensions argument and nodeDimension:663-668 returns an OperandDimension, so without them commits 2c and 4 cannot construct the argument or name the result, and "encodability is the same gate the numeric surface applies, because it calls the same functions" (§3.2) is unbuildable. DerivationMemo is already importable (solver.ts:69, from ./units-eval); relations.ts re-exports Dimension and INDETERMINATE:651 from ./units so a caller can destructure an OperandDimension. isBindingEdge is NOT in this list — it is already exported from src/semantics/connectors.ts:93 and already re-exported by src/semantics/index.ts:96-104, and re-exporting it a second time is TS2300: Duplicate identifier, i.e. npm run typecheck and npm run build red on the very first commit of the lane. What this commit does instead is de-duplicate it: delete the byte-identical private copies at src/semantics/solver.ts:914 and src/semantics/execute.ts:1495 and have both modules import { isBindingEdge } from './connectors';. The module charter — encode after the gates; report what the gates refuse — is the module docstring at the top of src/semantics/relations.ts, restated at the top of src/api/verification.ts in commit 2c, the way src/text/langium/diagnostic-codes.ts:1-17 carries its own invariant. No src/verification/ directory is created; no code would live in it and eslint src/ test/ scripts/ would not police it. CHANGE src/semantics/index.ts — for the newly lifted names only; it needs no change for isBindingEdge, which it already re-exports. CHANGE src/semantics/execute.ts (drop the private isBindingEdge copy), docs/CONFORMANCE.md. Tests: existing semantics.solver*.test.ts, semantics.units-eval.test.ts, units.integration.test.ts unchanged and green — plus semantics.execute*.test.ts and semantics.connectors*.test.ts, which are the regression surface of the de-duplication. NEW test/unit/semantics.relations.test.ts pins the contract: 2000 [kg] lowers to an SI marker of dimension M; d [m] >= t [s] is refused as dimension-clash; t2 - t1 on °C is refused as offset arithmetic while t2 >= 300 [K] is not; a [km] feature carries factor 1000; a Real compared with a bare literal stays unscaled. And the seam test the first draft did not have: a compile-only assertion that calls relationRefused(model, node, vars, nameToId, NO_MARKERS, new Map()) from outside the module and stores nodeDimension(...) in a declared OperandDimension. That is what proves the seam is usable by a second engine rather than merely export-annotated; a lifted function whose argument type stayed private is not lifted. Gate proves: the SMT encoder will reuse, not re-implement, the gates the numeric surface applies, and it can name the types it must pass. Review target: did any export change the order or the memoisation of a gate? And: three copies of one predicate existed (connectors.ts:93, solver.ts:914, execute.ts:1495) — one survives; did the two deleted call sites keep their behaviour exactly? Depends on: 0

Commit 2a — fix(text): clause bodies survive the round trip, and the serializer emits constraint`` Files: CHANGE src/text/langium/map-to-model.ts — mapRequirementClause:2089 walks node.body and node.members for every clause kind, not only node.expr; a nested verify R; inside objective { … } (grammar kind='verify', sysml.langium:282) becomes a Verify relationship owned by the objective — a deliberate deviation from the grammar's declared clause shape, which the serializer and the round-trip test both honour. CHANGE src/text/serializer.ts — requirementClauseLine:701 emits the constraint keyword after assume/require/assert and renders clause bodies. CHANGE docs/CONFORMANCE.md (the round-trip conformance row and the corpus byte diff), ledger. Tests: NEW test/unit/text.clause-bodies.test.ts: objective { doc /* … */ assume constraint { armed == true } require constraint { altitude > 0.0 } } survives parse → serialize → parse with the doc, the assumption and the guarantee intact — today the whole body is deleted and it serialises as objective; (measured); require constraint bound { doc /* … */ x < 10.0 } keeps both its doc and its constraint keyword; actor, stakeholder and frame bodies survive; objective { verify R; } yields a Verify edge and re-emits as verify R; inside the objective body. The corpus-wide serializer diff is measured and recorded; the 81 fixtures are re-run through checkText and any golden that moves is re-recorded in this commit with the reason; the L6 round-trip invariant (invariants.test.ts:201) is re-run and any movement in its named list is re-recorded here too. Gate proves: the standard's own home for a behaviour precondition and postcondition is readable and survives a save, and the writer emits a declaration rather than a reference. Review target: does any clause kind still ignore its body? Depends on: —

Commit 2b — fix(validation): requirement-subject resolves through effectiveFeatures Files: CHANGE src/validation/rules.ts — requirement-subject accepts a subject inherited through effectiveFeatures (today requirement r : Def; warns). CHANGE docs/CONFORMANCE.md, docs/AGENT-AUTHORING-CAMPAIGN.md (fixture count), ledger. Tests: CHANGE validation.rules.test.ts: silent on an inherited subject, still firing on a genuinely absent one; a new L4 fixture pins the behaviour change beside L4-requirement-no-subject and L4-requirement-subject-declared. Gate proves: one behaviour change, one regression surface, one review. Depends on: —

Commit 2c — feat(verify): contracts and obligations Files: ADD src/semantics/contracts.ts, src/semantics/obligations.ts, src/api/verification.ts (contractReport, obligationsReport; the charter docstring). CHANGE src/validation/types.ts — DiagnosticSource += 'verification', the only source this lane adds; its own doc comment (types.ts:35-38) says the type exists so a consumer can filter without parsing the code string, and four sources for one lane would buy nothing. CHANGE src/text/langium/diagnostic-codes.ts (+ verification/unsupported-expression, verification/contract-no-guarantee, verification/nonstandard-clause-location), src/api/index.ts (re-export contractReport and obligationsReport — the standing rule above), scripts/gen-diagnostic-codes.ts (it now also rewrites the **N catalogue codes** figure in docs/AGENT-AUTHORING-CAMPAIGN.md, so no later commit owes that file a hand edit for codes), scripts/lib/sysprose-spec.ts (rows contracts, obligations), scripts/sysprose.ts, test/unit/readme.test.ts (APP_DOORS, controls: [], no dagger, cell reads — no view yet), README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md; REGEN docs/CLI-REFERENCE.md, docs/DIAGNOSTIC-CODES.md, docs/AGENT-AUTHORING-CAMPAIGN.md's codes figure; ledger. Tests: NEW test/unit/api.verification.test.ts — uav-isr yields 2 contracts on subject uav : AirVehicle, each 0 assumptions / 1 guarantee, both satisfiedBy uav, status open; vehicle yields 1; a #prose requirement contributes none; a use case def with an objective yields 1 contract with 1 assumption and 1 guarantee; a plain constraint is classified as an obligation, not an axiom; assume constraint inside an action def still parses and raises verification/nonstandard-clause-location; refusal cases for dimension clash, offset arithmetic and a collection-valued feature; the Verify/Derive/Refine orientations are re-measured on their own probe models. L7 CLI cases for both rows and for REF resolution (qualified name, short id, ambiguous ⇒ exit 2). Gate proves: the worklist is complete and honest with no solver — every relation is either encodable or listed with the gate that refused it, and every role in the map has exactly one bucket. Depends on: 1, 2a, 2b

Commit 2d — feat(keywords): a general keyword reader, the SysproseVerification vocabulary, and foreign-keyword interop Files: ADD src/semantics/keywords.ts (keywordsOf, resolveKeyword, hasKeyword, FOREIGN_KEYWORD_ALIASES), src/semantics/verification-vocabulary.ts (SYSPROSE_VERIFICATION_LIBRARY — a plain metadata def <exceptional> ExceptionalOutcome; package following STATEMENT_KIND_LIBRARY:111, not the SemanticMetadata shape). CHANGE src/semantics/statement-kind.ts to consume the shared reader; scripts/lib/sysprose-spec.ts (contracts --keywords, obligations --from-keywords), scripts/sysprose.ts. ADD codes verification/foreign-keyword (info), verification/keyword-names-nothing (info). REGEN docs/CLI-REFERENCE.md, docs/DIAGNOSTIC-CODES.md; CHANGE docs/USER-GUIDE.md, docs/CONFORMANCE.md (the four-facet table of §2.1 with its spec citations), README.md, ledger. Tests: the package text round-trips idempotently from the second save — measured, #exceptional\n part def Abort; normalises to #exceptional part def Abort; on the first save and is stable thereafter, so byte-identity from arbitrary input is not asserted. #exceptional, #Exception, #precondition, #postcondition, #Observable, #SysproseVerification::exceptional and the misspelt #precondtion all parse with zero diagnostics and round-trip idempotently on an action def, an action usage, a use case def, a state usage, a port usage and an attribute usage — the interoperability ratchet. resolveKeyword returns the definition for #exceptional and undefined for #precondtion, which then produces verification/keyword-names-nothing from contracts --keywords and not from npm run check. A foreign #Exception produces verification/foreign-keyword naming the third-party spelling. obligations without --from-keywords yields bit-for-bit the pre-keyword obligation set. Negative test: the SemanticMetadata shape produces three ref/unresolved-specialization warnings today, pinned so nobody ships it by mistake. Gate proves: Sysprose reads and preserves anybody's #keyword vocabulary losslessly, ships its own one through the mechanism §7.27.4 sanctions, and cannot silently let a vocabulary it did not define change a proof. Review target: does any code path treat an alias hit as if the model had used a Sysprose keyword? Depends on: 2c

Commit 3 — feat(verify): verify --engine literal, the evidence record, VERIFY_EXIT_CODES, and the L8 suite Files: ADD src/semantics/engines/literal.ts, src/api/evidence.ts (modelVersionOf with id canonicalisation, obligationDigest over the canonical ExprNode, EvidenceRecord, recordEvidence), docs/schemas/{evidence-record,verify-report}.schema.json, test/campaign/verification.test.ts (the L8 golden-verdict runner). CHANGE src/api/verification.ts (verifyModel), src/api/index.ts (re-export verifyModel, recordEvidence); scripts/lib/sysprose-spec.ts — ADD the verify row with flags --engine auto|literal|smt, --free F, --record PATH, --allow-inconclusive; ADD VERIFY_EXIT_CODES beside CHECK_EXIT_CODES with the same style of comment explaining why it is a third contract; ADD exitContract: 'report' | 'verify' on CommandSpec. CHANGE scripts/gen-cli-reference.ts — today it emits the exit-code paragraph once for the whole sysprose section (:127, ${EXIT_CODES.replace(…)}) with CHECK_EXIT_CODES hand-written separately (:193); it must instead render that paragraph per subcommand from cmd.exitContract, or docs/CLI-REFERENCE.md documents verify under a contract where exit 1 means "the model did not load cleanly" — the exact opposite of VERIFY_EXIT_CODES, where exit 1 means refuted. renderCommandUsage (scripts/lib/sysprose-spec.ts:253, interpolating EXIT_CODES at :248 and :268) takes the same treatment, and test/unit/cli-reference.test.ts:34 asserts DOC === renderCliReference(), so the doc cannot be hand-patched into agreement. CHANGE scripts/sysprose.ts (judge(), top-level verdict: {discharged, violated, inconclusive, designAdmitted, exitCode} in every judging --json, degraded ⇒ 2). ADD codes verification/vacuous-pass, verification/not-evaluable, verification/unsupported-construct, verification/tool-absent, verification/design-admitted. CHANGE test/unit/readme.test.ts (APP_DOORS for verify: controls: [], no dagger, cell reads — no view yet), test/unit/cli-reference.test.ts — extend it('states the exit-code contract'), today only toContain('0 clean') / toContain('2 usage/IO error'), to assert that every exitContract: 'verify' command's section quotes VERIFY_EXIT_CODES and no 'report' command does; without that the third contract is unguarded. README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md, docs/AGENT-AUTHORING-CAMPAIGN.md (the L8 suite row); REGEN both generated docs. Tests: uav-isr both requirements holds-at-values (endurance 47.3 min ≥ 45 min; mtow 18.5 ≤ 25 kg), vehicle mass 1500 ≤ 2000 — exit 0 under --engine literal; the same run under --engine auto with SYSPROSE_NO_Z3=1 → every obligation verification/tool-absent, exit 2, and --allow-inconclusive does not lower it. A checkConstraints 'unknown' case → inconclusive: not evaluable, exit 2. An assume constraint { false } case → vacuous, exit 2 with and without --allow-inconclusive — vacuity is the §6 declared deviation, not an undecided obligation, and §2 puts it outside the flag's scope. A violating case exits 1 even with --allow-inconclusive. modelVersionOf is byte-stable across two loads of the same text (the UUID test), changes when a literal changes, ignores library elements, omits the git sha when git is absent. Records validate against the schema with ajv, with obligationDigest required. Gate proves: a pass is never printed without an antecedent witness; the literal engine never says "proved"; auto never degrades silently; every inconclusive is exit 2 by default; the digest survives a reparse. Review target: does any code path key a digest or an assertion name on an element id? Depends on: 2c, 2d

First deliverable, runnable after commit 3 with nothing installed beyond the repo: npm run sysprose -- contracts examples/uav-isr.sysml → 2 contracts on uav : AirVehicle, guarantees uav.endurance >= 45.0 [min] and uav.mtow <= 25.0 [kg], both satisfied by uav, the endurance one carrying the derived equation battery.capacity * usableEnergyFraction / cruisePower. npm run sysprose -- obligations examples/uav-isr.sysml --missing → 2 open obligations (the two require bodies) over an axiom set of 1 equation (battery.capacity * usableEnergyFraction / cruisePower) plus the literal feature bindings — 0 inequalities in the axiom set, because the model's only two inequalities are the obligations themselves; 0 relations refused. (Counts re-measured at commit time, not quoted from this document.) npm run sysprose -- verify examples/uav-isr.sysml --engine literal --record .scratch/uav.json → "holds at the model's values (no assumptions — the pass is unconditional at these values)" for both, exit 0, and a schema-valid evidence record bound to the canonical digest and to sysprose <version> / engine literal. npm run sysprose -- verify examples/uav-isr.sysml --engine auto (z3 not installed) → 2 inconclusive, verification/tool-absent, exit 2. npm run sysprose -- verify examples/vehicle.sysml --engine literal → the same for MassRequirement, exit 0.

(The record is written into .scratch/, which .gitignore already covers. out/ does not appear in .gitignore, so a documented first run that wrote there would leave an untracked directory for the next git status review to explain away.)

Phase 1 — the SMT engine (commits 4–6)

Commit 4 — feat(smt): z3 behind a dynamic import, the encoder behind the unit gates Files: package.json (z3-solver ^5.2.0 as an optional dependency), vite.config.ts (excluded from the browser bundle). ADD src/semantics/smt/z3-bridge.ts (loadZ3() → backend or {absent, reason}, honouring SYSPROSE_NO_Z3=1 so the absent path is testable on a machine that has z3; fixed smt.random_seed, per-check timeout, version capture), src/semantics/smt/encode.ts (ExprNode → terms; one variable per feature in its storage unit with factor·x + offset from the ScaleMap; exact rationals from attrs.valueText; sorts Real/Int/Bool from ScalarValues typing; if → ite; / by a free variable adds ≠ 0 and says so; %, variable exponents, strings, calls, indexes, collection-valued features refused with a code). CHANGE docs/CONFORMANCE.md. Tests: the three probe checks re-pinned (unsat, negation-unsat, sat with witness); timeout honoured on a hard NRA instance (returns unknown, never hangs); SYSPROSE_NO_Z3=1 → absent with a reason; version string non-empty; SI scaling verified (45.0 [min] → 2700); two encodes of the same model are byte-equal; the fragment rule — freeing a divisor promotes QF_LRA → QF_NRA and the report names the variable. Init is re-measured separately from the three checks and the figure registered (§6). Worker safety: the SMT suites are run under the default vitest worker pool and under a single fork, verdicts and wall clock compared. Full gate plus npm run test:e2e (this commit touches vite.config.ts). Gate proves: a shared, tested SMT seam exists; z3's absence is a first-class tested outcome, not an import error; the browser bundle does not carry the WASM; and the parallel-worker cost is known rather than assumed. Depends on: 1

Commit 5 — feat(verify): --engine smt — negation-unsat proofs, vacuity, axiom consistency, the differential gate, the relation census, and the CI contract Files: ADD src/semantics/engines/smt.ts (steps 0–3). CHANGE src/api/verification.ts, scripts/lib/sysprose-spec.ts (--timeout MS and --strict-vacuity added to the existing verify row, and to the §3 table's CLI column in the same commit so it keeps quoting what a reader can actually type; --strict-vacuity has the meaning §2 gives it — it raises verification/vacuous-property as an error and does not change the exit code). --fix is not shipped: the first draft made it conditional on a §6 definition beside --free that was never written, and this plan does not add a flag it has not specified. scripts/sysprose.ts. ADD codes verification/refuted, verification/vacuous, verification/vacuous-property (the error --strict-vacuity promotes the vacuity row to — it is declared HERE, with the flag that needs it, and reused unchanged at commit 14), verification/timeout, verification/inconsistent-axioms, verification/free-variable-unbounded. ADD .github/workflows/verify-examples.yml with three jobs: --engine smt with z3 installed (exit 0); --engine auto with SYSPROSE_NO_Z3=1 (asserts exit 2); --engine literal with SYSPROSE_NO_Z3=1 (asserts exit 0). CHANGE docs/CONFORMANCE.md; REGEN docs/DIAGNOSTIC-CODES.md. Tests: the differential gate — test/integration/verification.differential.test.ts: for every campaign fixture and both examples, --engine smt --free none agrees with checkConstraints on every encodable relation (proved ⇔ satisfied, refuted ⇔ violated, and unknown ⇔ inconclusive: not evaluable — the third row, asserted, not left undefined), including the strict-boundary rule of d568a1f; any disagreement fails with both messages printed. The relation census — every constraint-bearing user element is accounted for as encoded, refused-with-reason, or unsupported-with-code, and the counts are asserted equal to the element census; a case whose relation silently disappears fails the gate. A model with one false plain constraint and one violated require exits 1 with two refutations on both engines, never axioms inconsistent. Uav --free none → both proved; --free uav.cruisePower with only an upper premise → verification/free-variable-unbounded, inconclusive, exit 2, never refuted; adding assume constraint { uav.cruisePower >= 100.0 [W] and uav.cruisePower <= 600.0 [W] } → proved (QF_NRA) with a non-vacuity witness; a two-sided --free refutation prints design-admitted and exits 2; an inconsistent-axioms case → every obligation inconclusive with the core, never proved; a tautology case flagged. The npm test wall clock is measured before and after and registered (§6). Gate proves: "proved" is printed only after negation-UNSAT under a satisfiable axiom set, with a non-vacuity witness and a two-sided domain; the point mode cannot drift from the existing evaluator; and no relation left the pipeline unaccounted for. The tool-absent path is exercised in CI on every run, so it cannot rot into a silent green. Depends on: 3, 4

Commit 6 — feat(verify): consistency — requirement-set satisfiability with a named conflicting subset Files: ADD src/semantics/consistency.ts; CHANGE src/api/verification.ts, scripts/lib/sysprose-spec.ts (row consistency, --subject, --with-values, --minimize, --max-core), scripts/sysprose.ts, test/unit/readme.test.ts (APP_DOORS), README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md; code verification/inconsistent-requirements; REGEN both generated docs. Tests: uav-isr consistent with a re-evaluated witness under --with-values, and the literal values released without it; an L8 case adding require constraint { uav.mtow >= 30.0 [kg] } → inconsistent with a core naming both constraint ids; a core is labelled "a conflicting subset" unless --minimize completed; a °C relation appears under refused, not in the core; no solver → inconclusive, exit 2, and --allow-inconclusive does not lower it. Gate proves: inconsistency is only ever printed with a named subset from an UNSAT core; "consistent" always carries the refused count and the mode it was computed in; the word "realizable" appears nowhere. Depends on: 5

Checkpoint A. Full gate green; docs/USER-GUIDE.md has the verdict-vocabulary table; the CI workflow is running all three jobs. Decision point: does the differential gate hold across the whole fixture corpus, and did the relation census find any element the gatherer drops? If either exposed a genuine disagreement, that disagreement is the next commit, not phase 2.

Phase 2 — verdicts in the file, and the agent surface (commits 7–9)

Commit 7 — feat(evidence): attach, status, detach — the verdict facet, §7.27 carriers, the stale-evidence rule Files: CHANGE src/api/evidence.ts (attachEvidence, detachEvidence, evidenceOf, evidenceStatus naming the changed slice via impactClosure), src/semantics/verification-vocabulary.ts (extend commit 2d's package with Evidence; one package declaration, not two). CHANGE src/validation/rules.ts (+ stale-evidence, RULES 24 → 25). test/unit/docs-counts.test.ts holds nine RULES.length claims across seven files, and every one of them reads 24 today, so all seven are named here rather than hidden behind "every doc that quotes the rule count updates" — and note that one of them — src/ui/store.ts:943 — is source, not a doc. The nine are: docs/AGENT-AUTHORING-CAMPAIGN.md:136; docs/FEATURE-PARITY.md:78 and :127; src/ui/store.ts:943 (the // … validation (24 rules), textual RECOMPUTE comment); docs/TEST-REPORT.md:259 and :314; docs/architecture/05-data-flow.md:104; docs/architecture/06-sequence-diagrams.md:48; docs/USER-GUIDE.md:400. Missing any of them is seven failing assertions on a commit whose Files: list looked complete. CHANGE src/text/langium/diagnostic-codes.ts (+ validation/stale-evidence, verification/claimed-without-evidence, verification/verdict-overstates-evidence), scripts/lib/sysprose-spec.ts (rows evidence-status, evidence-attach, evidence-detach), scripts/sysprose.ts (refuses to write the input path unless named; refuses a degraded model; refuses under a faulted declaration with FAULTED_DECLARATION_REFUSAL), test/unit/readme.test.ts, README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md, docs/AGENT-AUTHORING-CAMPAIGN.md. CHANGE src/diagram/requirements-table.ts (verdict + evidence columns). ADD fixture L8-evidence-stale (fixture count +1); REGEN both generated docs. Tests: attach → serialize → parse → evidenceOf is the identity and idempotent from the second save; a second attach appends, does not overwrite, and a fail is never replaced by a pass without the diff being printed; attach on a library element throws; edit a literal → npm run check warns validation/stale-evidence naming the slice; a hand-written verdict = "pass" with no carrier fires verification/claimed-without-evidence; a --engine literal record attaches verdict = "inconclusive" and the requirements table shows holds-at-values, never pass; a verdict = "pass" facet over a non-proved carrier fires verification/verdict-overstates-evidence. Full gate plus npm run test:e2e. Gate proves: a verdict in the file always names its tool, version and model digest, cannot survive a model edit unnoticed, cannot be laundered, and cannot overstate the claim behind it. Depends on: 2d, 5

Commit 8 — feat(verify): verification cases get a computed verdict, gated by VerificationMethodKind Files: ADD src/semantics/verify.ts (runVerificationCases, writeVerdict). CHANGE scripts/lib/sysprose-spec.ts (verify --case), scripts/sysprose.ts. ADD examples/uav-isr-verification.sysml (an analyze case, a test case, and one mixed kind = (analyze, test) case). Codes verification/no-property, verification/verdict-changed, verification/method-not-performed — §2's exit table names it, so it must exist as a code rather than as prose, or the --allow-inconclusive scope has nothing to key on. CHANGE docs/CONFORMANCE.md, test/unit/docs-counts.test.ts — this commit ADDS the two CLAIMS entries the first draft deferred to commit 16: the example count against readdirSync('examples') and the subcommand count against COMMANDS.length. They belong here because this is the first commit that adds an example, and a guard that arrives after the count it guards has already moved four times guards nothing; commits 9, 10 and 14b then have a real entry to update rather than a no-op edit. REGEN docs/DIAGNOSTIC-CODES.md. Tests: the analyze case → pass with its obligation rows attached; the test-method case → verification/method-not-performed, "inconclusive: method is test — this tool performs analysis only", exit 2 with and without --allow-inconclusive, never exit 1 — the flag's scope (§2) covers verification/timeout and verification/unsupported-construct only, and an unperformed method is neither; the mixed-kind case is judged on the analyze part and reports the rest as not performed; a case verifying a refuted requirement → fail with witness; both the verify R by V; form and the objective { verify R; } form are found and cross-checked against traceabilityMatrix(model, 'VerificationCaseUsage', 'RequirementDefinition', 'Verify') — the metaclasses behind the verify preset in TRACE_PRESETS (scripts/lib/sysprose-spec.ts:68, the verify entry at :71), noting the axis metaclasses differ for a model that declares its requirements as usages; --record then evidence-attach writes the verdict facet plus @VerificationMethod { kind = analyze; }. Gate proves: a verdict is never claimed for a method the tool did not perform, and an unjudged case is never mistaken for a refutation. Depends on: 7

Commit 9 — feat(property): draft and check — gate 0, the four gates, and the back-translation Files: ADD src/api/property.ts; CHANGE src/api/index.ts (re-export propertyDraft, propertyCheck); scripts/lib/sysprose-spec.ts (rows property-draft, property-check) and scripts/sysprose.ts (the dispatch arms for both) — the dispatch is a literal switch (scripts/sysprose.ts:758-772, one case '<name>': per shipped command), so a spec row without an arm is a command that prints help and does nothing; codes verification/temporal-field-unencodable, verification/unresolved-name-in-property, verification/dimension-clash-in-property, verification/trivial-property, verification/nontriviality-unchecked. ADD examples/contract-authoring-prompts.sysml (a #prompt package: assume only on inputs and parameters; one guarantee per require; name the subject; never hand-write a verdict). CHANGE scripts/agent-repair-bench.ts (--suite verification), test/unit/readme.test.ts, test/campaign/cli.sysprose.test.ts (the L7 CLI case §3.0 promises per new command — no commit in the first draft named the L7 suite file, which is how a row ships untested; every row-adding commit from here on names it), README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md, test/unit/docs-counts.test.ts (the example count, against the entry commit 8 added); REGEN both generated docs. Tests: a drafted clause with scope = after is refused at gate 0, not accepted-with-gap; endurance >= 45 [min] refused with the suggestion uav.endurance; uav.endurance >= 45.0 [kg] refused as a dimension clash; uav.mtow <= uav.mtow trivial with z3 present and "unchecked" with SYSPROSE_NO_Z3=1 — both asserted; uav.mtow <= 25.0 [kg] passes gate 4 even though the model pins mtow = 18.5 [kg], and the limits register says why; an accepted clause returns the insertion range; golden back-translation strings; promptsFor collects the authoring guidance through the package. Gate proves: no generated clause reaches verify without being in an encodable fragment, parsing, resolving, agreeing dimensionally and being non-trivial on its own; and the tool never claims the clause means what the prose meant. Depends on: 5

Checkpoint B. A requirement can go prose → clause → proof → verdict facet in the file → stale on the next edit, entirely from the terminal. This is the point at which the plan is useful to an engineer even if nothing after it ships. Re-measure the docs counts and the bench. Decide #observable (§8 decision 6): if no shipped example and no real model has needed it by now, it stays unshipped. If you stop here, run the clean-stop pass (§8 decision 7).

Phase 3 — composition and safety (commits 10–12)

Commit 10 — feat(contracts): refine --via composition — Cimatti normal-form obligations over bind equalities and item flows Files: ADD src/semantics/refinement.ts (step (0) plus obligations (3) and (4) with nf(C) = ¬A ∨ G; γ from bind/BindingConnector via bindingEquivalenceClasses and the directional item flows propagateValues carries; every bare connection with no flow listed under notEncoded; opt-in --connections-as-equalities printed on every verdict line). ADD examples/uav-power-budget.sysml — component contracts on battery, flightComputer, propulsion, radio, wired with bind and one flow, not bare connect. CHANGE scripts/lib/sysprose-spec.ts (row refine, --via, --connections-as-equalities), scripts/sysprose.ts, test/unit/readme.test.ts, test/campaign/cli.sysprose.test.ts, README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md, test/unit/docs-counts.test.ts (the example count, against the entry commit 8 added). Codes verification/refinement-failed, verification/unconnected-assumption, verification/refinement-undecided, verification/contract-set-vacuous; REGEN both generated docs. Tests: obligation (3) proved on the power-budget example; removing a component guarantee → refuted with a witness naming that part; strengthening one component's assumption past what its siblings guarantee → its (4) refuted; the soundness case: A₁ = G₂ = p, A₂ = G₁ = p, system ⟨true, p⟩ — bare-guarantee obligations would pass, normal-form obligations do not; the vacuity case: C₁ = ⟨true, x > 10⟩, C₂ = ⟨true, x < 5⟩, system ⟨true, x > 1000000⟩ → vacuous, never refined; a model wired with flow discharges the downstream assumption without --connections-as-equalities; a model wired with bare connect encodes zero equalities and lists N connections, never a silent pass. Gate proves: compositional obligations are exactly Cimatti's, in normal form, over equalities the model states and the tool's own value semantics already honour; nothing temporal is claimed; and an unsatisfiable antecedent can never print "refined". Depends on: 5

Commit 11 — feat(contracts): refine --via derive|refine, and bounds Files: CHANGE src/semantics/refinement.ts (derivation obligations with the measured Derive orientation); ADD boundsReport over z3 Optimize; scripts/lib/sysprose-spec.ts (row bounds, --measure, --sense, --with-requirements), scripts/sysprose.ts, src/api/index.ts (re-export boundsReport), test/unit/readme.test.ts, test/campaign/cli.sysprose.test.ts, README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md; code verification/derivation-not-refinement; REGEN both generated docs. Tests: a derived requirement with a stronger assumption does not refine, with a witness; two derived children conjoin to imply the parent; reversed direction refuted. Bounds: --measure uav.endurance with a two-sided premise range → exact min/max in minutes; --measure uav.mtow --free all → unbounded above, with the line saying require clauses are excluded, and --with-requirements → 25 kg exactly; a nonlinear objective → "optimality not established"; the νZ optimum is never beaten by the heuristic optimize. Gate proves: derivation chains are checked with the orientation the mapper actually stores; bounds are exact or say they are not, and always name which clauses were axioms. Depends on: 10

Commit 12 — feat(safety): fault-tree — minimal cut sets from contract-failure injection Files: ADD src/semantics/fault-tree.ts; CHANGE scripts/lib/sysprose-spec.ts (row fault-tree, --element, --max-order), scripts/sysprose.ts, test/unit/readme.test.ts (APP_DOORS, controls: [], no dagger, cell reads — no view yet), test/campaign/cli.sysprose.test.ts, README.md, docs/USER-GUIDE.md; REGEN docs/CLI-REFERENCE.md. CHANGE src/semantics/verification-vocabulary.ts (+ FaultHypothesis), docs/CONFORMANCE.md; code verification/single-point-of-failure; REGEN docs/DIAGNOSTIC-CODES.md.

The one genuine forward dependency in this plan, closed here rather than left. The refusal message above points at check-behaviour --from-keywords, a subcommand created in commit 14 and a flag created in commit 14b — neither of which is in this commit's dependency set, and Checkpoint C sits immediately after this commit, so a build can legitimately ship 12 with phase 4 unbuilt and advertise a command --help does not list. So the pointer is conditional: findCommand('check-behaviour') is the single-token lookup already in the spec table (scripts/lib/sysprose-spec.ts:221), and the sentence is emitted only when it resolves. When it does not, the message is "this element is a state machine; contract-level fault trees do not cover behaviour" — the refusal and the exit code are unchanged either way. Tests: {battery} is an order-1 cut set for endurance on the power-budget example and {radio} is not; --max-order 1 never claims an order-2 set absent; an undecided order-1 check forbids the no-single-point claim; a vacuous baseline reports inconclusive: contract set vacuous, never no cut set; a StateUsage passed as --element exits 2 with the pointer to check-behaviour --from-keywords, never an empty cut-set list — and the same case run with the check-behaviour row absent from COMMANDS exits 2 with the fallback sentence instead (see the Files: note); enumeration is deterministic (identical JSON twice); hierarchy expands a derived contract into an intermediate event. Gate proves: cut sets are solver decisions over the refinement obligations with the order bound stated; the tool never claims absence of failures it did not check; contract-level FTA is never offered as behavioural safety analysis. Depends on: 7, 10, 11

Checkpoint C. The ISO 26262 lane is complete: safety goal → FSR as contract refinement → cut sets, all with witnesses and stated bounds. Review the --connections-as-equalities flag with the user: given that cristoforetti-2026 §4.1 maps connect and bind alike, is the opt-in still the right default?

Phase 4 — behaviour (commits 13, 14, 14b)

Commit 13 — refactor+feat(behaviour): the pure step function, and reach Files: ADD src/semantics/mc/config.ts (MachineConfig, enabledTransitions, stepConfig, hashConfig), src/semantics/mc/explore.ts, src/semantics/mc/profile.ts. CHANGE src/semantics/execute.ts — runHierRegion's fire / enterCascade / exitTo / chaseHierCompletion closures become calls into config.ts with the same first-enabled tie-break, and chaseHierCompletion returns its budget state. CHANGE scripts/lib/sysprose-spec.ts (row reach, --max-configs), scripts/sysprose.ts, test/unit/readme.test.ts, test/campaign/cli.sysprose.test.ts, README.md, docs/USER-GUIDE.md, docs/CONFORMANCE.md; the six verification/* behaviour codes; REGEN both generated docs. Tests: the differential test — for every machine in semantics.execute*.test.ts and both examples, runStateMachine equals the left fold of stepConfig with choice = enabledTransitions(...)[0] (visited, fired, performed, store, clock); stepConfig never mutates its input. reach on FlightModes: 4 of 4 states reachable, 0 dead transitions, verification/nondeterministic-choice at autonomous where two completion transitions are enabled and the simulator takes the first — the finding that matters on this model, with no invented trigger labels. A config-bound hit yields exhaustive:false and an empty unreachable list; a 70-step completion chain hits the 64 budget, sets exhaustive:false and empties the unreachable and dead lists in exactly the same way. Gate proves: the interpreter and the checker share one step relation; a bound hit — of either kind — can never masquerade as a finding. Depends on: 3

Commit 14 — feat(behaviour): check-behaviour — safety patterns as §7.27 metadata, with vacuity Files: ADD src/semantics/mc/patterns.ts (safety by bad-prefix search: absence, universality, bounded-existence, precedence; liveness: existence and response report "inconclusive: liveness not checked in-process" until a lasso search lands and a fairness assumption is named), src/semantics/mc/atoms.ts (state X, trigger t, fires T, node N, or an expression through parseExpr). CHANGE src/semantics/verification-vocabulary.ts (+ PropertyPattern). CHANGE scripts/lib/sysprose-spec.ts (row check-behaviour, --element, --pattern, --strict-vacuity with the §2 meaning — it raises the vacuity row to an error and does not change the exit code), scripts/sysprose.ts, test/unit/readme.test.ts, test/campaign/cli.sysprose.test.ts, README.md, docs/USER-GUIDE.md; REGEN docs/CLI-REFERENCE.md. CHANGE docs/CONFORMANCE.md. Codes verification/malformed-property, verification/unknown-atom (verification/vacuous-property already exists — it is declared at commit 5 with the --strict-vacuity flag that raises it, and is reused unchanged here); REGEN docs/DIAGNOSTIC-CODES.md. Tests: each safety pattern × scope on a hand-built machine with known truth; a response carrier on a machine with a bad-prefix-free graph returns inconclusive, never pass; a @PropertyPattern carrier round-trips idempotently from the second save; an antecedent that never holds → vacuous, exit 2, with or without --strict-vacuity; --strict-vacuity additionally raises verification/vacuous-property as an error rather than an info row, and both spellings are asserted so the flag cannot quietly acquire exit semantics §2 does not give it; a pattern name outside the catalogue exits 2; the semantic profile is pinned field-by-field to the execute.ts behaviour it describes. Optionally, a PSSM Clause 9 scorecard as expectFail-style cases with PASS/DEVIATES registered — only for the intents confirmed in the specification text. Gate proves: a pass is never emitted on a partial exploration or on a property class the engine cannot decide; vacuity is always surfaced; every verdict names the semantic reading it holds under. Depends on: 7, 13

Commit 14b — feat(behaviour): #exceptional configurations become absence obligations Files: CHANGE src/semantics/mc/patterns.ts — synthesise one absence × globally obligation per element carrying #exceptional inside the machine under --element. CHANGE src/semantics/mc/atoms.ts (state X atoms from tagged StateUsages), scripts/lib/sysprose-spec.ts (check-behaviour --from-keywords, reach reporting), scripts/sysprose.ts, test/campaign/cli.sysprose.test.ts, docs/USER-GUIDE.md, docs/CONFORMANCE.md, test/unit/docs-counts.test.ts (the example count, against the entry commit 8 added). ADD codes verification/exceptional-reachable (warning), verification/exceptional-not-in-machine (info). ADD examples/uav-isr-modes.sysml with an #exceptional state, rather than touching the shipped examples whose counts are pinned; REGEN both generated docs. Tests: a machine with a tagged failsafe reachable in 3 steps → fail with the witness trace and verification/exceptional-reachable; the same machine with the enabling transition removed → pass (exhaustive) under printed bounds; --max-configs 2 on the same model → inconclusive: bound exhausted, no pass and no absence claim; a tagged state with no incoming transition → vacuous, exit 2; --strict-vacuity additionally raises verification/vacuous-property as an error, and does not change that exit code; a foreign #Exception produces the same obligation with the third-party provenance printed on the verdict line; #exceptional on an element outside the machine → info, never a finding. Gate proves: a failure the model itself names becomes a safety obligation the explorer discharges, with the bound printed on every verdict. Review target: is there any path on which exhaustive === false reaches a pass? Depends on: 2d, 13, 14

Checkpoint D. Behaviour verdicts exist and are honest about their bounds. Decide whether z3 BMC / k-induction over guarded machines is worth a further commit, or whether the SMV export (commit 15) is the better answer for anything the explicit engine cannot settle.

Phase 5 — external engines and the closing pass (commits 15–16)

Commit 15 — feat(export): smt2, OCRA, SMV and Lean export; certificate-import; cross-check Files: ADD src/semantics/export/{smt2,ocra,smv,lean}.ts, src/api/certificates.ts, scripts/lib/external-tools.ts. CHANGE scripts/lib/sysprose-spec.ts (rows export and certificate-import, --format, --out, --cross-check, --from), scripts/sysprose.ts, src/api/index.ts (re-export importCertificate), test/unit/readme.test.ts, test/campaign/cli.sysprose.test.ts, README.md, docs/USER-GUIDE.md; REGEN docs/CLI-REFERENCE.md. CHANGE docs/CONFORMANCE.md. Codes verification/export-unsupported-construct, verification/trace-mismatch, verification/certificate-mismatch, verification/certificate-unparsed; REGEN docs/DIAGNOSTIC-CODES.md. Tests: the smt2 export is byte-stable across two processes (the qualified-name keying test); every obligation appears as a :named assertion; the in-process verdict equals the verdict of feeding the export back through fromString; --cross-check against the local z3 5.0.0 binary on PATH agrees, and a synthetic disagreement is reported as inconclusive; --cross-check cvc5 reports inconclusive: cvc5 not installed with the command to run, because there is no cvc5 binary on PATH (§6); a fake ocra shim on PATH yields a pass quoting the shim's own verdict line, garbage output yields "inconclusive: unparsed tool output"; a Lean log with sorry or an extra axiom → inconclusive naming the axiom; an nuXmv -bmc transcript imports as "no violation within k", never proved; an absent tool exits 2 with the files written. Gate proves: the obligation set is portable and independently re-checkable; an external claim enters the model only through a parser that checked tool, outcome, axioms and obligation digest; nothing in src/ imports child_process. Depends on: 5, 10

Commit 16 — feat(app)+docs: evidence in the views, the honesty pass, and every number re-measured Files: ADD src/diagram/contracts-table.ts (buildContractsTable, sibling of buildRequirementsTable) and the Contracts view — a NEW view kind. It is registered by adding 'contracts' to the ViewKind union in src/diagram/types.ts:17 (16 members today, 'general' … 'regroup') and a tb-view-contracts toolbar button; src/ui/store.ts only imports the type (:137, :243, :366) and has no union to edit, and docs-counts.test.ts has no editable view-kind claim — its viewKindCount() reads /export type ViewKind =([\s\S]*?);/ out of src/diagram/types.ts and counts the literals, so nothing in the test file changes. The three claims that DO move are prose: docs/FEATURE-PARITY.md:25 ((all 16 \tb-view-*`)) and :124 (**16 diagram view kinds**), and docs/USER-GUIDE.md`:41 ("gives you back 16 views"). CHANGE docs/FEATURE-PARITY.md and test/e2e/view-switching.spec.ts (which enumerates the tb-view-* ids). CHANGE src/ui/panels/Properties.tsx (evidence chip: current / stale / none; the keywords on the selected element with what each resolves to), src/ui/store.ts (memoised digest keyed on model.rev; a "prove in the terminal" hint with the exact command when crossOriginIsolated is false). CHANGE test/unit/claims.test.ts (below). CHANGE docs/USER-GUIDE.md (the verdict table: claim → engine → exact condition → exit code; the limits register), docs/CONFORMANCE.md (which standard vocabulary is read and written, the §8.4.17 deviation, the four-facet keyword table, the external-tool interop probe result), docs/AGENT-AUTHORING-CAMPAIGN.md (the L8 suite row, known limitations), test/unit/docs-counts.test.ts, architecture diagrams per the refresh rule. ADD scripts/pilot-write-roundtrip.ts fixture change — the interop probe of §3.10 pushes a verdict-bearing model (a verdict facet plus an @SysproseVerification::Evidence carrier) instead of buildSampleModel.

The claims guard, specified. claims.test.ts scans the whole tree with a SKIP_FILES allow-list, and the reserved words already occur widely in ordinary prose. Measured at f1cd587 by replicating the guard's own walk exactly (SKIP_DIRS, the six SKIP_FILES entries at claims.test.ts:50-56, the TEXT_EXT filter) over its 577-file scan set, case-sensitive whole-word occurrences, excluding this document: 77 safe, 46 correct, 19 verified, spread over 79 files. So reserving bare words turns the gate red on well over a hundred pre-existing lines. The guard therefore reserves sentence forms, not words, and the sentence form is subject-scoped: /\b(sysprose|the (tool|model|property|requirement|obligation|proof|clause|verdict|result|architecture|system))\s+(is|are|was|were|has been|have been)\s+(verified|correct|safe)\b/i and /\b(deadlock[- ]free|realizable)\b/i, with explicit allowances for hyphenated compounds (cycle-safe, no-op-safe, type-safe, NCName-safe), for the Verified By / verifiedBy column identifiers, and for "verified" used of a probe or a test ("verified against", "verified:").

Why subject-scoped, measured rather than assumed. The unscoped form — /\b(is|are|was|were|has been|have been|proven)\s+(verified|correct|safe)\b/i with those same allowances — was run over that same 577-file scan set at f1cd587 and fires on 14 pre-existing lines, none of them a claim about this tool — re-measured by the orchestrator at f1cd587 over the guard's own walk with negated() applied, and this is the list it returned: scripts/lib/exit.ts:42; src/collab/index.ts:5; src/diagram/requirements-table.ts:135; src/semantics/simulate.ts:21; src/ui/commands.ts:7 and :135; src/ui/store.ts:234; test/conformance/corpus.test.ts:9; docs/AGENT-AUTHORING-CAMPAIGN.md:1357; docs/TEST-REPORT.md:579; docs/UI-ROADMAP.md:122; docs/USER-GUIDE.md:113; docs/architecture/08-adversarial-review.md:369 and :488. The subject-scoped form fires on 0 of them, re-measured the same way. The price, recorded as a limit rather than hidden: a pronoun subject slips through — "it is safe" is not caught — which is why it is deliberately absent from the subject list (that one alternative alone puts corpus.test.ts:9 back). The guard catches the sentence a reader would quote against us, not every English sentence containing the word; the MUST-NEVER list (§Summary) is the rule, and this is its machine-checkable half. Commit 16 is budgeted for a measured 0 hits, not an assumed one. The scan extends to src/semantics/engines/**, src/semantics/mc/**, src/semantics/keywords.ts, src/semantics/verification-vocabulary.ts and src/api/verification.ts; proved must sit within the negation window of unsat, negation, z3 or kernel; consistent must be followed by "within scope" or "over the N encoded"; and the words standard, SysML v2 and conformant are reserved within the negation window of Exception, Observable, precondition and postcondition, outside the explicit "not standard" rows of docs/CONFORMANCE.md. Commit 0 adds docs/04-formal-verification-plan.md to SKIP_FILES, alongside claims.test.ts and CLAUDE.md, for the same reason those two are there: this document has to quote the banned forms verbatim in order to ban them. It is not in the list today, and today's guard does not fire on it; without the entry the guard would fire on this file once commit 16 lands the new sentence forms. Commit 16 only re-checks that the entry is still there and still carries its reason.

Tests: plant "verified by z3" in a fixture doc → the guard fails; "not verified" passes; plant "the standard #Exception keyword" → the guard fails, "#Exception is not standard" passes. docs-counts green with every number measured, not quoted: rules 25; codes (56 + the new verification/* families); fixtures (81 + L8-evidence-stale + the L4 subject case); examples 6 if 14b shipped, 5 if it did not — the 2 shipped plus uav-isr-verification (8), contract-authoring-prompts (9), uav-power-budget (10), plus uav-isr-modes (14b); since the full plan includes 14b, the full-plan figure is 6, and it is measured with readdirSync('examples'), never quoted; view kinds (+1 for Contracts, measured off src/diagram/types.ts); and the two CLAIMS entries added at commit 8 — the subcommand count against COMMANDS.length and the example count against readdirSync('examples') — re-measured here. The interop probe (§3.10) runs offline against createServer() in CI and against SYSMLV2_PILOT_URL on demand; whatever the live result is, it is written into docs/CONFORMANCE.md — a failure is recorded as a failure, not deferred. Full gate plus npm run test:e2e. Gate proves: every sentence the surface prints or documents is one the code can make true; the reserved forms cannot come back through a doc edit; the app never shows a verdict it did not compute; and every count in every doc was measured in this commit. Depends on: 0, 1, 2a–2d, 3–15 (every commit in the plan)

5. Verification of the verifier

Eight mechanisms, each a test that fails loudly rather than a convention.

Known-answer models. An L8 suite corpus where the answer is known by construction: mtow <= 25 with mtow >= 30 is unsatisfiable with a two-element core; x == x is a tautology; assume { x > 1 } require { x < 0 } with axiom x == 2 is vacuous; the two-component mutual-support model (A₁ = G₂ = p, A₂ = G₁ = p) must fail refinement under normal form; the contradictory-sibling model (C₁ = ⟨true, x > 10⟩, C₂ = ⟨true, x < 5⟩) must report vacuous, never refined and never "no cut set". Each case carries a golden verdict list, so a regression shows up as a diff, not as a wrong verdict nobody noticed.

The differential gate (commit 5) — and what it does not prove. With --free none the SMT engine answers the same question checkConstraints answers, so it must give the same answer on every encodable relation across the whole fixture corpus and both examples, including the unknown row and the strict-boundary rule fixed in d568a1f. But the gate compares two consumers of one gatherer: encodability "is the same gate the numeric surface applies, because it calls the same functions". A relation neither surface gathers — a construct the shared parseRelationBody drops, a feature chain that fails to resolve — is silently absent from both, both say "nothing to report", and the gate is green. So the differential gate proves the two ENGINES agree on the relations the shared gatherer produced. It establishes nothing about a relation the gatherer dropped. What earns proved is the negation-UNSAT under a satisfiable axiom set with a two-sided domain, plus the relation census.

The relation census (commit 5). Every constraint-bearing element in the user model is accounted for as encoded, refused-with-reason, or unsupported-with-code, and the counts are asserted equal to the element census. A case whose relation silently disappears fails the gate. This is the counter-measure to the blind spot above, and it is the one the first draft did not have.

Witness re-evaluation. Every SAT model is substituted back through evaluate with the same scope shape checkConstraints uses before it is printed. A witness the in-process evaluator does not confirm is reported as "inconclusive: witness not confirmed", never as a violation. This catches encoder bugs — a wrong unit factor, a sign error, a mis-scaled offset — in the direction that matters. Note its limit, exposed by the cruisePower = -1 W case: re-evaluation confirms arithmetic, not physical admissibility, which is why the unbounded-free-variable rule (§3.4) is a separate and blocking check.

Mutation. The behaviour differential test (commit 13) is a mutation test in disguise: the fold of stepConfig must reproduce runStateMachine exactly, so any change to the interpreter that the extracted step function does not mirror fails immediately. For the SMT layer, single-field mutations of a case (flip >= to > at an exact boundary; change 18.5 to 18.6) must move the verdict in the expected direction and must move the model digest.

Two-solver agreement, honestly scoped. export --format smt2 --cross-check <tool> re-checks the exported obligation with a second engine. On this machine z3 5.0.0 is on PATH and cvc5 is not: which cvc5 finds nothing, and cvc5 1.3.4 exists only as a Python package in ~/.venvs/quant, which a PATH-and-version probe cannot see. So the cross-check that runs today is the z3 binary against z3 WASM, which catches export defects but is not two independent engines; --cross-check cvc5 reports inconclusive: cvc5 not installed with the command to run, and the two-engine claim is not made until a binary exists. A disagreement is always reported as inconclusive with both verdicts named — the tool never picks a winner. The export itself is tested to be what the in-process solver saw, by feeding it back through fromString and comparing verdicts, and to be byte-stable across processes (the test that catches any residual dependence on UUID element ids).

The interoperability ratchet. A case holding #Exception, #Observable, #precondition, #postcondition, a qualified #SysproseVerification::exceptional and a misspelt #precondtion, on six element kinds, must parse with zero diagnostics and round-trip idempotently from the second save, forever. It is what stops a future vocabulary commit from making Sysprose the only tool that can read its own files.

The campaign ratchet and the claims guard. The existing "an error cannot become OK by saving" ratchet is the L6 round-trip invariant (test/campaign/invariants.test.ts:201) — a named list of cases whose fault survives parse → serialize → check — not the golden/repair pair. Commit 2a's serializer change is the most likely thing in this plan to disturb it, so 2a re-runs it and re-records any movement with a reason. The L8 suite adds its own ratchet in the same spirit: a golden verdict may become more conservative without ceremony and may never become less conservative without an explicit re-record. The claims guard (commit 16) scans every new string and document for the reserved sentence forms; the guard is itself verified by planting a violating sentence in a fixture doc and asserting the test fails. And the CI job that runs --engine auto with SYSPROSE_NO_Z3=1 and asserts exit 2 means the honest-absence path is executed on every push — the single most likely thing to rot into a silent green, exercised continuously.

6. Risks, semantic traps and non-goals

Non-goals (deliberate)

1. No unbounded proof in TypeScript. The in-process behaviour engine decides only the finite abstraction it exhaustively explored. Anything unbounded goes to z3 k-induction or to an SMV export, and the report names which.
2. No event pool, deferred events or PSSM completion events. triggerEquals is an exact match and completion chasing is bounded at 64. The profile prints deferredEvents: 'none' and a model needing them gets verification/behaviour-unsupported-construct, never a verdict.
3. No dense time in-process. after(n) is a discrete clock; real-time patterns with sub-tick bounds are export-only.
4. No liveness in-process. existence and response are inconclusive until a lasso search lands and a fairness assumption is named.
5. No reactive realizability. consistency decides satisfiability of static contracts. katis-2022 and larraz-tinelli-2022 are about a different question; the word realizable is reserved by the claims guard.
6. No kernel-checked proofs in-process. z3 is trusted as a solver. The vocabulary is "proved by z3 (negation unsat)", never "kernel-checked" — that phrase is reserved for an imported Lean result whose axiom set was parsed.
7. No LLM inside the tool. Property authoring is the agent's job, guided by #prompt; the tool supplies the dictionary, the template, gate 0, the four gates and the back-translation. danso-2026 sets the bar and the gates are the answer to it.
8. No invented syntax. Properties, evidence, fault hypotheses and temporal patterns are §7.27 metadata over a shipped SysproseVerification package, exactly as #prompt is a keyword over SysproseStatements. Two of the four keywords put to this plan are refused outright because the standard already expresses them, and one of the two remaining is held (§2.1).
9. No in-browser solver in this plan. z3 WASM needs SharedArrayBuffer, i.e. COOP/COEP headers GitHub Pages cannot set. The app reads evidence and says "prove in the terminal" with the exact command. The coi-serviceworker workaround is a later decision, not a promise — and cross-origin isolation (COOP: same-origin + COEP: require-corp) would also break the optional Google Drive feature's sign-in popup and its docs.google.com Picker iframe, so in-browser z3 and Google sign-in constrain each other; that too is a decision for later, not this plan's.

The one declared deviation from the standard

§8.4.17 — a RequirementCheck with a false assumption. Part 1 §9.2.14.2.8 gives the RequirementCheck result as allTrue(assumptions) implies allTrue(constraints) (the shipped Systems Library/Requirements.sysml spells it with the call parentheses), so a requirement whose assumption is false is true under the standard's own semantics. This tool reports vacuous ⇒ inconclusive ⇒ exit 2 instead, because a requirement discharged by an unsatisfiable antecedent tells an engineer nothing and is the classic way a requirement set passes while meaning nothing. This is a deviation, not an interpretation, and it is recorded as one in docs/CONFORMANCE.md with the clause number beside it. --strict-vacuity makes it louder; nothing makes it agree with the standard.

Semantic traps, and how each is reported

Expected yield on a real model

Nothing in this lane promises that a real requirement set will be decidable. On examples/uav-isr.sysml — the best case that exists, a model written by the same hands as the tool — 0 of 2 guarantees are refused and both are encodable. That number is not a forecast. A requirement set drawn from a programme will contain prose-only requirements (no formal clause), temporal ones (gate 0 refuses them), °C arithmetic and offset scales (refused), collection-valued and enum comparisons (unsupported-construct), and nonlinear obligations that time out. A user approving this lane should expect the first honest run on a real model to land a substantial fraction in no-formal-clause and not-encodable, and should treat obligations --missing as the deliverable that measures it. The first thing to do after commit 2c is to run it on a real requirement set and record the histogram in the ledger; if the encodable fraction is small, that is information about the model and about this plan's value, and it arrives before the SMT engine is built rather than after.

Performance, the gate budget, and licence limits

z3 WASM: init plus three checks measured once at 343 ms in a Node 22 process — init alone was not timed separately, and z3-solver is not in node_modules today, so the figure is re-measured at commit 4 and registered. The WASM asset is tens of megabytes, dynamically imported and excluded from the browser bundle.

The baseline the budget moves from, measured rather than deferred. npx vitest run at f1cd587 on this machine: 192.74 s wall clock, 129 files, 2245 tests (/usr/bin/time, one run, the full unit + integration + conformance + campaign suite; npm run test:e2e is separate and not in this figure). That number is machine-dependent — it is a developer VM, not CI — so it is a baseline to move from, not a threshold to defend in the abstract; what is portable is the ratio, and every re-measurement is taken on the machine that took the previous one.

The gate budget, because nobody costed it. This plan adds, under "full gate on every commit": a differential gate over 81 fixtures + 2 examples, a relation census over the same, a fault-tree enumeration of Σ C(n,k) solver calls, and an explorer defaulting to 10 000 configurations. Vitest runs spec files in parallel workers, and each worker that touches z3 pays its own WASM init. Therefore:

• The wall-clock budget for npm test is 192.74 s + 25 % ≈ 241 s, anchored on the measured baseline above and re-registered at commit 5 with the same command on the same machine. A commit that exceeds it either explains itself in its message or moves the solver-touching suites behind npm run test:smt — a script the full gate still runs and the per-commit gate may skip. A budget with no baseline and no escape hatch is not a budget; both are now stated, and the escape hatch is the redesign trigger, not a silent slide.
• Per-suite timeout policy: every solver-touching suite declares an explicit vitest timeout; no solver call is unbounded; the default per-check timeout is 5000 ms and the fault-tree and explorer bounds are as documented.
• z3 WASM under worker parallelism is treated as unproven until commit 4 measures it. Commit 4 runs the SMT suites under the default worker pool and under a single fork, comparing verdicts and wall clock, with smt.random_seed fixed so a determinism failure is a real one and not a seed. If the WASM instance turns out not to be worker-safe, the SMT suites are pinned to a single worker and the cost is recorded — a budget decision, not a correctness one.

Core minimisation costs at most one extra check per core member; fault-tree enumeration prints its check count; explicit-state exploration defaults to 10 000 configurations and depth 200 and prints the frontier size when a bound is hit.

External tools: ocra and nuXmv are free but not open source (FBK licence) and are never bundled; Kind 2 is open; z3 is MIT — recorded in docs/LICENSES.md. Not installed on this machine today: nuXmv, NuSMV, SPIN, UPPAAL, Kind 2, Alloy, TLA+ tools, the cvc5 binary (which cvc5 finds nothing; the 1.3.4 Python package in ~/.venvs/quant is invisible to a PATH-and-version probe), and z3-solver itself until commit 4. z3 5.0.0 is on PATH. Every one of those absences is an exit 2 with the files written and the command to run printed.

7. Literature map

Shelves 11_formal_methods_foundations_and_practice and 12_model_verification_sysml_and_mbse in /media/sf_Projects/SystemsPerspectiveBib; reading paths H, K, L, M in review/Reading_Guide_2026-09-05.md.

The re-targeting caveat, stated once and applying to every row below. Every document cited here except cristoforetti-2026 was written for a pre-SysML-v2 target: UML/SysML v1 (barbau-bock-2020, dania-clavel-2016, clariso-2020, wu-farrell-2021, omg-pssm-1.0-2019), AADL/Lustre (cofer-2012, stewart-2021), or timed automata (vogel-2022, peres-ghazel-2023). The shelf's own reading guide says so: path H ends "treat each paper as a recipe to re-target, not a drop-in", and path K adds "the safety line stops at SysML v1". Each is a recipe to re-target, and where this plan re-targets one, the divergence is named in that feature's own §3.x section.

Read before implementing each phase. Phase 0: omg-sysml-2.0-part1-2026 §7.21, §7.24, §7.27 (the normative text this lane reads and writes), almeida-2024 (which readings are settled — the unsupported-construct register comes straight out of it), cofer-miller-2014 (what an evidence record must carry). Phase 1: filipovikj-2018 (the SMT-first argument), dania-clavel-2016 (the many-sorted encoding, undefinedness kept explicit, and the negation-UNSAT formulation), kupferman-vardi-2003 (vacuity), wu-farrell-2021 (cores and their minimisation). Phase 2: mavridou-2026 and ma-2026 (the FRETish fields, which three are mandatory, and the dictionary), danso-2026 (the acceptance bar the gates answer), clariso-2020 (what a certificate is and how staleness should behave). Phase 3: cimatti-2015 §4 and Theorem 1 — read the normal-form definition before writing a line of refinement.ts, then cofer-2012 and westman-2013, then bozzano-2014 and stewart-2021 for the cut-set construction. Phase 4: andre-2023 §2.6 (the decision list that becomes the profile record), omg-pssm-1.0-2019 Clause 9, vogel-2022 (patterns, scopes, and which of them are liveness). Phase 5: cristoforetti-2026 (the component mapping), fbk-ocra-2.1.0-2021 (the Othello grammar), barbau-bock-2020 (SMT-LIB conventions).

Four corrections to the shelf's use, recorded so they do not propagate.

1. khelifati-2025 is Combining SysML V2 and BIP to Model and Verify CPS Interactions — an interaction-verification mapping, not a study of native SysML v2 expression evaluation. It is cited here (if at all) as a neighbouring approach, never as the baseline for checkConstraints.
2. benavides-2010 is a feature-model analysis survey and does not back an optimisation feature over a SysML constraint system; it is dropped.
3. seidewitz-2020 is the metasemantic protocol for language extension. Measured: the words "metadata" and "annotation" occur 0 times in it. It therefore does not support the sentence "tool-specific data belongs in metadata" — that sentence is the specification's, and its citation is omg-sysml-2.0-part1-2026 §7.27. seidewitz-2020 is kept only for the extension discipline. Earlier drafts of this plan and of the annotation design both mis-attributed it, in the same way.
4. cofer-2012 does not formulate the obligation as A ∧ ¬G UNSAT; its goal form is ⊨ G(H(As) ⇒ Ps), discharged by k-induction over Lustre. The negation-UNSAT formulation this plan uses is dania-clavel-2016's.

8. Open decisions for the user

1. Should --allow-inconclusive exist at all, and how far should it reach? The strict contract (any inconclusive ⇒ exit 2) is what stops a missing solver turning CI green. The flag is an escape hatch for a team that wants a green build while a nonlinear obligation times out. The danger nobody named in review is the flag's scope: unscoped, it also forgives a solver that was never installed, and it forgives a real violation that got mislabelled axioms inconsistent. Recommended default: ship the flag, scoped. It lowers 2 → 0 only for verification/timeout and verification/unsupported-construct. It never lowers verification/tool-absent, never lowers verification/vacuous, never lowers verification/method-not-performed, never lowers design-admitted, and never wins over a violation. The summary prints the inconclusive count first and names which inconclusives were forgiven. Revisit after a month of real use. And the flag that is deliberately NOT shipped: a team wanting a green build over a verification case whose method the tool did not perform would need a separate --allow-unperformed. This plan does not ship one, and no commit gate in §4 forgives verification/method-not-performed. If you want it, say so and it becomes its own decision — it is not something --allow-inconclusive quietly grows into.

2. Should a connection between ports ever be read as an equality? The specification does not say it is one, and propagateValues does not treat a bare connect as one — so the default is to refuse and list it. But examples/uav-isr.sysml wires nine connections and zero binds, so a refinement check on the shipped example encodes nothing until the model is edited. Counter-evidence to weigh: cristoforetti-2026 §4.1 — the one published SysML v2 → OCRA path — translates connect and bind alike into OCRA ports and connections, and Cimatti's γ is by definition the connection-and-delegation assertion. So this plan's refusal is a stricter reading than the published path takes, not a consensus, and that is the strongest argument for shipping --connections-as-equalities rather than only refusing. Recommended default: keep the refusal as the default and ship the opt-in, noting that γ already includes item flows so a model wired with flow is checkable as-is, and ship examples/uav-power-budget.sysml using bind. If you would rather the shipped ISR example be checkable, the alternative is to add bind statements to it — say the word and that becomes part of commit 10.

3. z3 as an optional dependency, or a hard one? Optional keeps the browser bundle clean and makes the absent path a real tested state. But the reasoning in the first draft was wrong: npm installs optionalDependencies BY DEFAULT, and skips them only on a platform/engine failure or with --omit=optional / --no-optional. A fresh npm ci would have z3-solver, so absence is not the default and must be forced. Recommended default: optional, with the honest-absence path exercised by the CI job that sets SYSPROSE_NO_Z3=1 (and, for a genuine no-install check, npm ci --omit=optional) — not by imagining that a fresh clone lacks the package.

4. Which phases do you actually want — and what does each cost? The first draft asked this and gave no cost for any answer, so it could not be answered as posed. The estimates below are commit counts and regression surfaces, which is what this project actually spends; the phase-0 range is the one to trust least until commit 2a's corpus diff is measured.

Recommended default: commit to phases 0–2 (twelve code commits: 1, 2a–2d, 3–9, plus the doc-only commit 0), then reassess at Checkpoint B. Phase 3 is the highest-value next block for your domain. Phase 4 answers questions the shipped examples barely pose — a four-state and a three-state trigger-less toy — so it is worth doing after you have a model whose modes matter.

5. Does #prompt guidance for property authoring belong in the shipped examples? Putting authoring guidance into examples/uav-isr.sysml makes the agent loop self-documenting, but it changes the example's element counts, which several tests and docs pin. Recommended default: a separate examples/contract-authoring-prompts.sysml, so the shipped ISR and vehicle models stay exactly as they are.

6. Should Sysprose ship the #exceptional keyword, and what about #observable? The specification is genuinely silent on both — "exception" occurs 0 times in Part 1, "observable" twice in one narrative sentence — and §7.27.4's own example (#situation occurrence def Failure;) shows a failure marker being user-defined, so shipping is sanctioned. But a shipped metadata def the tool writes into user files is a compatibility commitment: withdrawing it later turns a user's file into verification/keyword-names-nothing. Recommended default: ship the reader, the resolver and the alias table (commit 2d), ship #exceptional, and HOLD #observable. #exceptional earns its entry at commit 14b, where it turns a hand-written safety question into an absence × globally obligation — one of the four patterns the engine can actually decide — with a witness trace and a printed bound. #observable discharges nothing; its entire output would be one info verdict and an atom filter, and nothing in this plan depends on it. Its design is written (§3.12) and it is one commit away whenever a shipped example needs it.

7. If you stop at a checkpoint, what happens to the docs? At Checkpoint B the §3 table has twelve rows, and six of them — refine, bounds, reach, check-behaviour, fault-tree, and export / certificate-import — do not exist. docs/CLI-REFERENCE.md is generated from the spec table, so it stays honest on its own; the README capability table and docs/USER-GUIDE.md are prose and would not. The clean-stop pass: delete the unshipped rows from the §3 table into a short "Not built" list at the end of §3, with the commit numbers that would build them; regenerate docs/CLI-REFERENCE.md; trim the README capability table and the USER-GUIDE sections to what COMMANDS actually holds — both are guarded, so readme.test.ts:315 and user-guide.test.ts:226 fail loudly if you do not; mark the unshipped verification/* codes as reserved-not-emitted in docs/DIAGNOSTIC-CODES.md; and record the stop point and the reason in the ledger. Recommended default: budget one commit for the clean-stop pass at whichever checkpoint you stop at, and treat it as part of stopping, not as optional tidying. A plan that advertises six tools it does not have is the same defect this document exists to prevent, arriving through the back door.