Sysprose — Conformance Scorecard

Self-assessment, not certification. This scorecard measures Sysprose against the OMG SysML v2 / KerML / API & Services specifications as read by this project. Sysprose is a candidate implementation; it has not been certified or conformance-tested by the OMG or anyone else, and nothing here is a conformance claim.

Generated: 2026-07-01; suite, corpus and parse-rate figures re-measured 2026-09-04. Numbers below are captured from a live test run, not asserted from memory. Reproduce with the commands in the last section.

This is an honest conformance scorecard for the clean-room SysML v2 / KerML modeler. It maps the project's automated evidence onto the OMG SysML v2 standard family and states, candidly, what is and is not covered. Every pillar is a faithful, load-bearing subset — see docs/TEST-REPORT.md §8 for the pillar verdicts and docs/LICENSES.md for the clean-room / consulted-spec record.

Consulted specifications (implemented from, never copied — see docs/LICENSES.md): OMG SysML v2 v2.0, OMG KerML v1.0, OMG Systems Modeling API & Services v1.0 (REST/HTTP PSM, element-graph JSON, Query language), OASIS OSLC Systems Modeling Language v2.0 + OSLC Core 3.0, W3C RDF 1.1 (Turtle / XML Syntax) and JSON-LD 1.1, OpenAPI 3.1.

Headline numbers

Dimension Result
Conformance suite (test/conformance) 71 passed / 0 failed across 4 files
Full automated suite 4688 passed / 0 failed / 0 skipped across 157 files + 217 E2E across 84 spec files = 4905 green (measured 2026-10-15)
Command-line surface 22 subcommands in one spec table, over 6 shipped example models, each of which is verified on every push — both figures measured off the tree by test/unit/docs-counts.test.ts, never quoted
OMG element-graph JSON Schema validity of our api-json exports PASS (all standard models, import→export stable)
Reference XMI standard libraries ingested 38,761 elements across 98 packages (from 109,673 source elements)
Real .kerml / .sysml corpus parse rate 100 % (94 / 94 files, 0 parse errors)
OMG REST endpoints validated against the OpenAPI 3.1 schema 10 / 10 live endpoints (server: 25 paths / 29 operations / 18 schemas)
OSLC Core structural conformance 8 / 8 structural checks + 11 full-shape checks (catalog / provider / query / resource / oslc:ResourceShape + Turtle / RDF-XML / JSON-LD)
Interop — self round-trip over HTTP (test/interop) PASS — PilotApiClient push→pull preserves the 13-element pilot model (element set + endpoints + query), and the verdict-bearing fixture's carrier, both verdict cells and its record string character for character
Interop — LIVE round-trip vs. the real OMG pilot (SYSMLV2_PILOT_URL) RUN, and mixed — read of 300 live elements and a Package write round-trip PASS (2026-07-02); the verdict-bearing write of 2026-09-09 is refused as written (four defects of our own dialect) and, once those are repaired in the probe, accepted with the structure intact and every tool-local value dropped — the evidence's contents do not survive. §6.1 has the measurement, and names the one row it could not take.

1. Round-trip invariants — roundtrip.test.ts (25 tests)

Each of three standard models — buildSampleModel(), examples/vehicle.sysml, and the bundled ISQ + SI library packages — is asserted to uphold the cross-format invariants a conformant tool must preserve. The preserved identity is the order-independent multiset of metaclass @@ qualifiedName.

Invariant Holds Notes
Endpoint integrity — every element has an id, no relationship endpoint dangles PASS (3/3 models) integrityViolations() empty for every model.
model-json round-trip — Model.fromJSON(m.toJSON()).toJSON() deep-equals m.toJSON() PASS (3/3) Loss-less native snapshot.
api-json round-trip — importModel(exportModel(m,'api-json')) preserves the element set PASS (3/3) Element-graph interchange is set-stable.
api-json schema validity — export validates against the OMG element-graph JSON Schema (draft 2020-12) PASS (3/3) See §2.
api-json import→export stability — the rebuilt export also validates PASS (3/3) Interchange is idempotent under the schema.
textual round-trip — parseModel(serializeModel(m)) reproduces the element set PASS (3/3) Full-fidelity: the serializer emits every specialization relationship (: Type, :>, :>>, ::>) and the mapper reconstructs the FeatureTyping element on parse, so the ISQ+SI library model round-trips textually too (the former declared subset boundary is closed). Requirement-clause bodies now survive it, and the writer emits the constraint keyword the published grammar needs to read a clause as a DECLARATION rather than a reference — see the corpus byte diff below.

Four additional schema-guard tests assert the element-graph schema rejects malformed documents (missing elements, missing @id, missing @type) and accepts a minimal well-formed graph.

Corpus byte diff of the writer (measured 2026-09-06, across the requirement-clause commit b16a457 and over the corpus as it stood there). serializeModel was run over 236 files — examples/, the 140 .sysml files the fixture corpus held at that commit, and the 94 files of ~/.stdlib-src/sysml.library — before and after the requirement-clause fix. The corpus has since grown (141 fixture files, 237 in all, after the requirement-subject commit added one); the figures below are the ones that experiment measured and are not re-derived by any later commit. Output moves on 29 of them (2 examples, 11 fixtures, 16 standard-library files), +2,817 bytes in total: 46 clause lines gain the constraint keyword, 3 regain a private, and 9 of the 29 also gain clause-body content that was previously deleted on every save — doc notes and nested members on TradeStudies, CausationConnections, SpatialItems, MeasurementReferences, DerivationConnections, Cases, Items, Requirements and VerificationCases (a tenth, Views.sysml, regains a multiplicity rather than a body). The other 207 files are byte-identical.

The keyword is written only where the clause DECLARES: the published grammar's first RequirementConstraintUsage alternative is an owned reference subsetting, so require sat; names an existing constraint and must not become require constraint sat;. Checked over the wider OMG release-model corpus as well (~/.stdlib-src/sysml/src, 251 files, 50 of which move): across all 487 files, no reference-form clause line is rewritten into a declaration. Reproduce by serializing the same 487 files across b16a457 — the corpus at that commit, not today's — and the round-trip and campaign suites cover the result.

2. Interchange — OMG element-graph JSON

3. API & Services PSM — api-contract.test.ts (22 tests)

The REST surface is now a networked HTTP/Express server (src/server, started on an ephemeral port under // @vitest-environment node). For each representative endpoint the live response body is validated with Ajv + ajv-formats against the response schema declared for that endpoint in the served OpenAPI 3.1.1 document — proving the API and its own description are self-consistent.

Endpoints validated (10/10):

The served OpenAPI document exposes 25 paths / 29 operations / 18 component schemas.

4. OSLC PSM — oslc-conformance.test.ts (8 tests)

OSLC Core 3.0 structural conformance of the linked-data facade (src/api/oslc.ts served via src/server, with a dependency-free RDF serializer src/server/rdf.ts):

5. Corpus parse conformance — corpus.test.ts (16 tests)

Known real-world corpus files parse with 0 errors, produce non-empty models, and are dangling-free (all endpoints resolve in-model), confirming the textual front-end and model builder agree with the interchange invariants.

6. Interop / round-trip — test/interop, scripts/pilot-roundtrip.ts

Our PilotApiClient (src/interop) speaks the OMG Systems Modeling API & Services REST protocol directly over fetch: it discovers projects/branches, POSTs OMG change records to a branch head to create a commit, and pulls the paginated OMG element-graph back, reconstructing a native Model from the @id/@type element JSON. It is a general client, not a self-test harness — the same code path drives both the self round-trip and the live-pilot adapter below.

6.1 The verdict-bearing write probe — what another tool did with our evidence (2026-09-09)

A Package surviving the wire says nothing about the two things the verification lane writes, and both of them are tool-local tags the specification does not define: a metadata RequirementMetadata { attribute verdict = "…"; } cell and an @SysproseVerification::Evidence { … } carrier holding the record (§8.2, §8.3). A conforming reader is entitled to ignore either. Whether a real one does is a fact about somebody else's server, so scripts/pilot-write-roundtrip.ts now pushes a verdict-bearing model — scripts/lib/verdict-fixture.ts, 19 elements, written by the real verify + attachEvidence path, one carrier, two verdict cells and a 1466-character record string — instead of a bare Package. It was run against the same public pilot on 2026-09-09, and this is what it measured.

Stage What was pushed Result
1 — as this tool writes it the 19 elements of ModelApi.toModelJSON(), unmodified REFUSED — POST …/commits → 500.
2 — three shape defects of our dialect repaired the same 19 elements with the metaclass name Satisfy corrected to SatisfyRequirementUsage, RequirementDefinition.text sent as a list where the specification has text : String[0..*], and the boolean MetadataUsage.annotation dropped where the specification has annotation : Annotation[0..*] STILL REFUSED — POST …/commits → 500. Stage 2 differs from stage 3 in exactly one property, so this is what isolates the fourth defect: MetadataUsage.type, which we send as a string and which the specification derives.
3 — MetadataUsage.type dropped as well the same 19 elements, type gone ACCEPTED, and the values did not come back. 19 pushed, 19 pulled. Structure preserved, re-derived by the script on every run: 19/19 ids, 19/19 metaclasses, 14/14 declaredNames, 18/18 containment (owner) edges, and the one text body returned as sent once it was a list (the pilot adds an empty text: [] to one further element — an addition of its own, not a loss of ours). Every tool-local property was dropped — value (the cell that holds each verdict string and the whole record), requirementRole, declares, expression — so the facet returned as a named, empty shell: 2 verdict cells sent / 0 back, 1466 record characters sent / 0 back, 4 record summary cells sent / 0 back.

One row this probe cannot measure, and does not pretend to. The carrier count is not comparable at stage 3. MetadataUsage.type is the only property on the wire that says an @SysproseVerification::Evidence carrier is one — it is what verdictBearingSignature reads to find carriers at all — so the very repair that got the commit accepted is the repair that makes a carrier unidentifiable, and a perfect lossless echo would have returned 0 carriers too. The script prints that row as N/A … NOT MEASURABLE rather than scoring it, and the repair is held back to its own stage for exactly this reason. What IS measured is the thing that matters more: the carrier's contents — the claim word, the engine, the model digest and the whole 1466-character record — were dropped.

Read that as it is. The pilot did not misread a Sysprose verdict, upgrade a claim or return a verdict nobody computed; it kept the model and discarded the annotation, which is exactly what a reader is entitled to do with a tag it does not know. So the interoperability of the evidence record is now measured, and the measurement is negative: today, the values a Sysprose verdict is made of do not survive a round trip through that server's API, and no claim is made that they survive any other. The four dialect defects are ours and are not fixed here — they are recorded so the next commit that touches toElementJSON has the failing shapes in hand. The offline control runs on every push (test/interop/self-roundtrip.test.ts, "round-trips a verdict facet and an evidence carrier"): the same fixture through the same client against our own server keeps the carrier, both verdict cells and the record character for character. That is a control on the fixture and on our own wire, not a second opinion about the pilot's — the carrier row above is unmeasurable on the pilot for a reason that is ours, and the offline test cannot supply the number the live run could not take.

Honest caveat. The live round-trip is exercised (above), and it is a representative exchange — 19 elements written, a bounded 300-element read — not a full-model bidirectional migration. It answers the API/JSON path only; what a foreign textual parser makes of the .sysml bytes is a different question and is untested. Also, the pilot does not support project deletion (DELETE /projects/:id → 500), so the clearly-named sysprose-interop-test-* projects each run creates — one per stage, three per run — remain on that public demo server. Point SYSMLV2_PILOT_URL at any conformant pilot to reproduce; the script re-derives every figure in the table above, structure rows included, so a re-run either reproduces it or contradicts it.

7. User-defined keywords — the mechanism, and the one vocabulary Sysprose ships

SysML v2 §7.27.1 says a metadata definition with no nested features "simply acts as a user-defined syntactic tag on the annotated element", and §7.27.4 makes the (short) name of such a definition writable as a #keyword in front of a declaration. That mechanism is what Sysprose borrows. The vocabulary carried over it is not part of the specification, and nothing in this tool describes it as if it were.

A practitioner's four-keyword vocabulary was assessed against the published specification. Two of the four are things the notation already expresses, one names a real gap that is deliberately not shipped, and one is adopted:

Facet Keyword proposed Does SysML v2 express it? The construct the specification supplies Decision
Before #precondition Yes, three ways assume constraint in a requirement body (RequirementConstraintKind = assumption, Part 1 §8.2.2.21.1); objective { assume constraint { … } } on any case, typed by Cases::Case::obj : RequirementCheck[1]; guard on a transition (TransitionPerformances::TransitionPerformance::guard) Rejected. Read the standard construct; a keyword would be redundant syntax.
After #postcondition Yes require constraint; objective { require constraint { … } }, whose subject defaults to the case result per the shipped Systems Library/Cases.sysml (subject subj default Case::result;) and is bound to the case subject per VerificationCases.sysml Rejected, for the same reason.
Valence #Exception No exception* occurs nowhere in Part 1. VerificationCases::VerdictKind::fail is a case result, not a model-authored classification of an outcome, and RiskMetadata::Risk is probability and impact. §7.27.4's own example is #situation occurrence def Failure; — the specification demonstrates a user-defined failure marker Adopted as #exceptional, over the shipped metadata def <exceptional> ExceptionalOutcome; in SysproseVerification (src/semantics/verification-vocabulary.ts). A Sysprose extension, not standard vocabulary.
Visibility #Observable No "observable" occurs twice in Part 1, both inside one narrative use-case sentence — a sentence, not a construct. out direction and flow say what crosses an interface, not which step is published; VerificationMethodKind sits on the case Held, not shipped. A metadata def written into a user's file is a compatibility commitment; this one would discharge no obligation.

What is read, and what that reading may do. contracts --keywords inventories every keyword in a file with what it resolves to — resolution is KerML full name resolution against the MetadataDefinitions in scope, with the bundled library as the namespace of last resort, which is why the library's own #moe resolves. A keyword naming nothing in scope is reported (verification/keyword-names-nothing, info); a third-party spelling this tool recognises is reported with its provenance (verification/foreign-keyword, info) and never described as standard. verification/foreign-keyword also comes from obligations --from-keywords, one row per obligation a keyword actually filed; verification/keyword-names-nothing comes from contracts --keywords alone, since a keyword naming nothing files nothing. Neither comes from anywhere else: npm run check does not judge a keyword.

What a keyword may move, and what it may never touch. A third-party #precondition / #postcondition files a premise or something to show only under obligations --from-keywords, and only on a plain constraint. It never overrules a clause role the author wrote, it can never add an axiom, and — the direction that matters as much — it can never take one away: a keyword on a calc leaves the calculation's defining equality (total == a + b) exactly where it was, because a vocabulary that could silently drop a definition out of the proof context would leave every obligation over that calculation standing on a free variable.

Measured, and pinned by test/unit/semantics.keywords.test.ts: #exceptional, #Exception, #precondition, #postcondition, #Observable, a qualified #SysproseVerification::exceptional and a misspelt #precondtion all parse with zero diagnostics on six host declarations, are stored exactly as written, and round-trip. The round trip is idempotent from the second save rather than byte-identical from arbitrary input. A keyword colliding with a hard keyword of the notation must be quoted — #derive part def A; does not parse, #'derive' does.

8. verify — one declared deviation, and two slots this tool does not bind

npm run sysprose -- verify reaches a verdict. Three things about it belong in a conformance record rather than in a release note.

8.1 The declared deviation: a requirement with a false assumption

Part 1 §9.2.14.2.8 gives the result of a RequirementCheck 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 specification's own semantics.

Sysprose reports it as vacuous ⇒ inconclusive ⇒ exit 2 instead. A requirement discharged by an antecedent that does not hold tells an engineer nothing, and it is the classic way a requirement set passes while meaning nothing. This is a deviation, not an interpretation, it is the only one in the verification lane, and no flag launders it: --allow-inconclusive is scoped to verification/timeout and verification/unsupported-construct and does not reach verification/vacuous-pass. The case is pinned in test/fixtures/verification/vacuous-assumption/ and its --allow-inconclusive twin.

8.2 The verdict slot the standard defines, and this tool does not bind

The standard's own verdict slot is VerificationCases::VerificationCase::verdict : VerdictKind {redefines result}. Sysprose does not bind it. What it writes instead — from a later commit of the verification plan — is a metadata RequirementMetadata { attribute verdict = "…"; } facet, which is a tool-local, unbound tag holding a quoted string: RequirementMetadata has 0 occurrences in Part 1, which has only DerivedRequirementMetadata and OriginalRequirementMetadata, and src/semantics/requirements.ts says in its own header that the identifier resolves to nothing. A conforming reader is entitled to ignore that line entirely, and nothing obliges it to interpret the string. The value list mirrors the library's VerdictKind literals; it is not a VerdictKind reference.

That facet is written for two claims only — proved ⇒ pass, refuted ⇒ fail — and everything else, holds-at-values included, writes inconclusive.

8.2b The one standard slot this lane writes, and the gate in front of it

@VerificationCases::VerificationMethod { attribute kind = analyze; } on a verification case is standard, and it is the only standard element this lane writes. evidence-attach puts it on a case that stated no method, so the file records which method the computed verdict was reached under instead of leaving a reader to assume one; a case that already states a method is left exactly as written.

The gate that annotation exists for. VerificationMethod carries kind : VerificationMethodKind [1..*], so a case may legitimately say kind = (analyze, test). Sysprose performs analysis and nothing else. A case whose list contains analyze, or which states no method at all, is judged on the analyze part and reports every other kind as not performed. A case with no analyze in its list is not judged at all: verification/method-not-performed, inconclusive, exit 2 — never exit 1, because an unjudged case is not a refutation — and --allow-inconclusive does not reach it, because §2 scopes that flag to verification/timeout and verification/unsupported-construct. A kind spelling this tool does not recognise is reported by name and treated as not analyze. The shipped examples/uav-isr-verification.sysml carries all three shapes and is exit 2 with every obligation in it discharged, and a job on every push (.github/workflows/verify-examples.yml, method-gate) asserts that exit code with and without --allow-inconclusive, against the control of the same file narrowed to its analyze case, which is exit 0.

Every spelling of the method is read, because the arm that judges is the arm a case falls into when none is found. The definition may be named in declaredName (metadata VerificationMethod { … }), in attrs.type (the annotating form), in attrs.typeRef, or on a FeatureTyping child (metadata vm : VerificationCases::VerificationMethod { … }); the kind cell may be named or may redefine (attribute :>> kind); and the method may be declared once on a verification def and inherited by its usages. All of those are read, through the generalization chain, and so is a kind cell that names a VerificationMethodKind under a definition name this tool cannot resolve.

The facet is rolled up per REQUIREMENT. A case verdict is a summary over the set of requirements a case verifies; a verdict facet is a sentence about one of them. Each requirement's facet is computed from that requirement's own obligation rows, and a requirement this run produced no row for is written nothing at all and is named in the report's skipped list.

And the case verdict is not the file's verdict. A case's verdict is the library PassIf reading over the engine that was asked for; the facet that may be written into the file is pass only where every obligation was proved. So a green --engine literal run over a passing case writes inconclusive, and the report prints the difference on its own line.

8.2c Staleness is scoped to what a proof stood on, and the schema grew one optional property

validation/stale-evidence used to compare one number: a digest over the whole user model. Every edit anywhere moved it, so every record in the file went stale on every edit — including edits no proof in the file could read. An --engine smt record now carries a proofScope, and the checker compares that.

What is in it, and what each part catches. The footprint — the axiom rows the clause's read-closure reaches, each with its relation in normal form — by NAME and by DIGEST, so both an axiom that changed what it says and an axiom that newly entered the closure are visible. A digest over the whole axiom set, which is what the run's single consistency check stood on: proved means the negation is unsatisfiable under a satisfiable axiom set, and one added assert can void every proof in a file, including proofs whose footprint never touches it. A digest over the requirement's own premises, which is what the non-vacuity check stood on and what separates proved from vacuous. And a digest over the goal — the clause itself — because all three of the others are about a proof's CONTEXT and none of them is about what was to be shown; beside it the checker reads the clause's own obligationDigest, which every record has carried since the lane shipped. The scope also records the RESOLVED --free set every part was computed under: flags keeps the spellings a person typed, and a recomputation reading those would drop different rows and report an untouched file as stale.

Every row digest carries the SCALE, not only the relation. The digest a record is KEYED by (obligation.obligationDigest) canonicalises the expression tree and keeps the magnitude the file writes, with the declared unit nowhere in it — which is right for a key, because a record has to stay matchable to its clause across a relabel. It is wrong for a scope. Measured on examples/uav-isr.sysml, editing capacity : ISQ::EnergyValue = 640.0 [Wh] to 640.0 [J] leaves the node capacity == 640 byte-identical while the solver reads a quantity 3600 times smaller, and the endurance obligation goes from proved to refuted; the same holds for 18.5 [kg] → 18.5 [t] on the mass proof and for 35.0 [W] → 35.0 [kW] on examples/uav-power-budget.sysml. So each row in the scope is digested over its relation AND each variable's unit, affine SI map and declared sort, plus whether the unit gates granted the relation a scale at all. A scope built on the key digest alone said nothing about any of those three edits, which is the one thing §3.3b's MUST-NEVER list forbids: a scoped verdict reading current over a record whose obligation no longer holds.

Two of the four parts enrich the sentence and never change the verdict. The axiom-set digest is taken over EVERY axiom row's (name, normal form) pair, and the footprint is a subset of those same rows digested the same way — so a footprint member that changed what it says necessarily moves the axiom-set digest too, and a member can only enter or leave the read-closure if some axiom, premise or goal digest already moved. stale therefore reduces to axiom set, premises or goal moved. The footprint parts are what let a finding NAME the axiom a reader has to re-read, and they are in the census for the same reason; the narrowing this feature buys comes entirely from the edits that touch no axiom at all, which on examples/uav-isr.sysml is eight of nineteen.

Measured, on the two shipped examples. examples/uav-isr.sysml, 19 single edits against two proofs: eight move the whole-model digest and nothing either proof reads — a declaration with no value, a doc line, a state, an action, a part definition, a string facet, a renamed connection, a prose requirement — and the records stay put where the old comparison called all sixteen readings stale. The other eleven are reported, and the table in test/campaign/verification.test.ts states which parts each of them moved. On that model every one of the twelve axioms is a feature-value binding, so any numeric edit anywhere moves the axiom-set digest — that is the price of the third part, and it is visible in the table rather than hidden in a sentence. examples/uav-power-budget.sysml, nine edits against six proofs, is where the premise digest earns its place: raising one assume constraint { fc.supplyVoltage >= 20.0 [V] } to >= 200.0 [V] moves no axiom, no footprint member and no symbol, and takes the obligation from proved to vacuous. The first three digests all read unmoved; the premise digest is what stops the record reading current within this proof's scope over a proof the tool itself calls vacuous.

The unsat core is not what is recorded, and the substitution is the point. §3.3b of the implementation plan asked for a digest over the core. §8.3a's measurement below is why it is not: the core's membership moves with solver-context warmth, and a record is promised byte-identical across two runs over an unchanged file. The footprint is computed from the MODEL by the encoder's own relevance walk, is a pure function of it, and is what the core is a subset of. That the two walks agree is not assumed: footprintOf is asserted set-equal to the engine's own relevantAxioms over every model in the verification corpus and every shipped example — 58 models, 107 obligations compared and 11 whose goal the encoder refused, which never had a closure taken over them at all. The twin is a re-implementation, not a shared function: the rule that reads it is synchronous and reachable from the browser bundle, so it has to model the encoder's REFUSAL discipline as well as its symbol walk — a refused axiom is carried by the closure rather than pruned by it. The corpus therefore carries a model whose axiom the encoder refuses on a sort it cannot encode (footprint-non-proposition.sysml), so that half of the agreement is tested rather than taken on trust. The equality is held by that test; it is not a property of the code's shape.

The word current is never the scoped verdict. A scope that did not move reads current within this proof's scope, and the clause naming what that scope was is part of the sentence; bare current is said only of a record with NO scope, where it means what it has always meant — the record was taken over this model. The checker is silent where nothing in the scope moved; npm run check -- <file> --json publishes the reading per live record, inside the file's report object rather than beside it — {scoped, matched, wholeModelMoved, footprintContentMoved, footprintMembershipMoved, axiomSetMoved, premisesMoved, obligationMoved} and the sentence. matched is false where a record carries a scope this model states no obligation to recompute it against — the clause was deleted, or two anonymous clauses share one qualified name — and the comparison falls back to the whole model, saying so in its own sentence. That census is the instrument for a question no single run can answer: whether the extra digests earn their keep is a rate over edits, and one check sees one model version.

evidence-status is unchanged, and answers a different question. It reports whether a record was taken over THIS model — a fact about the file. The checker reports whether the edit could have reached the proof. Both are true at once, and a file where the first says stale and the second says nothing is a file where something moved and no proof in it could have read what moved.

One-directional forward incompatibility, stated as the measured fact it is. docs/schemas/evidence-record.schema.json gains proofScope as an optional property; a record carrying no per-instance facet keeps schema = "sysprose-evidence/1", so every record written before this build still validates and recordOfCarrier still reads every carrier in the wild. (A later change adds sysprose-evidence/2, which carries an optional per-instance facet and nothing else; both versions are read side by side, and the schema discriminates them. verify --record writes a requirement's clause read in a context or an instance as …/2, so a record file holding one is refused whole by a build before it.) The other direction does not hold: the schema is compiled with additionalProperties: false at every level in two places — the corpus test and loadRecords in scripts/sysprose.ts, which refuses the whole attach if any record fails — so a record written by this build is refused by evidence-attach on any build before it. A model file's pattern value can be edited back; a written record cannot be un-written on a build that will not read it. Records written by --engine literal carry no proofScope at all, and they are read under the whole-model comparison they were written under.

8.3 What the engines may and may not claim

--engine literal evaluates the model's own feature values through the same checkConstraints surface the app's Analyze button uses. Its claim word is holds-at-values and it can never reach proved. --engine auto resolves to the SMT engine or reports verification/tool-absent for every obligation, exit 2; it never falls back to a point evaluation, and --allow-inconclusive never lowers that row. The absence is exercised on every run of the L8 corpus and on every push in CI (.github/workflows/verify-examples.yml) with SYSPROSE_NO_Z3=1, because it is only reachable when something is missing and is therefore the single most likely path in this lane to rot into a silent green.

--engine smt ships and may say proved — and that word means exactly one thing. Per obligation O with premises P under axioms A, the engine runs check(A) once per run, then check(A ∧ P ∧ ¬O), check(A ∧ P) and check(¬O). proved requires: the negation UNSAT, the axiom set SATISFIABLE (an unsatisfiable one makes every negation unsat, so every obligation in such a run is verification/inconsistent-axioms with the core named — never a proof), the premises SATISFIABLE (otherwise verification/vacuous), and every feature released by --free confined on BOTH sides (otherwise verification/free-variable-unbounded, which is blocking and never a refutation). A goal that is unsat when negated with no context at all is still proved and is FLAGGED as a tautology, because x == x is not evidence about a design. Every sat witness is substituted back through the tool's own evaluator before it is printed, and with nothing freed it must also read as violated on the numeric surface; a witness that fails either gate is inconclusive: witness not confirmed, never a violation. A counterexample found under --free is design-admitted — exit 2, never exit 1 — because a = value is a binding the model states.

What the two engines agreeing does and does not establish. With --free none the SMT engine answers the question checkConstraints answers, and test/integration/verification.differential.test.ts asserts they agree on every encodable relation of both examples, all 82 campaign fixtures and the L8 corpus models: proved ⇔ satisfied, refuted ⇔ violated, and unknown ⇔ inconclusive: not evaluable. But that gate compares two consumers of one gatherer — a relation neither surface gathers is absent from both and the gate is green. So the relation census in the same file accounts for every constraint-bearing user element as encoded or refused-with-reason and asserts the counts equal the element census; a relation that leaves the pipeline without a word said about it fails there. Neither mechanism is a claim that the gatherer reads every construct the standard defines.

consistency answers a different question, and may say consistent only with the count of what it left out. verify asks whether each requirement holds of the design the file describes; consistency asks whether the requirements on a subject could be met by any design at all, and the two disagree by construction on a file whose values break a requirement. By default every feature carrying a literal value is RELEASED and only the structural axioms are asserted — assert constraint bodies, bind equalities, the defining equations of derived features — because a requirement set is inconsistent when nothing satisfies it, and answering that with the values that happen to be in the file is a question about one design point; --with-values re-pins them and asks the weaker question, and every verdict line names the mode. Each requirement is asserted as A ⇒ G, one implication per guarantee under that requirement's assumptions — the reading Requirements::RequirementCheck states and the one verify uses on the same file, named on every verdict line. Read as A ∧ G instead, two requirements guarded by mutually exclusive assume clauses (a mode- or phase-conditional pair) would be reported as contradictory, which they are not: no single design point is ever required to meet both. A set of implications is satisfiable by making every antecedent false, so each requirement that carries assumptions is also asked whether it can be ENGAGED at a point the whole set admits. A set that holds only because a requirement in it never applies is reported inconclusive under verification/vacuous — exit 2, forgiven by no flag — which is §2's rule that vacuity is inconclusive always, applied one level up; the witness is still published, because the set is satisfiable and only its meaning is in doubt. Mutually exclusive modes pass that check and two requirements under the same assumption with colliding guarantees do not, which is the discrimination the implication reading buys. An assume clause a gate refused stands the whole requirement down rather than being dropped from the antecedent, since G alone is the stronger claim and the model does not make it. On unsat the tool reports the conflicting subset z3's core produced, named by requirement and by the qualified name and element id of each relation, under verification/inconsistent-requirements — an error, exit 1, forgiven by nothing. That subset is called a conflicting subset: only --minimize, having run its deletion loop to completion, may call it minimal. On sat the design point is substituted back through the tool's own evaluator before it is printed. A relation a gate refused is listed and not asserted, which is sound in one direction only — an inconsistency found without it stands, a set called consistent without it may not — so the refused count is printed beside every verdict. A subject whose requirements state no relation this lane encodes is inconclusive, never consistent, and a run in which nothing at all was decided is exit 2 with --allow-inconclusive and without it. There is no point-evaluation counterpart for this question, so an absent backend decides nothing and exits 2.

What consistency is not. It decides the satisfiability of static contracts. Whether a reactive implementation can be built to meet a specification over time is a different question, is a declared non-goal of the verification plan (§6), and no surface of this tool claims it.

Evidence records bind a claim to a canonical model digest taken over qualified names, never element ids (ids are fresh UUIDs on every load), to the tool version, and to the flags that changed what was shown. They carry no timestamp, so they are byte-stable across runs. Their shape is schemas/evidence-record.schema.json, and every record the corpus produces is validated against it.

A record can now be written into the model, as a @SysproseVerification::Evidence { … } annotation on the requirement it is about — §7.27's annotating form over a metadata definition, which is the notation's own extension point and not invented syntax. Three properties of that write path are asserted rather than asserted about. The model digest excludes what a verification run itself wrote — the Evidence carrier, everything under it, and the verdict cell beside it — so a freshly attached record is current while an edit to any part of the author's own model — a literal, a status facet, a new part — still moves it. That exclusion is drawn by shape, not by provenance: every verdict cell on a requirement's facet carrier is out of the hash, including one a person typed on a requirement that never carried evidence, because nothing in the file marks which of the two wrote it. The consequence is stated rather than hidden — a hand-raised verdict is caught by verification/verdict-overstates-evidence, which compares the facet against the record's claim, and not by the digest. Every other facet a requirement carries — status, risk, owner, rationale — stays in the hash. The verdict facet is derived from the record's claim on every path, and is never copied from the verdict field a record states: a --engine literal record, whose claim is holds-at-values, writes inconclusive however its own JSON is spelled, and evidence-attach refuses a --from file whose stated verdict does not follow from its claim rather than half-trusting it. pass is written for proved alone. A requirement that states several obligations carries the worst of them, so one clause's pass can never overwrite another clause's fail and the verdict does not depend on the order the clauses were written in. And evidence accumulates: a second run appends, a fail is never overwritten by a pass, and every verdict a run moved is printed with both claims.

A verdict that outlived its model is a warning on the ordinary path. validation/stale-evidence fires from npm run check, not only from the verification lane, because the next person to open the file runs the checker. It names the requirement's slice — the declarations to re-read — and, for a record that carries no proof scope, states on every finding that a whole-model digest cannot say WHICH element moved. For a record that does carry one it names what moved (§8.2c) and is silent where nothing in the proof's scope did. Two further states are reported by name and never silently: a verdict facet with no record behind it (verification/claimed-without-evidence, info — a verdict reached by inspection is ordinary requirements management) and a verdict = "pass" over a claim that is not proved (verification/verdict-overstates-evidence, error).

Measured, and it is a negative result: what another tool makes of a Sysprose evidence record or verdict facet. The verdict facet is 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 ignore that line, and the one that was asked did. §6.1 records the probe: pushed to the public OMG pilot on 2026-09-09, the model came back with its 19 ids, 19 metaclasses, 14 names and 18 containment edges intact and every tool-local value dropped — both verdict cells and all 1466 characters of the record. Nothing was misread and no verdict was invented; the evidence's contents simply did not travel. (Whether the carrier ELEMENT survived is the one row that probe cannot take, and §6.1 says why.) Inside Sysprose the write path holds — the same fixture through the same client against our own server keeps all of it — so the boundary is the reader, not the writer. The digest also catches model edits, not a hand-edited record.

8.3a --why — an unsat core is a sufficient reason, and it is shown rather than recorded

verify … --engine smt --why names the members of the unsat core the solver returned for each proved row: the axioms, the goal, and the side conditions the encoding added, each with the kind it was asserted under. Three things about it belong here rather than in a release note.

It is not the set of assumptions the claim depends on, and the tool never says it is. A core is a sufficient reason, chosen by the solver. Measured on test/fixtures/verification/models/three-reasons.sysml, where mtow is bound at 18.5 kg and capped at 20 and at 22: the core for mtow <= 25.0 [kg] names mtowCapB — the weakest of the three sufficient facts — and does not name the model's own value at all, and swapping the two caps' declaration order does not move the pick. So an axiom listed may not have been needed and an axiom not listed may still carry the claim; that sentence prints beside every core the command names, and the words depends on appear on no --why line.

A side condition is kept, and it shares its name with an axiom. The encoding asserts a non-zero divisor where a relation divides by a variable, labelled with the qualified name of the row it guards. On examples/uav-isr.sysml the endurance proof's core carries both axiom:…AirVehicle::endurance and side:…AirVehicle::endurance, so a display filtered to axioms — or one deduplicating by qualified name — would drop a real dependency of that proof.

It is displayed and counted, never recorded. No evidence record carries a core and schemas/evidence-record.schema.json has no property one could be written into, because the membership of a core is the solver's choice and not a property of the model. (The schema has since grown one optional property, and it is the footprint — the model-level walk the core is a subset of. §8.2c says what that is and why the substitution was the honest one.) What was measured, stated as the observation it is: on examples/uav-isr.sysml, one file and one seed, the endurance proof's core is six labels in a fresh process, and five — the same four axioms and the goal, without the side condition — when the same obligation is judged inside a test worker running the whole verdict corpus of test/campaign/verification.test.ts. What differs between those two runs is not established: a probe that repeats the same call, and one that judges every model in that corpus first, both return the six in one process. The observation is what this section rests on; the mechanism behind it is not offered. Both cores are sufficient, neither is wrong, and a record quoting either would break the promise that two runs over an unchanged file write byte-identical evidence. That is also why this commit's three proved fixture goldens did not move, against its own plan entry, which asked for their detail to be re-recorded with the core in it: the plan's ordering decision is that a core is displayed and not recorded, and detail is copied verbatim into every evidence record, so writing one there would have recorded it through the back door and made the golden a golden over solver state. What --json does carry, per obligation, is the axiom census {modelAxioms, footprintAxioms, scriptAxioms, coreAxioms} — how far the answer narrowed, which is a question about a model and is worth asking of one before any feature is built on it. Measured today: no narrowing at all on examples/uav-isr.sysml (4 core axioms of a 4-axiom footprint), and 24 footprint axioms to 9 core axioms over the six obligations of examples/uav-power-budget.sysml. The census is four numbers rather than the three the plan named, because a published numerator with no denominator cannot be read, and because scriptAxioms and footprintAxioms do not bracket each other in either direction: a kept row that divides by a variable asserts twice, and a kept row the encoder refused asserts nothing. coreAxioms is read against footprintAxioms.

And the member list itself is in the --json payload on every run, with the flag and without it — the flag gates the text display, not the field. The sufficiency sentence is printed under every core on the text path; in the payload it exists only as the field's description in docs/schemas/verify-report.schema.json, so a consumer that renders these members carries that sentence itself.

The flag decides nothing. The claim word, the code and the exit status of a run are the same with it and without it — and a run that reached no proof says so in a sentence about proofs, because two other cores in this lane print on rows of their own: the one under verification/inconsistent-axioms is about the whole file's axiom set and the one under verification/vacuous is about one obligation's premises.

8.3b property-check — what the five gates establish, and what they do not

property-draft and property-check stand before the engines: they judge a clause an agent proposes, never the model, and neither of them writes anything. Both obey the reporting exit contract for that reason — a refused clause is an answer about a string the caller passed and exits 0, with the verdict in the report — because §2 reserves the judging contract's exit 1 for an obligation refuted at the model's own values and nothing else.

Gate 0 refuses a clause whose scope is not global, whose timing is not always, or that writes a condition at all: those three FRETish fields state something about time, and no in-process engine in phases 0–3 of this plan decides a temporal claim. It is a refusal, not an acceptance with a gap. Gates 1–3 are the tool's own gates — parseRelationBody, resolution in the subject's scope, then evaluateConstraintQuantityDetailed and readRelation — so a clause this command accepts is one the SMT encoder can read; a private re-implementation of any of them would let property-check accept what verify then refuses.

Gate 4 is SYNTACTIC non-triviality, and this is the limit. The clause and its negation are checked satisfiable under z3 with no axioms asserted at all, so a clause the model's own feature values already satisfy passes it: uav.mtow <= 25.0 [kg] is accepted over a model that pins mtow = 18.5 [kg]. What the gate refuses is a clause that is valid or unsatisfiable on its own (x <= x). verify's tautology check and the vacuity report are what decide the other question. The limit is printed on every report rather than left to be inferred, and it is one of the two limits in the §6 register that this command carries.

Nothing here reads prose, and no report ever says a clause is the formalisation a requirement asked for. Every report — text and JSON, accepted or refused — carries the same fixed line: "meaning is not checked; read the back-translation." The back-translation into structured English is the only defence the tool offers against a clause that parses and means the wrong thing, and reading it is the author's job. scripts/agent-repair-bench.ts --suite verification measures how much of the gate surface a model clears from the draft alone; it deliberately does not score meaning.

8.3c refine — whose obligations these are, and what γ is allowed to assert

refine --via composition decides Cimatti's Theorem 1, in normal form, over a decomposition the model states with satisfy. With nf(C) = ¬A ∨ G the two obligations are (3) ⋀ nf(C′) ∧ γ ⊨ nf(C) and (4), for each component U, A ∧ ⋀_{S′≠U} nf(C′) ∧ γ ⊨ A_U; both are preceded by a satisfiability precondition, step (0) check(A ∧ ⋀ nf(C′) ∧ γ).

Normal form is a soundness requirement, not a presentation choice. With bare guarantees the static check admits mutual support: A₁ = G₂ = p and A₂ = G₁ = p against a system contract ⟨true, p⟩ makes G₁ ∧ G₂ ⊨ G provable while an implementation with p false satisfies both component contracts and breaks the system guarantee. cofer-2012's soundness argument for the bare form rests on a temporal order a static check does not have; this tool does not borrow it, and the case is pinned as a known-answer model.

Step (0) is what stops a contradiction proving an architecture. Sub-contracts ⟨true, x > 10⟩ and ⟨true, x < 5⟩ over one bind class make the antecedent of (3) unsatisfiable, so (3) holds vacuously; the run reports verification/contract-set-vacuous, exit 2, and never refined. Vacuity is one claim word and one exit code across this whole lane (§2), and no flag lowers it.

γ is bind ∪ the item flows, and that is a deliberate reading with recorded counter-evidence. The connection assertion is built from the bind/BindingConnector equalities and from the directional item flows propagateValues already carries, encoded as target = source — the same edges checkConstraints, the app and every other report honour, so a proof here cannot rest on an equality the rest of the tool does not believe. A bare connection is refused: it is listed under notEncoded with the hint bind the attributes if they are one quantity, and the count travels with every verdict. --connections-as-equalities opts into the OCRA reading and prints the fact on every verdict line. cristoforetti-2026 §4.1 — the one published SysML v2 → OCRA path — translates connect and bind alike, and Cimatti's γ is by definition the connection-and-delegation assertion, so the default here is a stricter reading than the published path takes rather than a consensus. It is recorded as a choice, not as a fact about the standard.

What it never claims. Nothing about ordering or time: this is the propositional and numeric shape of contract refinement, not OCRA's temporal one, and every verdict line says so. No report says "the architecture satisfies its requirements"; none says refined while an obligation is undecided; none says refined when the antecedent of (3) or (4) is unsatisfiable.

A refused clause, and which half of the contract it came from. Any refused clause on a system contract stands its whole decomposition down as verification/refinement-undecided, because dropping a conjunct of nf(C) would weaken the goal being proved. On a component contract the two halves of nf(C′) = ¬A ∨ G move in opposite directions, and the tool treats them so: a refused require conjunct only weakens that component's normal form, which a proof survives, while a refused assume conjunct strengthens it — dropping a₂ turns ¬a₁ ∨ ¬a₂ ∨ G into ¬a₁ ∨ G, and with every assume refused the normal form collapses to a bare G, which is the axiom "this component promises its guarantee unconditionally" that the file never stated. So a component with a refused assume is kept out of the premise set — the only sound premise for a normal form with an unknown conjunct of A is ⊤ — and its own obligation (4) is verification/refinement-undecided, which stands the group down. Both facts are reported either way. test/fixtures/verification/models/refinement-refused-clause.sysml pins both directions.

What the delegation half costs, stated rather than hidden. A constraint body reaches a nested quantity through the type of each part, while a connector endpoint written as a.p resolves to a usage-scoped implicit copy that keeps connect a.p to b.p from collapsing into a self-edge. The two spellings denote different elements, so an equality over the second joins nothing the contracts talk about, and a decomposition wired that way reports its assumptions as undischarged rather than proving them. examples/uav-power-budget.sysml names the definitions' features in its bindings for exactly that reason, and says so in its own doc comment. Closing the gap would need a delegation term in γ that the plan does not specify; until it does, the failure direction is the conservative one.

8.3d fault-tree — what a cut set is a claim about, and the four it never makes

fault-tree injects contract failures into the decomposition §8.3c judges. A basic event is "sub-contract i not honoured", and a set F is a cut set exactly when obligation (3) — ⋀ nf(C′) ∧ γ ⊨ nf(C), the same obligation, the same normal form, the same γ — fails with the normal forms in F out of the premise set. That is stewart-2021's fault injection into an AGREE contract and bozzano-2014's basic event, and the enumeration goes through one seam into the refinement module rather than transcribing the normal form a second time: a fault tree over a second reading of nf(C) = ¬A ∨ G would enumerate cut sets of an architecture the other command never judged.

Cut sets are minimal, bounded and counted. Sets are enumerated by increasing order up to --max-order (default 2); every superset of a cut set is pruned rather than checked, because withdrawing more guarantees cannot restore an obligation that already failed; and the number of solver checks is printed. Pruning removes the supersets of sets shown to be cut sets, never those of a set the solver did not answer about — such a superset is still a cut set, but its minimality was never established, and the row says so rather than calling it minimal. A @SysproseVerification::FaultHypothesis { maxOrder = 2; } carrier pins the bound in the model — rauzy-2019's point that the safety model and the design model stay separate and are synchronised by something written down — and the flag overrides it, with the report naming which of the four the number came from. Both cell spellings are read, with and without the attribute keyword; a cell that cannot be read is reported as such rather than passed off as the default.

The four sentences it never writes. No cut set over a vacuous contract set: obligation (3) cannot fail from an unsatisfiable antecedent, so step (0) runs first and a contradiction is verification/contract-set-vacuous at exit 2 (§8.3c's rule, one lane along). No single point of failure when any order-1 check was undecided: the field is null rather than false there, and there is no --allow-inconclusive on this command to forgive one. Any undecided check spends the 2, including one that sits inside a tree whose enumeration also found cut sets — that tree is not an undecided tree, so the undecided checks are counted in their own figure and tested before the return 0. An absence without its bound: "no cut set up to order 2 — higher orders not explored" is the whole sentence, and §6's register lists it beside "no violation within k". And an empty cut-set list over a state machine: a state machine passed as --element is answered with a measurement rather than a tree — how many failure-mode flags and #exceptional states it carries, which is what a behavioural fault tree would inject and aim at — and exits 2 under the row that names a state machine whose failure modes this command found none of (or, over a machine carrying a flag this build does not inject, found and does not inject — the same row). Nothing is enumerated over it and no absence is claimed. And the route measures exactly the machines the census counts — the roots reach walks: a state inside a machine is refused with the machine named, and a state definition that owns no transition is refused as not one of this tool's machines, so one payload never carries a machine answer beside machines: 0 and a tagged hazard is never counted against itself as 0. The --json payload carries a file-wide census of the same two things (faultTree.behaviouralLane), which is the measurement a behavioural fault tree is held behind; it reads 0 on every shipped example and every verification fixture, and a census that finds nothing is the result rather than a failure.

What it is, said on every report. Contract-level fault-tree analysis over the refinement obligations — not a behavioural safety analysis, and nothing about ordering, time, rates or probabilities. The model states no failure rates and this tool derives none: a cut set here is a structural statement about which contract failures suffice, and an order-2 cut set is what redundancy looks like from the failure side rather than a finding against the design.

8.4 The SMT seam: the solver backend and the encoder the engine stands on

z3-solver ^5.2.0 is an optional dependency. src/semantics/smt/z3-bridge.ts loads it through a dynamic import behind a variable specifier and answers either a backend or { absent, reason } — it never throws because a package is missing, and SYSPROSE_NO_Z3=1 forces the absent path so that a machine which HAS z3 can still exercise it. Every check is bounded (5000 ms by default, no spelling for "unbounded"), the random_seed is fixed at 0, and z3's version is captured rather than assumed. A script z3 REFUSES — a malformed term, or a set-logic its assertions do not fit — is reported as error, never folded into the unknown that --allow-inconclusive may forgive.

src/semantics/smt/encode.ts turns a body the unit gates already passed into an SMT-LIB2 script. Four properties of that encoding belong in a conformance record because they decide what a later verdict means:

What ships over it. The SMT engine (src/semantics/engines/smt.ts) drives this seam as of commit 5 of the verification plan; §8.3 above states what it may and may not claim. The seam's own rules are unchanged by that, and they are what keep an engine defect from reading as a verdict.

Not in the browser, and the build enforces it. z3 WASM needs SharedArrayBuffer, i.e. COOP/COEP headers a static host cannot set, so the package is excluded from the bundle (optimizeDeps.exclude and rollupOptions.external in vite.config.ts) and nothing in src/ imports it statically. external alone would point the wrong way for an import — it leaves a bare z3-solver specifier in the emitted chunk, which builds green and breaks the published page at load time — so a refuse-bundled-z3 build plugin fails the build when any emitted chunk names the package in an import or a require. The app's affordance is the terminal command, not a smaller solver.

Measured on this machine, not remembered (Node 22, z3 5.1.0 via z3-solver 5.2.0): init() ~105 ms, three checks (unsat, negation-unsat, sat with a witness) ~137 ms — the plan carried one combined figure of 343 ms and could not say which half it was. The two SMT suites were run under vitest's default worker pool and under a single fork: 66 passed both ways, 5.4 s against 7.1 s wall clock, and they add ~5 s to npm test. z3 WASM is worker-safe here, so the suites are NOT pinned to one worker. The cost the plan asked to be known rather than assumed is contention, and it is visible: inside the FULL suite (137 files across the default worker pool) the same two figures measure 311 ms and 358 ms, with no change to any verdict. A related figure, measured because a later commit's call counts depend on it: one z3 context is reused across checks and only the solver is fresh, because a context per check leaks ~9 MB of WASM heap that nothing gives back — 400 checks cost 2 GB before the fix and ~140 MB after, and a suite case runs 200 checks against a stated bound. npm test itself is 296 s on this machine, past the plan's 241 s budget; the SMT suites are ~5 s of it, so that overrun is not theirs to fix.

Re-registered at commit 5, same command, same machine (§6 asks for the wall clock before and after, not for a promise). Measured with /usr/bin/time npx vitest run: 287 s over 137 files with the engine present and none of its suites written, and 351 s over 138 files with all of them — a +64 s delta, on a run that also went from 2 533 tests to 2 581. The engine's own cost is the differential gate and the relation census, which load 103 models and run BOTH engines over each (~18 s measured on their own), plus the sixteen SMT cases the L8 corpus gained and four single-field mutation cases. The last 18 s of the delta arrived with the adversarial review, which added four L8 cases on the gate-refused seam and widened the flag-scope sweep from the encodable rows to every censused one. The budget the plan set was 241 s and this build does not meet it: the overrun predates the engine — 296 s was already registered at commit 4 — and it is recorded rather than rounded away.

Re-registered again at commit 6, same command, same machine: 374 s over the same 138 files, a +23 s delta on a run that went from 2 581 tests to 2 595. Almost all of it is the process boundary rather than the solver: the four new L7 cases each spawn tsx and bind the standard library (~6 s apiece), while the eight new L8 consistency cases run in process and cost ~2.4 s between them. The budget is still 241 s and this build still does not meet it, for the same reason and by the same accounting.

Where the budget actually went, and the one file that was spending it. By the end of the lane the gate's wall clock was not the solver and not the engine: it was test/campaign/cli.sysprose.test.ts, which spawned npx tsx scripts/sysprose.ts 240 times — a node, a tsx transform of the whole import graph and a bind of the 38 761-element library apiece — and ran 787 s of a 790 s run. Every other file in the suite finished in parallel underneath it, so the gate cost what that one file cost, and every commit after it paid the bill again. The cases now ask what they are asserting: the ones about the PROGRAM (exit status, - on stdin, a payload past the pipe buffer, an unknown flag or subcommand, an unreadable or unwritable file, every --help, an invocation through a symlinked path, the one nonlinear optimisation whose memory is unbounded, and one end-to-end run per exit contract) still spawn — 82 spawns, down from 240 — and the ones about the TEXT call the same main in this process, which scripts/sysprose.ts now exports and runs only when it was run as a script. A bridge case spanning all 22 subcommands runs the same argv both ways and requires the same bytes and the same code, so the equality the split rests on is checked rather than assumed.

Both spawn figures are counts of processes actually started, not of the places in the source that say to start one: spawnSync was wrapped in that file and the calls logged, once over the file as it stood at c929278 and once over the file as it stands now. The distinction is not pedantry — several call sites sit inside loops. The figure this section published before, 223, was a count of run([ lines in the source, and the run it described started 240 processes.

The wall clock was taken the same way at both ends, one file at a time (npx vitest run test/campaign/cli.sysprose.test.ts), each started with ps -eo pid,args | grep "[v]itest" showing nothing on the machine but the run about to begin: 772.77 s over 96 cases before, 268.50 s over 99 cases after — the same assertions over the same models, at a little over a third of the wall clock. Neither figure is delicate. The before run had another worktree's suite join it partway through, and the same file measured 776.44 s on a machine that was running four of them for its whole length: half a percent apart, because what this file spends is serial process startup rather than CPU, and startup does not contend.

A first cut of this split was faster and unsound, and the number it produced is recorded here so nobody chases it again. Moving EVERY case in-process reached 322.96 s at the gate — and produced five Aborted(Runtime error: The application has corrupted its heap memory area (address zero)!) unhandled errors from z3-solver's WASM module over 70 in-process solver calls. z3 carries process-global state and does not survive being driven many times inside one worker; the subprocess boundary had been supplying that isolation for free, and converting the calls removed it silently. vitest's own warning for that condition is the point — an unhandled error of this kind "might cause false positive tests", so the failure mode is a GREEN run, not a red one. A solver-bearing subcommand therefore spawns, for the same reason - does: not because the assertion is about the process, but because the invocation needs one. Under SYSPROSE_NO_Z3 no solver loads, so those cases stay in-process.

At the gate the change reads as 760.83 s → 548.74 s for npx vitest run (145 files, 3 000 tests, 0 failed, 0 solver aborts), both measured on an idle machine with ps showing no other vitest process. This one file is still the longest pole. Measured on the tree that ships this: 48 call sites spawn because what they assert is the process contract, 70 more are routed to a spawn at invocation because their subcommand can load the solver, and 113 run in-process. Neither spawning set is available to trade — one is the contract, the other is the isolation.

8.5 check-behaviour — what a safety verdict is a verdict about

Nothing here is a claim about the specification's execution semantics. The engine is a walk of the configuration graph the interpreter in this repository defines, and every verdict it prints carries the six-field semantic profile that says what that interpreter does — run-to-completion bounded at 64 chase steps, innermost-substate priority, shallow history by parent map, regions concatenated rather than interleaved, no event pool at all, and a discrete after(n) clock the walk over-approximates by offering each label as an event. andre-2023 §2.6's point is that every published formalisation of state-machine semantics differs on exactly those six, so a verdict that did not name its reading would be one nobody could reproduce or contest. PSSM is not implemented and no conformance with it is claimed.

Which properties it decides, and which it refuses. Four patterns — absence, universality, bounded-existence, precedence — are safety properties, and a bad-prefix search over a finite graph decides them. One — cover — is a guarantee in Manna–Pnueli's sense (◇β): not finitely refutable, which is why the engine cannot decide existence, but finitely witnessable, which is why the same search that refutes absence of P confirms cover P — the bad prefix of the one is the witness of the other, and the monitor is shared byte for byte. One — recovery — is branching-time (AG EF p: from every reachable configuration, some continuation reaches p), which no bad-prefix search decides in either direction; it never reaches the search and is answered by reverse reachability over the walk's retained relation, as recoverable or as not recoverable naming the configurations that cannot, and ONLY over a walk whose relation is the machine's own (walkIsExact, register row A7) — both directions behind one gate, because a guard the walk could not decide removes an edge the model states and would otherwise manufacture the refutation at exit 1 — with recoverable withheld besides wherever the interpreter's chase budget stops a run of a trigger-less machine somewhere that does not hold p; it reads state and node atoms only, through the same selection absence reads them with, and refuses the other three kinds rather than earning a refutation from an empty target set. Two — existence, response — are liveness, and a bad-prefix search finds no bad prefix for either on any graph; both report inconclusive: liveness not checked in-process until a lasso search lands and a fairness assumption is named. A pass is emitted only when the walk saw the graph whole: the four conditions §3.8 states, computed from exploreMachine's walk, and the fifth this tool added afterwards — every guard the walk consulted decided something. A bound hit, a parallel or history machine, a guard the walk could not evaluate, an unreadable property, an atom that names nothing, a witness the interpreter does not take (verification/witness-not-replayed) or a recovery withheld because the chase budget stops a run somewhere that does not hold p is inconclusive ⇒ exit 2. A fail does not need exhaustion, and the asymmetry is deliberate: a bound can hide a violation and can never invent one.

cover has two words of its own, and neither is one of the four above. A witness is covered: it stands on a partial walk exactly as a fail does, because a bound can hide a run and can never invent one, and it exits 0. No witness over a graph seen whole is not covered: a decided absence, published under the same five conditions a pass is, and a missing behaviour rather than a violated requirement — so it carries verification/not-covered as an info line and exits 2, and spends the 1 only under --cover-required, which adds verification/cover-required as an error beside the info line and changes no claim word. covered ⇒ pass would file a witness under a word that means on every reachable configuration; not covered ⇒ inconclusive would file a decided answer under the word reserved for undecided; not covered ⇒ fail would print verification/refuted about a design that violates nothing — the exact defect the pattern exists to fix. Two disclosures ride on the witness. A run that consumed a trigger carries the environment sentence, which names the triggers that run consumed: the walk offers every trigger the machine names wherever it can decide that the interpreter takes its next event — where no completion transition is due, or where the chase budget is spent with one still due — so a witness that consumes abort is a claim about that environment and not about one that withholds abort — a function of the triggers since commit 24 of the model-checking plan, never a constant with an example trigger inside it. A run that crossed an after(n) dwell, or a transition whose guard the walk read against a store nothing valued, keeps the claim and re-words the warrant — a run this WALK admits, naming the step and the mechanism — because the walk advances no clock and the interpreter may never take that trace; the bare a run this semantics admits is never printed over it. The condition is register row W1 in src/semantics/mc/publishable.ts: relationIsTheMachines, or the per-step alternative over the transitions the trace actually used, and no member of the bound family. One semantic decision, recorded rather than implied: under before and between, absence establishes a breach only when the segment closes, so a cover witness under those scopes extends to the closing R — a between whose segment never closes is vacuous, exactly as for absence. Where any guard on the machine could not be evaluated, a cover is inconclusive under verification/guard-undetermined — the register's row A5 reads the same five conditions a pass does, and that includes every guard decided — the census counts the exposure as a fraction (coverUnreached and coverUnreachedBehindUndefinedGuard, on --json: the unreached states, and how many of them sit behind an undecided guard alone), and --cover-required prints on every such row that it was not applied, quoting that fraction, rather than spending the 1 on an unbound model parameter.

A refutation says whether it is one run or every run, and the word is gated. Every fail a bad-prefix search produces carries an every run? line — modality on --json — with one of three values. potential claims that some maximal run of the MACHINE avoids the violation, and names it: a cycle that never enters the violating configuration, or a configuration of the retained relation with no way out — on a machine that names no trigger, only one a run reaches inside the chase budget without the violation, and otherwise the configuration where the budget stops such a run; it is register row W3, a maximality witness, and it stands only where walkIsExact holds — on FlightModes it names the cycle manual → autonomous → manual, which is the simulator's own tie-break read the other way. guaranteed claims that every maximal run of the machine reaches the violation; it is register row A8, an absence claim (no avoiding run), and it reads the same gate. not decided is the word for everything else, with its reason: a walk not seen whole, a stateful monitor or a step atom (the product does not collapse onto the configuration graph), an expression atom (the store is not retained), a named trigger, an after(n) dwell, a guard the walk consulted and could not decide, or the interpreter's 64-step chase budget — a walk that follows it through a stopped chase, or, on a machine that names no trigger, a guaranteed that a run the budget stops before the violation would contradict — on the latch machine the naive answer is guaranteed, about a design that sits in nominal forever when nobody sends unlatch, and the line says not decided instead. None of the three moves a count, a code or the exit code: the row is a fail with a witness before the line and after it. What none of them claims: nothing about the interpreter (simulate takes the first declared branch and may never produce the run potential names — the simulator sentence prints beside it wherever the machine has a choice point), nothing about an environment, and nothing about time.

Those five conditions have exactly one definition, and the claims this lane makes are a list a test can walk. publishabilityOf in src/semantics/mc/publishable.ts is the conjunction both reach and check-behaviour read — the same four conjuncts off the same walk, plus the product-search conjunct only the second of them has, which is a field a walk-only claim does not carry rather than a false it would print "bound exhausted" from. Beside it sits walkIsExact, a second and stricter predicate for a different kind of claim, and the published answers that read it are the trap list (register row A6), the modality on a refutation (A8 and W3), the wording of a covered warrant (W1) and both directions of recovery (A7): an absence list gets smaller as edges are added, so a walk that offers more edges than the machine grants cannot invent one, while "nothing here is inescapable" gets easier to state as edges are added and the same over-approximation falsifies it. Two registers, ABSENCE_CLAIMS and WITNESS_CLAIMS, record which of the two each claim reads, which way it moves as edges are added, and what is published instead when its condition fails; test/unit/semantics.mc.publishable.test.ts asserts the wiring by reflection, so a claim added without a condition is a failing test rather than a review comment. Nothing about the standard is claimed by any of this: it is a record of what THIS tool's walk may and may not say.

The walk retains the successor relation it computes, and the relation is the one reachability was computed from. exploreMachine produced an edge for every step it took and discarded it; it now keeps it, as integer node numbers in breadth-first discovery order, together with the active state stack and the active leaf of each configuration. Four things about that record are worth stating, because each of them is a way the same field could have been dishonest. It is over innermost-level steps only — the profile's priority rule says an inner enabled transition beats an outer one, so a configuration reached by firing a beaten transition is one no run of this reading enters, and it is not a node. It holds no edge into a configuration a bound refused: such a configuration is never numbered, and openFrontier — the negation of exhaustive, never a test on which bound was hit — is how a reader learns one existed. An edge into a configuration the walk has already seen is recorded at the revisit prune, beside the edge into a newly admitted one, so the relation is the union of the two sites; recording only at the admission point would retain the breadth-first spanning tree, which has one edge fewer than it has nodes and no cycle at all, and the two edges the prune contributes on examples/uav-isr.sysml are exactly the ones that close that machine's cycles. And it is interned to integers: a configuration hash is built from element ids, which are fresh on every load, so no hash string reaches a report, a digest or a JSON payload. The gate for the commit that added it was that every row reach publishes on the shipped examples is unchanged; the relation is now read by the component census and by the trap list below.

The components of that relation are computed, and what they are allowed to say about the MACHINE is a separate question that is asked first. reach --json now carries an exactness census beside its edge census: how many edges the walk retained, how many of its transitions this engine reads as a dwell, how many events the machine names, how many guards were consulted and decided nothing, whether the walk saw the graph whole — and whether the retained relation has a cycle. That last field is three-valued. It answers true or false only where the relation the walk retained is the relation the model states, and null everywhere else, because the question is about the machine while the graph is the walk's: an edge behind a guard nothing valued is a cycle-closing edge the walk never had, and a walk that refused a construct outright has an empty relation that trivially has no cycle. A boolean there would state a property of a graph nobody built. The census itself is not a finding and is not printed: it is a --json payload field, and every claim the command published before it still reads the same conjunction it read before — a state nobody enters and a transition nobody fires are claims that can only shrink as edges are added, and pointing them at a gate built for the claims that GROW would empty a sound finding out of a shipped command.

One claim now reads the stricter gate, and it is the first of the kind that grows. reach reports each set of reachable configurations no run leaves — a bottom strongly-connected component of the retained relation — as verification/unrecoverable-mode, a warning at exit 0, naming the states of the set (the union of the active stacks, never the leaf alone) and the shortest way in. Three kinds of bottom component are exempted and never reported: an ending (final states and done nodes), a single configuration with no successor (which is already verification/deadlock, so one fact gets one row), and the component holding the opening configuration, which is the machine's own reachable core. That third exemption is what keeps all three shipped examples silent — each is one component holding its opening — and the campaign's exact diagnostics array over examples/uav-isr.sysml is unmoved. The list is gated on walkIsExact and on nothing looser: the "no trap" its emptiness asserts gets easier to state as edges are added, and each row's "nothing leaves this set" is falsified by a MISSING edge, so a bound, an unsupported construct, a dwell transition, a named trigger and an undecided guard each EMPTY the field rather than shorten it, and the three of those that refuse a walk that finished print an inconclusive: line naming the clause. Four fixtures pin the four mechanisms by name: a factory-built preempted dwell (time), the latch's unlatch (environment), the trapguard trio (store — the base file refuses, = false publishes the trap because the guard is DECIDED and the relation is the machine's, = true is one whole-graph component and is exempted as the core), and --max-configs on the trap probe. The --json row carries a trap census — components, bottom components, and how many were exempted as endings, deadlocks or the core — three-valued like the acyclicity field, so a bounded walk never publishes "3 exempted as deadlock" about frontier nodes that only look like sinks; where the gate held and no trap was found it carries a sentence naming what was exempted, byte-identical on a DAG into done and on a two-state sink beside that sink's deadlock row, and that sentence is never a text row. What the row never says: that the machine can recover, that it livelocks, or anything about the system the machine models.

A cycle the interpreter's chase goes round is a finding of its own (U1, 2026-10-14). reach reports a reachable set of configurations where a trigger-less transition is due at every one and the transition the interpreter fires at each — the first enabled at the innermost level, by declaration order — leads to the next, round and back, as verification/completion-livelock: a warning at exit 0, once per cycle of states, naming the states in the order the chase goes round them and the shortest way in — a run the simulator makes wherever the walk holds one, and said to be the walk's own, with the state where it parts from the simulator, where it does not. Such a run spends its 64-step chase budget there and moves on only on an event (on a machine that names no trigger, it ends there). It is decided over configurations and over the interpreter's own chase, so a loop whose guard or store takes the chase out on its own is not reported, and a cycle only another branch of a choice could leave is — with the state where declaration order keeps the chase on it named in the row. It stands on steps the walk took, so a bound does not withhold it; a guard the walk could not evaluate on a trigger-less way out of the cycle, or a dwell as the chase's step, does, and a withheld line says so in its place. check-behaviour files the same published rows beside its verdicts and moves none of them. On v9 it is ten rows, one on each of the ten machines whose interpreter run spends the budget. On the shipped examples it is three rows, one on each machine whose trigger-less transitions cycle: FlightModes' chase goes round manual ⇄ autonomous in examples/uav-isr.sysml, which moved the campaign's exact diagnostics array over that file by one row, VehicleStates' round idling ⇄ moving in examples/vehicle.sysml, and views-tour.sysml's FlightModes round standby ⇄ flying. The trap row still never says the word (docs/06 §8.8).

One row did move, and it moved towards saying more rather than less. A verification/deadlock row — this configuration has no enabled way out — used to be withheld across a whole machine whenever any guard anywhere in it was left undecided. That is one question asked in place of another: what can make such a row wrong is an undecided edge out of the configuration the row is about, over its own active stack, and an undecided guard in another region of the same machine cannot. The question is now asked of the configuration. Where every guard decided, the two readings are the same expression and every row is unchanged; where one did not, a genuine sink whose own way out nobody was ever consulted about is reported instead of being lost with the row that really is undecided.

The declared deviation of §8.1 extends to this command, in the same words. A property whose antecedent never holds is vacuous ⇒ inconclusive ⇒ exit 2, not true — the two antecedents this engine detects are a scope no explored run opens and a precedence whose P never occurs. Sub-formula-replacement vacuity is not done. --strict-vacuity raises the row to verification/vacuous-property, an error, and changes no exit code. The verdict vocabulary is six words — pass, fail, vacuous, inconclusive, covered, not covered — the last two cover's alone, and closed after them; this command never says proved, never says verified and never says deadlock-free.

The property carrier is Sysprose's, not the specification's. @SysproseVerification::PropertyPattern { attribute pattern = …; } is §7.27 annotating metadata over a metadata def this tool ships as text, exactly as the evidence carrier is (§7). A conforming external reader may ignore it entirely, and nothing is claimed about what another tool makes of it. And the value pattern = "cover" is a forward-compatibility commitment of the same kind as an added evidence-record field (§8.2c): it is persisted in a user's file, and a build before it reads the carrier through the same generic cell reader and then refuses the value as verification/malformed-property — inconclusive, exit 2 — on a model that is green on this build. One-directional, in the same direction as every other carrier commitment here, and priced in this paragraph rather than left unsaid; the alternative, a --pattern-only feature with no carrier value, was rejected because PropertyPattern exists so a property travels with the file. The value pattern = "recovery" is the same commitment, made the same way: a file carrying it is refused by any build before the pattern landed as verification/malformed-property — inconclusive, exit 2 — on a model this build decides; recorded here in the commit that added it.

8.6 The vocabulary this lane reads, and the vocabulary it writes

Scattered across §7 and §8 this is already true; gathered in one place it is checkable. The rule the two tables encode: the lane reads the notation's own constructs and writes almost nothing back, and the little it writes is one standard annotation plus tags that are visibly this tool's.

Read — the specification's own constructs, taken at their own meaning.

Construct What the lane does with it
RequirementDefinition / RequirementUsage, and their subject, assume, require, objective clauses The contract: assume is the premise, require the promise, subject who both are about. Nothing is inferred that the clauses do not say.
objective on a CaseDefinition/UseCaseDefinition/VerificationCaseDefinition and their usages A contract on a behaviour, with the subject defaulted to Case::result per the shipped Systems Library/Cases.sysml and bound to the case subject per VerificationCases.sysml
Satisfy, Derive, Refine, Verify Who claims to discharge what, and in which direction — Derive is read source = original, target = derived
ConstraintUsage bodies, feature values, ISQ typing and unit literals The relations that are encoded, scaled to coherent SI; a construct outside the encodable fragment is verification/unsupported-construct, named (§8.3)
VerificationCases::VerificationMethod and VerificationMethodKind The gate of §8.2b: a case without analyze in its list is not judged at all
VerificationCases::VerdictKind literals Mirrored as strings in the values the verdict facet may take. It is not a VerdictKind reference and does not pretend to be (§8.2).
Any #keyword over a metadata def, ours or a third party's Inventoried with what it resolves to, and never acted on by accident (§7)
@SysproseVerification::FaultHypothesis { maxOrder = N; } Read, never authored — a tag of this tool's own that a reviewer writes, carrying an ASSUMPTION and never a result: how many independent contract failures are credible at once. The bound it states overrides the built-in one, and a carrier this tool cannot read is reported as provenance rather than passed off as a default (§8.3d)

Written — one standard annotation, and three tags that are this tool's.

Written Whose vocabulary Where it is justified
@VerificationCases::VerificationMethod { attribute kind = analyze; } on a case that stated no method The specification's, and the only standard element this lane writes §8.2b
metadata RequirementMetadata { attribute verdict = "…"; } Tool-local. RequirementMetadata has 0 occurrences in Part 1; the identifier resolves to nothing, and the value is an unbound quoted string §8.2
@SysproseVerification::Evidence { … } Tool-local, §7.27 annotating metadata over a metadata def this tool ships as text §8.3, and the interop measurement in §6.1
@SysproseVerification::PropertyPattern { … }, metadata def <exceptional> ExceptionalOutcome Tool-local, the same mechanism, and named as an extension everywhere they appear §7, §8.5

What a carrier BODY may say, and the one spelling it may not. A vocabulary is a metadata def and the cells its annotation body carries, and the second half is as hard to withdraw as the first, so the shapes are recorded here and pinned in test/unit/semantics.keywords.test.ts rather than left to be discovered by whoever writes the next carrier. A set is one cell holding a ;-delimited list, and the delimiter with the spacing around it comes back from a save byte-identical. Both spellings of a cell are read: the ordinary §7.27 annotation body { maxOrder = 2; }, which the parser stores as a keyword-less ReferenceUsage, and { attribute maxOrder = 2; }. A carrier this tool sees and cannot read is reported as provenance — the run says a carrier is present and was not read — instead of being attributed to a default, because the bound is the same number either way and the sentence about where it came from is not. The spelling that is not available is the repeated same-named cell: validation/duplicate-name files an error on each sibling, so a file spelled that way cannot appear in any model that passes npm run check — and a command handed one prints the errors above its report and exits non-zero, reporting on what parsed rather than reading the repeated cells as a set.

Everything else the lane produces — verdict lines, SMT-LIB, Othello, SMV, Lean skeletons, evidence JSON — leaves the model alone and lands in the terminal or in a file. No command in this lane edits a requirement's text, a constraint or a value.

8.7 connectivity --signature — what the census measures, and the two conditions it does not transpose

It measures structure, and it calls it structure. --signature adds a census to connectivity: how many parts declare a directed port, own an internal part and wire the two together, how many connectors join two ports of the same part, how many directed features port defs hold, how many parts own a behaviour, how many item flows and binding classes the user wrote, how many of the "ports" in the inventory are constraint parameters, how many ports are inout, and how far the connector graph reaches. Every one of those is a fact about what the model declares. A connect is not a guarantee that anything is transported, and no field here is named for a dependency or derived from one; the text path prints "structural only — a connect is not a guarantee that anything is transported" on every verdict the mode reaches, findings or not. The flag reaches no verdict and spends no exit code: connectivity reports.

Consistency conditions 1 and 2 are not evaluated, and 3 and 4 are not transposed. The consistency conditions this census measures for read a dependency relation inside a part — "this in port may be used within it to obtain that out port". There is no intra-part dependency relation in these models to derive a template from, so conditions 1 and 2 are not evaluated, and conditions 3 and 4 are not transposed at all: both presuppose a procedure activation — an entry at which an output is undefined and an order over which it becomes defined — and a part is a continuously existing structure with no entry. Measured on the shipped corpus rather than assumed: across all six examples, connectors joining two ports of one part read 0, directed features held by a port def read 0, and parts owning a behaviour read 0 of 14 on examples/uav-isr.sysml. Exactly one part in the whole tree declares a boundary port, owns internal parts and wires the two together — Vehicle on examples/vehicle.sysml — and it is degenerate: one in port, two internal parts, and no out port at all, so there is no in→out template to read off it. Drone on examples/views-tour.sysml declares a boundary port over an internal part too and counts 0, because its port is wired to the ground station and never to the part behind it: a boundary that reaches nothing inside offers the same empty template as no internal structure at all. Silence here would read as coverage, which is why the limit is recorded rather than left out.

The two granularities are this tool's reading, and are kept apart. unconnectedPorts answers per DECLARATION — a port declared on a part def used three times is one entry, and it leaves the list as soon as any one usage is wired — while unconnectedPortUsages answers per port OCCURRENCE, which is the granularity a dangling end actually has. Neither is the specification's: the notation defines a port, not a report, and the split is Sysprose's answer to the fact that collapsing the two hid real dangling ends. They are never mixed in one sentence, and unreconciledPorts is the report's own standing check that the two readings agree about the same port rather than two lists left for a reader to diff. The census inherits both readings unchanged and adds a third figure of the same kind — the connector metaclasses the inventory's own walk does not enumerate (BindingConnector and ItemFlow), published as a row rather than left to be found by diffing two source files.

The chain is read per occurrence, and is withheld where it cannot be. The longest directed chain --signature prints names a part occurrence and the port on it at each end (… :: fuelOut), because its graph has one node per port occurrence and not one per declared port. Keyed on declarations, two usages of one part def collapse onto one node, and the walk then publishes chains that compose two wires meeting only on paper and cycles a two-part model does not have. Where even the occurrence reading cannot separate two ends — which is exactly what ConnectivityReport.sharedOccurrences counts — the cycle answer and the chain are both withheld rather than guessed. And the chain never composes through a part: an in and an out occurrence of one part are two nodes with no edge between them, because the relation that would join them is the intra-part dependency this census reports the absence of.

Mapping to OMG conformance statements — and the honest gaps

OMG conformance area Addressed by Honest gap
Textual notation parsing Langium grammar; 100 % corpus parse; full textual round-trip stability Parse + full round-trip are closed; the residual is deep formal-semantics corners, not grammar coverage.
Model interchange element-graph api-json validates against the OMG JSON Schema; XMI library ingest (38.8k elements); self round-trip over HTTP via PilotApiClient No XMI export; interchange identity is the element-set multiset, not byte-for-byte; no live OMG pilot-server round-trip exercised offline (see §6).
API PSM (REST + Query) 10 live endpoints validated against OpenAPI 3.1; versioning/Query engine; concurrent-writer commit serialization (test/server/concurrency*); interop client round-trips over HTTP (§6) OpenAPI surface is representative (25 paths), not every endpoint/param.
Annotation vocabulary (§7.27 keywords) Prefix keywords are read, resolved against the MetadataDefinitions in scope and preserved verbatim through a save (src/semantics/keywords.ts); Sysprose's own #exceptional ships as text a user pastes, over the mechanism §7.27.1/§7.27.4 defines The vocabulary is Sysprose's, not the specification's, and the tool says so on every line that prints one. A third-party spelling is read only through a declared alias table, contributes to no worklist unless obligations --from-keywords asks it to, and is never reported as standard; hasKeyword — what a later engine asks — answers only from real resolution, so an alias hit is never mistaken for the shipped keyword. #observable is designed and deliberately unshipped.
OSLC PSM OSLC Core catalog/provider/query + Turtle/RDF-XML/JSON-LD + oslc:ResourceShape full-shape resources (test/server/oslc-shapes) A representative subset of the OSLC SysML PSM (no delegated dialogs).
Requirements — contracts and obligations contracts / obligations read RequirementDefinition / RequirementUsage clause roles and case objectives into an assumption/guarantee inventory and a proof worklist (src/semantics/contracts.ts, src/semantics/obligations.ts) These commands report structure only. They evaluate nothing and decide nothing: no solver stands behind them, and neither prints a word about whether a requirement holds. A clause an element INHERITS is disclosed and never filed. On a row whose element also wrote a clause of its own, the inherited one is listed marked (inherited), under a count that says how many of the clauses shown the element itself wrote and which element wrote each of the others; on a row whose element wrote none — requirement massOk : MassLimit;, the ordinary way to apply a requirement — the row names the definition the clauses are filed on instead, exactly as it always did. Either way it enters no worklist, moves no obligation digest and reaches no evidence key: the clause is filed once, on the element whose body holds it, so a requirement USAGE is still not read through its definition's clauses (the definition carries its own contract, and the usage's row names it rather than being counted as bodiless). The app shows less than the terminal here, on purpose and said plainly: the Contracts view (src/ui/panels/ContractsTable.tsx) shows an inherited clause as a count and the element it came from (ContractRow.inheritedClauses, inheritedFrom), while contracts lists the clause's body marked (inherited); the view's assumption and guarantee cells hold the declared clauses only, and nothing in the app files, counts or verifies an inherited clause any differently from the terminal. Only a clause some contract in the same run FILES is disclosed — a general type the run left out, a #prose statement or a clause written outside a case's objective, is disclosed nowhere. The variables and fragment a row carries are its declared clauses' and are labelled declared wherever an inherited clause is shown beside them; an attribute declared in a port def is one element however many ports reach it, so the variables a clause reads are reported per PATH and their in/out direction is taken from the port the path names; discharged and stale are declared in the status vocabulary and never produced, because both are read back from an evidence record that does not ship yet.
Requirements — verdicts (verify) verifyModel judges each obligation with a named engine — a point evaluation (src/semantics/engines/literal.ts) or negation-UNSAT in z3 (src/semantics/engines/smt.ts) — and writes an evidence record bound to a canonical model digest (src/api/verification.ts, src/api/evidence.ts); §8 above states the exit contract, the deviation and the two unbound slots One declared deviation (a requirement with a false assumption is vacuous, not true — §8.1) and one slot deliberately unbound (VerificationCase::verdict — §8.2). proved is reachable only under --engine smt, only as UNSAT-of-negation over a satisfiable axiom set with satisfiable premises and a two-sided domain, and only for the quantifier-free arithmetic fragment the unit gates pass — anything else is inconclusive with a code, and a missing solver is exit 2 rather than a fallback. The two engines are held to one answer by a differential gate over the whole fixture corpus, and every constraint-bearing element is accounted for by a relation census; neither says the gatherer reads every construct the standard defines. What an external tool makes of a record or a verdict facet is untested.
Safety — cut sets from contract-failure injection (fault-tree) Minimal cut sets over the refinement obligations of §8.3c, enumerated by increasing order with supersets pruned and the check count reported (src/semantics/fault-tree.ts); §8.3d above states what a cut set claims and the four sentences the command never writes Contract-level FTA, never a behavioural safety analysis, and every report says so. No failure rates, no probabilities and no importance measures: the model states none and none is derived. Every absence carries the order it was checked to; a vacuous contract set is reported as vacuous and never as "no cut set"; an undecided order-1 check forbids the no-single-point claim; a state machine is answered with a count of its failure-mode flags and #exceptional states — exit 2, nothing enumerated — rather than with an empty list. The order bound is an assumption about how many failures are credible at once, carried in a Sysprose metadata definition, and what an external reader makes of that carrier is untested.
Behaviour — bounded safety verdicts (reach, check-behaviour) An explicit walk of a state machine's configuration graph, exploring every enabled transition where the simulator takes the first (src/semantics/mc/), with safety patterns decided by bad-prefix search over it, the cover guarantee witnessed by the same search, and the recovery branching-time pattern decided by reverse reachability over the retained relation where the walk is exact; §8.5 above states the profile, the split and the exit contract This is a reading of THIS tool's interpreter, not of the specification's execution semantics, and every verdict prints the six-field profile it holds under. PSSM is not implemented and no conformance with it is claimed. Liveness is not decided in-process; a parallel or history machine is refused rather than walked; a bound hit empties the unreachable and dead lists and can never produce a pass — it does NOT empty the deadlock rows, which are about a configuration the walk already dequeued and offered every input at, and which a bound cannot make wrong; and a guard the walk consulted and could not evaluate withholds all three of reach's absence claims outright (verification/guard-undetermined) rather than reading “did not evaluate” as “is false”, and makes check-behaviour report inconclusive rather than pass or vacuous. Every edge-bearing element under a machine is accounted for by a census as walked, read by the opening, refused, with neither end a node the walk can stand on, or as no step at all (a typing, a subsetting, a connect — facts about the states rather than steps between them) — and an edge that sequences behaviour and that the relation does not hold (one carrying a payload today, an unforeseen spelling tomorrow) refuses the machine rather than shrinking its absence lists; both spellings of a state-to-state edge, transition and first … then …, are walked. The property carrier is a Sysprose metadata definition, and what an external reader makes of it is untested.

The load-bearing gap. The interop client round-trips fully against our own spec-shaped server (§6), and against the live OMG pilot it round-trips a read and a Package write but not what this tool annotates a model with: the verdict-bearing probe of §6.1 is refused as written and, repaired, comes back with every tool-local value dropped. So the gap is no longer "untested" — it is measured, and negative for the evidence record. Re-run it with SYSMLV2_PILOT_URL set and npx tsx scripts/pilot-write-roundtrip.ts. We validate against the published specifications and schemas (clean-room) and our own spec-shaped server, not a running OMG reference implementation. Each pillar is a faithful, load-bearing subset per docs/TEST-REPORT.md §8; the honest residual is the deepest formal-semantics corners, not breadth. Nothing here is a conformance claim: Sysprose has never been conformance-tested by the OMG or anyone else.

How to reproduce

cd sysprose

# Full unit + integration + conformance suite (4688 pass / 0 skip, 157 files)
npm test                    # === npx vitest run

# Just the conformance scorecard suite (71 pass, 4 files)
npx vitest run test/conformance --no-coverage

# Interop self round-trip over HTTP (8 pass, 1 file)
npx vitest run test/interop --no-coverage

# Real .kerml/.sysml corpus parse rate (100 %)
npx tsx scripts/grammar-coverage.ts

# Self round-trip against our own OMG server (push→pull, 13 elements EQUIVALENT)
npm run interop             # or: npx tsx scripts/pilot-roundtrip.ts

# Live-pilot round-trip (requires a reachable OMG SysML v2 pilot server)
SYSMLV2_PILOT_URL=https://pilot.example/api SYSMLV2_PILOT_TOKEN=… npm run interop

# Live-pilot WRITE probe — what a foreign reader does with a verdict (§6.1)
npx tsx scripts/pilot-write-roundtrip.ts

# Networked API / OSLC server (manual smoke)
npm run serve               # then GET /api/... and /oslc/...

# End-to-end (213 tests across 84 spec files)
npm run test:e2e