Corpus Health

Corpus Health is the standing view of whether the rules you have written are coherent with each other. It runs a suite of checks over the rules, axioms and claims in scope and reports what it finds: contradictions, rules that can never fire, alignment that quietly forces a claim to a constant, verdict levels no rule can ever produce, and requirements the corpus does not meet.

What this does not check

Corpus Health checks the rules against each other. It does not check them against the source policy. Nothing here can tell you that a rule faithfully transcribes the regulation it came from, that a threshold is the right threshold, or that a guide's intent survived the translation into DSAIL. A clean report means what you wrote is internally coherent — not that it is correct.

That distinction is repeated in the product's own empty state, because a green badge is exactly the kind of thing that gets read as more than it says.

The Page

Workspace sidebar → Corpus. That lands on Corpus Health; the tab strip switches to the Vocabulary Workbench. Everything is scoped to your active group.

The page has a header, three tabs, and a findings list.

Control	What it does
The headline sentence	The contradiction count, and how many of them exist only because of the alignment — see The headline
Last run … / Never run / Last run unknown	When the reports on screen were produced. Unknown until the page has finished reading them — see Three states
Re-verify	Runs the suite again, ignoring the cache. It runs as a job; the page refreshes when the job finishes
Profile status chips	One per scope profile; click one to filter the page to it, click again to clear
Findings / Coverage / Decisions tabs	The two report surfaces, and every decision recorded about a finding — see Withdrawing a decision. The Decisions tab carries a count when there are any
Four filter selects	Finding class, severity, classification, and ruleset. The class and ruleset lists are built from what the current findings actually contain, so an empty option list means no finding carries that dimension

Selecting a profile chip also scopes Re-verify to that profile. With no profile selected it verifies every declared profile.

If no scope profile has been declared at all, the header says so — "No scope profiles declared — Re-verify checks the whole corpus as one ad hoc scope" — and the run still works. Declaring profiles is what makes the result repeatable and what the publish gate keys on.

Three states, which mean different things

Unknown. While the page is still reading, the headline says "Checking the corpus…" and the timestamp says "Last run unknown". Nothing is called clean, and nothing is called unverified, because neither is known yet.

Unreadable. If the page cannot reach the service, the headline says so — "Corpus Health could not be loaded — the service is unreachable (HTTP 502)" — and the findings area says "Whether this corpus contradicts itself is unknown right now — not resolved." The previous group's findings are discarded rather than left standing, and no clean sentence appears anywhere on the page.

Known. Only then does the page state a result, and it states one of two:

• Verification has not run yet. The headline reads "Never verified — nothing here has been checked", and the findings area says "Nothing has been checked, so this is not a clean bill of health." There is a Run verification button in it. The clean sentence never appears in this state: no report means no result, so "Never run" and "No contradictions" can never be on screen together.
• No inconsistencies found in the checked scopes. A real clean result, with the caveat attached: "This checks the rules against each other — not against the source policy."

The distinction is deliberate, in all three directions. Silence and a pass are not the same thing, and a surface that renders them identically is lying by omission.

Switching groups

The corpus is group-scoped, so every finding, rule id, witness, chip and count on this page belongs to one group. Changing the active group in the header clears the page and re-reads it. Nothing from the previous group is shown under the new one, in either direction — a corpus with live errors never appears as "Never run / No contradictions" because the fetch behind those words has not landed yet.

The Checks Are Data-Free

Every check takes a resolved slice and nothing else. No documents, no claim values, no sample corpus, no generated test cases. Two things follow, and both matter more than they first appear.

The findings are complete, not sampled. A finding is a statement about the whole input space, arrived at by solving. "No document has triggered this contradiction yet" is not evidence of anything; "no input can trigger it" is a proof, and so is its opposite.

They run before any data exists. You can verify a corpus the day it is written, with nothing uploaded and nothing evaluated. That is what makes verification an authoring-time activity rather than a post-mortem one.

Document impact analysis — "which document changes verdict if I add this rule" — is a genuinely different, deliberately data-dependent operation. It lives in Analysis, not here.

What Each Finding Means

The suite runs in stages, cheapest first, and each stage feeds the next. The stage names appear in the report; what follows is what each finding is telling you.

Structural faults

No solver involved. These are the faults that would make every later answer meaningless.

Finding	Severity	What it means, and what to do
empty_slice	error on a publish gate, warning elsewhere	The profile resolved to no rules at all. Nothing contradicts nothing, so without this the run would read clean — indistinguishable from a corpus that was checked and found consistent. On a publish gate it is an error, because a gate over nothing lets everything through while reporting clean. The finding names which emptiness this is, because the fixes are opposite: a ruleset ref naming a ruleset that does not exist (check the spelling, or author a rule into it), or rulesets that do exist whose every rule is tagged for another context (widen the profile's scope, or re-tag the rules). It names the excluding tags and the rules they excluded, so the second case is never reported as the first.
undetermined_solved_for_claim	error	An incomplete claim: no extraction question, and no rule or axiom in scope determines it. It can get a value from neither extraction nor logic, so every verdict depending on it is silently UNKNOWN. Either give it a question or write the rule that determines it. The Registry tab shows the same state, registry-wide, as the claim's extraction status.
unsupported_construct	error	A rule or axiom uses a DSAIL construct the corpus layer cannot compile. Rewrite it in the supported subset.
stale_pin	warning, or info when only documentation moved	A rule in this slice pins a claim version below the registry's current one — measured against the oldest pin any of the slice's rules holds, so a claim two rules pin differently is judged by the rule furthest behind. The version gap raises the finding; what moved grades it. A run reads a claim's question and its declared reading from the current registry, not from the pinned version — so if either has moved, a run asks something this report never checked, and the finding is a warning naming which one. If the newer version changed only a gloss or an owner, a run asks exactly what was checked, and it is an info saying so. Either way nothing is auto-upgraded: read what changed, then Re-pin claims to current on each rule the finding names — which re-resolves that rule's source against the registry and appends a version recording that you accepted the newer wording.
orphan_claim	info	A registry claim in scope that no active rule or axiom names. Not a fault — sometimes it is vocabulary waiting for a rule — but worth a glance.

The run halts here on an unsupported_construct: a slice that cannot be compiled cannot be solved over, and handing the solver something it can only mis-explain produces findings that evaporate the moment the real fault is fixed. The report says it halted rather than pretending to be complete.

There is no finding for a rule that names a claim the registry does not have

Because the corpus does not let that state exist. Two gates, one on each way into it:

• Writing the rule. Load-time validation resolves every @namespace.name before a rule or axiom is stored, and a name the registry does not hold is minted as an unreviewed draft claim and queued for vocabulary review rather than left dangling. The rule stores, its response lists the id under validation.minted, and the draft carries a provisional gloss and question naming the rule it came from. So a typo does not break the rule — it puts a claim in your review queue.
• Deleting the claim afterwards. DELETE /claims/{id} answers 409 while any rule version still links the claim, and names the rules: "Corpus claim clas.portion_level is still linked by 3 rules (alpha.waveform_floor, bravo.waveform_alone_u, mosaic.band_location). A rule whose vocabulary has been deleted stops compiling, so the claim stays. Edit or delete those rules first."

So a verification report has nothing to report here, and looking for a dangling_reference on this page will always come up empty. The corpus fails this closed rather than detecting it after the fact, which is the stronger of the two — a finding would tell you about rules that had already stopped compiling.

Alignment hygiene

The axiom layer is verified in isolation, against the claim domains only, with no rules present at all.

Finding	Severity	What it means, and what to do
axiom_set_inconsistent	error	The axioms contradict each other. Verification halts here. Fix the crosswalk before reading anything else.
axiom_over_constrains	warning	An axiom pins a claim to a single constant for every input — the classic bad bridge, silently rewriting every rule that touches that claim. Almost always an equivalence that should have been an implication.
axiom_vacuous	warning	The axiom is already implied by the others, so it adds nothing. Safe to keep, but it is not doing the work you think it is.
collapse_to_equivalence	info	A cycle of subsumptions that amounts to an equivalence. Usually worth saying so explicitly by replacing the cycle with one alias.

Why it halts. If the crosswalk between vocabularies is itself contradictory, every downstream rule conflict is an artefact of a broken bridge. Reporting them would bury the one finding that matters under a pile of noise that disappears the moment the bridge is fixed. So the report stops, and says it stopped.

One rule at a time

Each rule on its own, against the axiom and domain background.

Finding	Severity	What it means, and what to do
rule_unsatisfiable	error	The rule can never be complied with by any input. As written it fails everything.
rule_never_fires	warning	The rule's condition can never hold, so it is vacuously satisfied and constrains nothing.
rule_tautological	warning	The rule is always true, so it constrains nothing.
verdict_unreachable	warning	A level of an ordered claim that no combination of rules can produce. One finding per level, so a scale with two unproducible levels reports both.

rule_never_fires is the highest-yield check in practice. It catches typos, contradictory conjunctions, and refinements narrowed until nothing satisfies them — rules that look like they are doing work and are not.

verdict_unreachable is the one people are surprised by. A four-level scale where the top level can never be produced means either a missing rule or an unused level, and both are worth knowing before the scale is published.

Rule against rule

Pairs of rules, comparing whether one entails the other. Pairing happens after claim closure, so two rules comparable only through an alias axiom are still compared — which is exactly where cross-source redundancy hides.

rule_subsumed carries a deliberately asymmetric severity:

• Within one ruleset it is a warning. Redundancy inside a single ruleset is usually an authoring mistake.
• Across rulesets it is info. The same requirement genuinely appearing in two policies is expected and often correct — deleting either would lose an authority citation. It is reported as an alignment fact worth recording, not a defect to fix.

rule_subsumed is directional, and two equivalent rules produce two findings — one each way round — because deleting the redundant rule means choosing which of the two is redundant.

Pairwise comparison has a budget. When a very large slice exhausts it the report is marked truncated and carries a verification_truncated finding naming the stage that stopped, which means "not every pair was compared" — not "no more findings exist". The conflict scan below has its own cap and reports the same way.

There is a second budget, and it fails the other way. A verification stage is a series of proofs, and the solver can spend its time on one without deciding it. When that happens the stage stops and the report carries a verification_incomplete finding — an error, not a warning — naming the stage and the query it could not settle. It is an error deliberately: a report with no findings from a stage that never finished is indistinguishable from a clean one, and everything downstream, the publish gate most literally, reads clean as permission. Re-run the verification, or raise the solver budget; a verification_incomplete finding is never dispositioned away as a false positive, because it is not a claim about the rules at all.

The whole slice at once

rules_contradict (error) is the conflict scan: an input assignment under which the rules in scope cannot all hold. Each finding names the rules involved and carries a witness describing the class of inputs that triggers it.

This stage runs twice — once with the axioms and once without — and reports the difference, which is where the headline comes from.

Coverage against what you declared

coverage_gap (warning) reports a stated requirement the rules do not meet. coverage_obligation_invalid (error) reports an obligation that does not compile against the slice — it does not parse, or names a claim the slice does not load. coverage_undetermined (warning) reports an obligation the run reached but could not decide — its target claim is not in the slice, or the solver ran out of budget. All three need a declaration first — see Coverage obligations.

Pass is a finding, not a default. The Coverage badge is derived from the findings a report carries about that obligation: any finding naming it produces a badge that is not green, and the badge for a finding class the page does not recognize is Reported rather than Pass. An obligation reads Pass only when a report evaluated it and said nothing about it. Silence and a pass are not the same thing, and the Coverage tab never renders them identically.

Each finding names the obligation it is about, so two obligations over the same target claim are two findings with two verdicts and two decisions. This is what makes a disposition specific: a decision recorded against one obligation's gap never acknowledges another's.

The Headline

The sentence under the page title is the contradiction count, split by whether the alignment layer caused it:

3 contradictions — 2 appear only under the current alignment.

That single sentence tells a reviewer immediately whether the problem is the policies or the crosswalk written between them. The second clause is dropped rather than printed as "0 appear only under the current alignment", which would read as a finding of its own. With no contradictions at all it reads "No contradictions in the checked scopes."

Reading a Finding

Every finding carries the same anatomy.

A prose summary, built from the rules' and axioms' authored summaries. You should be reading "Revealing waveform X is SECRET. and The existence of waveform X, standing alone, is UNCLASSIFIED. cannot both be honoured" — not a pair of identifiers.

A severity badge — error, warning, or info — and a classification badge.

The implicated rules, each as id@version, with its ruleset and its authority citation — or the explicit "no authority cited", because an uncited rule in a conflict is itself worth noticing.

Claims and axioms named in the core, each a link into the Vocabulary Workbench at that exact entry, and the obligation where the finding is a coverage one.

The core is not decoration — it is the finding's identity. Everything that makes this finding a different finding from its neighbours is in it: which obligation, which unreachable level, which rule entails which. That is what makes a decision about one of them a decision about that one only.

A witness, where one applies: a generalized scenario rather than an assignment dump. The platform starts from a concrete counterexample and drops every condition that turns out to be irrelevant, leaving the class of inputs that actually triggers the finding, rendered as a sentence beginning "any subject where". A reviewer handed a raw forty-claim assignment has to do that generalization in their head, and will get it wrong.

Classification is what routes the finding

Badge	Means	Goes to
Depends on alignment	An axiom is in the core	Vocabulary review
Across rulesets	Rules from more than one ruleset	Governance — a precedence decision
Within this ruleset	One ruleset's rules only	Back to the author
Registry	A structural or registry-level fault	Whoever owns the claim

Alignment takes priority deliberately. A conflict that exists only under the current crosswalk is a claim about vocabulary, not about policy, and sending it to a legal reviewer wastes their time. A Depends on alignment badge is also a link, straight to the implicated axiom.

A worked report

Verifying the corpus built in the SCG Portion Marking Tutorial produces three findings — one error and two warnings — and they are a good tour of the suite. A corpus this small produces no info finding: the two that exist (orphan_claim and collapse_to_equivalence) both need vocabulary the tutorial never writes.

rules_contradict · error · Across rulesets. alpha.waveform_floor@1 (in scg.alpha) and bravo.waveform_alone_u@1 (in scg.bravo) cannot both be honoured.

Revealing waveform X is SECRET. and The existence of waveform X, standing alone, is UNCLASSIFIED. cannot both be honoured.

any subject where not The portion names a deployment site and The portion reveals that waveform X exists and not The portion states the operating band

Alpha floors that portion at S; Bravo caps it at U. Neither rule looks wrong in isolation, and both are faithful transcriptions — the contradiction lives in the pair. Because it is across rulesets, resolving it needs both owners.

verdict_unreachable · warning · Registry.

No rule in scope can produce clas.portion_level = TS — either a rule is missing or the level is unused.

coverage_gap · warning · Registry.

A portion stating the frequency band must never remain UNCLASSIFIED. — but an input exists where it does not hold.

any subject where The portion states the operating band

Nothing in scope forces a level on a portion that merely mentions the band with a low frequency, so it marks U. That is a hole in the rules, and only a declared obligation could have found it.

Dispositions

A finding a reviewer has looked at and decided about should stop re-surfacing. Four actions are offered on every finding row. All four require a rationale — there is no dismiss that leaves no trace, because a finding that stops surfacing with no recorded reason is indistinguishable from one nobody ever looked at.

Accept precedence

Use it when: the disagreement is real, and the resolution is authority rather than wording — one rule governs and the other yields wherever both apply. Choose the governing rule from the finding's own rules; the modal names the one that will yield. Needs a finding with two rules in it, and does not apply otherwise.

Add distinguishing claim

Use it when: reading the witness makes you say "but those two rules mean different things." The corpus is missing a concept. This queues a candidate into the merge queue, prefilled with the claims the witness turned on, records the finding as deferred pending that review, and takes you to the candidate.

Accept redundancy

Use it when: the overlap is real and intended — the expected cross-ruleset case, the same requirement in two policies, both worth keeping for their citations. Record why, so the next reviewer does not re-litigate it.

Not a conflict

Use it when: the finding is wrong, or does not apply here. Record why; this decision is what stops it re-surfacing.

Each disposition also takes a scope, prefilled from the finding's own, recording the context the decision holds under. A recorded decision shows on the finding row from then on, with who decided it, when, and their rationale — and on the Decisions tab, which is where it stays reachable after the finding stops being reported.

Precedence changes what the rules mean

A precedence decision is not bookkeeping — it is compiled. The subordinate rule is guarded so that it does not apply where the governing rule's condition holds, and every subsequent query answers accordingly.

Because that changes rule semantics, the set of active precedence decisions is part of the slice hash. Recording, changing or removing a precedence gives you a different corpus configuration: cached verification reports no longer match, and any approximating model distilled under the old configuration is retired. This is intended — it is what makes it impossible to serve an answer computed under precedence rules that are no longer in force.

Dispositions expire when the rules change

Each disposition is keyed to a fingerprint over the finding's class, its core including every version, and its scope. Bump any implicated rule or axiom and the fingerprint no longer matches, so the finding comes back — flagged "Previously accepted — the rules have changed since", with the prior rationale behind a disclosure.

This is the desired semantics, not an inconvenience. An acknowledgment must not outlive the thing it was about, and a stale approval hiding a live defect is the failure mode the whole mechanism exists to prevent.

Every edit counts, including one that changes only prose. A rule's summary is what a reviewer read when they accepted the exception, so changing it appends a new version and moves the fingerprint exactly as changing the DSAIL would. Re-pinning a rule's claims does the same. The decision does not vanish — it is on the Decisions tab, invalidated, naming which object moved and the finding now reported in its place — but it stops acknowledging anything until someone decides afresh.

Withdrawing a decision

A recorded decision carries Withdraw this decision, behind a confirmation, in two places: on the finding row while a report still raises that finding, and on the Decisions tab always. A judgement nobody can revise is a judgement nobody can correct: without this, a mistaken "not a conflict" keeps a real finding acknowledged — and keeps releasing it through the publish gate — until every implicated rule happens to be bumped.

The Decisions tab is the durable half, and it exists because the finding row is not reliable ground to stand a withdrawal on. A decision can stop having a finding to sit beside: accepting precedence is compiled, so the contradiction it settles genuinely stops being reported; a corpus edited enough stops producing the finding for other reasons; and deleting a scope profile takes its reports with it. The tab lists every decision in the group newest first — what it was about, what was decided, by whom, when, the rationale, and the governing/subordinate pair on a precedence — so none of them is a one-way door.

Each entry also says what the decision is currently doing, which is not the same question as what it says:

Standing	What it means
In force	A current report carries the finding, and this decision is why it is not open
Invalidated by a rule change	The rules moved under it, so the finding is being reported again as "Previously accepted" — this decision no longer acknowledges anything
Not in the current reports	No current report raises the finding in any version. A compiled precedence decision that resolved it looks like this
Its finding is no longer stored	No stored report carries the fingerprint, so the subject cannot be shown — only what the decision itself recorded

An invalidated entry also names what moved — rule:alpha.waveform_floor 3 → 4 — so re-deciding means reading a diff rather than re-reading the corpus.

The standing is part of the decision's API record

It is not something the screen works out for itself. GET /api/v1/corpus/dispositions returns standing and applies on every decision, so a release gate, an audit export or a compliance report reads the same answer this tab shows. applies is true for In force and for nothing else — the other three standings all mean the decision is holding nothing open. See Corpus API.

The confirmation states the consequence for that decision rather than one sentence for the easy case. A decision in force: the finding reads as open again and the gate stops releasing what it was holding back. A decision whose finding nothing currently raises: nothing on the Findings tab changes today, and re-verifying is what shows what the corpus reports without it. A precedence decision adds that it is part of the slice hash, so withdrawing it makes every report that ran with it stale. In every case the old rationale is not kept; record a new decision if you want one on the record.

Coverage Obligations

The checks above find things that are wrong. Finding things that are missing needs a declaration, because a corpus has unbounded unregulated inputs and "coverage gap" is undefined without a stated domain of discourse. The Coverage tab says so on the page: "an unregulated input is not a gap until someone says it should have been determined."

Declaring one

Coverage tab → Declare obligation. Four fields plus scope:

Field	What to put in it
Summary	The obligation as a sentence a reviewer can judge: "A portion stating the frequency band must never remain UNCLASSIFIED."
Predicate (DSAIL)	A boolean expression naming the inputs the obligation is about: @sys.freq_band_mentioned. Conjunctions are normal — And(@sys.freq_band_mentioned, @ops.deploy_location_mentioned).
Target claim	The claim that must be determined for those inputs — picked from the registry, not typed.
Requirement	Must be determinate (the target must get some value) or Must not equal default (the target must move off a stated default).
Default value	Only for the second requirement: the value the target must not remain at, e.g. 0.
Scope	Comma-separated tags the obligation applies under. Leave empty and it applies wherever its target claim is in the slice.

Verification then searches for an input that satisfies the predicate and violates the requirement. If one exists the obligation has a gap, and the gap arrives with the generalized witness describing which inputs fall through.

The two requirements answer different questions. Must be determinate catches a verdict the rules leave open. Must not equal default catches a verdict the rules leave at its floor — which is the more common real-world failure, because "we never decided" and "we decided it was fine" look identical from outside.

Three rejections happen at the dialog, not at the next verification run. The test is the same one in all three cases: an obligation that cannot compile is an obligation no run can check, so it is refused here rather than becoming a permanent coverage_obligation_invalid.

• A claim that is not in the registry — a misspelling, most often — is refused with the name in the message.
• A predicate that does not parse is refused with a sentence about your own text — "the '(' at character 4 is never closed and the ',' at the end has no argument after it" — rather than a parser position, because a bare expression is parsed inside a synthetic assertion and the parser's line, column and offending token belong to that wrapper.
• A predicate that does not type-check is refused in the same words the axiom and rule editors use for it — "claim '@sys.freq_band_mentioned' is declared boolean but is used where numeric is required" — because all three surfaces compile the source through one checker rather than each carrying its own opinion about what DSAIL means.

The type check here is deliberately registry-wide, not scoped to a profile. Identifier resolution happens first inside one compile, so a slice-scoped check fails on the first name the profile does not reach and never gets as far as the types — which is how a scope fault comes to hide a type fault behind it. Against the whole registry nothing is out of slice, so the type fault is the one you see. Whether a particular profile reaches the claims is a separate question, and its answer is that profile's report.

Reading the tab

Each obligation shows its summary, its predicate, its id at the version it is currently declared at, its target and requirement, the scope it applies under — or every context, when it carries no tags — a badge, and which report that badge came from. Under it, one row per report that could speak to the obligation, each carrying that report's own verdict, that report's own explanation and, where it produced one, that report's own witness.

That structure is the point. A verdict is a property of a report, so nothing on a card is ever assembled from two of them: a card carrying one profile's Gap badge above another profile's "not checked" explanation above the first one's witness is three answers stacked into one, and each part of it is true of something different.

With more than one profile's report in view — which is what the tab shows when no profile chip is selected — the headline badge is the strongest verdict across the reports, and it names the profile it came from.

"Strongest" here means most informative, in three bands: an adverse finding first (Gap, Invalid, Reported), then Pass, then the ways of having no answer (Stale, Not checked, Not verified). Both halves of that matter. An adverse finding always outranks a Pass, so one profile's Pass can never bury another profile's gap. And a Pass outranks a silence, because a profile that actually evaluated the obligation has more to say about it than one that did not — an obligation checked and passed by exactly one profile headlines Pass, from that profile, not "Not checked" attributed to a profile with nothing to say. The attribution is what makes the headline readable rather than merely alarming, and the per-profile rows below always carry every profile's own verdict whichever way the headline went.

Selecting a profile chip narrows this tab the same way it narrows the findings, and by the same test the server uses: an obligation is shown when every tag it carries is one the profile names, and an untagged obligation is shown under every profile. The tab then says which profile it is narrowed to and how many obligations that left out.

Which obligations a profile answers for

A profile can bound itself two ways, and which bound it uses decides which obligations reach its verification:

• It names scope tags. An obligation reaches it when every tag the obligation carries is one the profile names. An untagged obligation carries no context requirement, so it reaches every profile.
• It names only rulesets. Then it never names a context to load one under, so a context-tagged obligation does not reach it at all. Only untagged obligations do.
• It names neither. That is the whole group: every claim is in the slice, so every obligation is checkable there and every obligation reaches it.

The middle case is the one worth understanding, because a profile selecting by ruleset is an ordinary way to define one and its scope is legitimately empty. Read as "no filter", an empty scope pulled in every obligation in the group — so an obligation about a radio-frequency corpus was checked against a fair-housing profile, could not be decided there because none of its vocabulary was in the slice, and came back as a Not checked warning. On a publish-gate profile that is not merely noise: it held the profile's chip off Clean, and the obligation clock ran with it. (It does not block the gate — condition 5 blocks on a warning whose core names the rule or axiom being published, and this finding's core names an obligation.)

The obligation clock is narrowed by exactly the same rule, and has to be: read wider than the set a report was verified against, declaring one obligation anywhere in the group marked every profile's report stale and blocked every gate on stale_obligations.

An untagged obligation still reaches a ruleset-bounded profile, and that is deliberate: with no tags it names no context to be excluded by. If it is about vocabulary a profile does not govern, its report will say Not checked — which is the correct answer to a requirement someone declared as applying everywhere.

There are two ways out, and they answer different questions. Give the obligation a scope tag if it was only ever meant to bind one context — a one-field edit, and the profiles that do not name that tag stop being asked. Record a decision on the finding if the obligation really is global and this profile genuinely cannot answer it: the warning goes on being reported, with your reason attached, and the profile's chip returns to Clean. Editing the obligation afterwards bumps its version, which retires the decision and brings the warning back for a fresh look — see Dispositions expire when the rules change.

Badge	What it means
Gap	A run found an input that satisfies the predicate and violates the requirement
Invalid	The obligation does not compile against this profile's slice. The finding names which cause it was: a claim the registry does not hold at all (fix the spelling), or a claim the registry holds that this profile's rulesets do not read (fix the scope — see below). Withdraw it or fix it; no run can check it
Reported	A run reported something about this obligation that this page has no specific badge for. Never a Pass
Not checked	A run reached the obligation and could not decide it — its target claim is not in the slice, or the solver ran out of budget
Stale	The report that checked it was run against a corpus that has since changed, so what it found no longer stands
Not verified	No report speaks to this obligation: none has run, none ran after it was declared, or the ones that ran do not cover its scope
Pass	A report checked this obligation and found no input that violates it

Pass is the only badge that requires positive evidence, and every other state is grey, amber or red on purpose. It is the same principle as the page's empty states: an obligation that has not been through a verification run is unknown, not clean. Declaring an obligation does not check it; Re-verify does.

A newly declared obligation reads Not verified even when reports exist, with the reason on its row — "declared after the last verification run, so no report covers it — re-verify to check it" — because a report only checked the obligations that existed when it ran. Declaring, editing or withdrawing an obligation also marks the profile's report stale: obligations are a declared input to verification alongside the slice, so a change that leaves the slice hash untouched still changes what verification would find.

Not verified and Stale are different states, and a never-checked obligation is never Stale. Because declaring an obligation is itself a change that stales the reports around it, the two conditions are true at the same moment for a brand-new obligation — so whether a report ever covered it is decided first. Staleness is a property of an answer: it says what a report found no longer stands. Where no report ever found anything, there is no answer to have gone stale, and the honest badge is Not verified.

Editing and withdrawing one

Each obligation card carries Edit and Withdraw. Declare is not a one-way door: an obligation with a typo would otherwise be a permanent error finding.

Editing supersedes by version. Saving records the next version rather than rewriting the current one, because every stored report cites the obligations it checked as id@version — a rewritten version would leave those citations describing wording that no longer exists, and the report would go on presenting a verdict under text nobody can read. The new version's timestamp is also what marks those reports stale, so nothing reads as a verdict on the new wording until you re-verify.

Withdrawing takes everything computed from it. Every version of the obligation goes, the coverage findings about it are withdrawn from the reports that carry them, and any dispositions recorded against those findings go with them. The affected reports keep every other finding, have their status and counts recomputed downward, and are marked stale. The page reports what the withdrawal removed rather than leaving it implicit.

This is the one amendment a stored report ever takes, and it is only ever subtractive. An obligation is a declared input to verification and not part of the slice, so removing findings about a withdrawn one leaves the report's slice-hash correspondence exactly as it was — while the alternative leaves an error citing an obligation nobody can open, edit or withdraw.

Scope Profiles and Staleness

Consistency is a property of a resolved slice, so verification always runs per declared scope profile — never over every possible combination of scope tags, which nobody wants a report on.

A scope profile is a named combination: a scope tag set, the corpus rulesets in play, and whether it is a publish gate.

The header carries one status chip per profile. A finding present in every profile is a corpus-level defect; a finding in one profile only is a scope-interaction defect, usually a missing scope tag on a rule or an axiom. The report set names the profiles it checked, because "the corpus is verified" is meaningless without them.

Stale is a first-class status. When a profile's current slice hash no longer matches its last report's — or a coverage obligation the profile answers for was declared or edited after the report ran — the chip reads Stale — "the corpus changed since this run" — and that outranks whatever the report concluded. A green badge against an edited corpus is worse than no badge at all. A profile with no report for its current slice reads Unverified.

A chip reads what is still open, not what the run found. Those are two questions and the report answers both: status is the immutable record of what the checks produced, and open_status counts only the findings nobody has decided. The chip shows the second, and says so when they differ — "1 decided finding; the run itself found warnings".

This is what makes a status recoverable. Without it, one finding a reviewer had read, accepted and written a rationale for held a profile off Clean permanently, with no way back short of editing the corpus — and a standing nobody can recover from is one people stop reading. The finding itself is never hidden: it stays on the Findings tab with its decision, its decider and their reason attached, and the headline still counts it. Only the chip moves.

Two things it deliberately does not do. It never softens Halted — a run that stopped at V0 or V1 never reached most of the corpus, so deciding the findings it did produce says nothing about the checks it never ran. And Stale still outranks it: a decision about yesterday's finding is not a verdict on today's corpus.

What staleness does not cover: a claim edited after the rules pinned it

A slice pins claim versions. A rule's claim links are frozen at the rule version that wrote them, so editing a registry claim afterwards moves neither the pin nor the slice hash, and every report goes on correctly reading current — it describes the version it verified, and that version has not changed.

Evaluation does not pin. A ruleset rule naming @ns.foo carries no version, so its runs inherit the claim's current question and its current declared reading. Reword a governed claim and a run starts asking the new wording while every verification report describes the older one.

Neither behaviour is wrong and staleness is not the lever for it: the reports are accurate about what they checked. Two other things say it, and both are graded by whether a run's question moved or only a gloss did: stale_pin in the report itself — warning when a live-read field moved, info when the newer version is documentation — and Ahead of verification on the claim in the Vocabulary Workbench, which names the pinned version and what changed since.

Clearing it is one action. Open the rule in the Vocabulary Workbench, and if any of its pins are behind the editor says so above the source and offers Re-pin claims to current. That re-resolves the rule's existing source against the registry as it stands now and appends a version recording that you accepted the newer wording; it changes nothing else about the rule and keeps its ruleset membership. Re-pin every rule a finding names and the finding goes. Until something does, the finding stays for good — pins are never upgraded on their own, which is the point, and rewriting them otherwise happens only when a rule's source is edited.

Reports are immutable and keyed by slice hash. An unchanged corpus with an unchanged obligation set returns its cached report rather than re-solving; Re-verify forces a fresh run and records it, so the Last run timestamp always names a run that actually happened.

Declaring a profile. New profile on this page opens the editor: name it, give it the scope tags and rulesets that define its slice, and say whether it is a publish gate. Selecting a profile chip and clicking Edit profile reopens it.

The Rulesets list offers the corpus rulesets that already exist, each at a version. A bare id verifies every version of that ruleset; id@version verifies exactly one.

A ruleset ref that names no ruleset is refused at save, with the name in the message, exactly as a mistyped claim is refused in the obligation dialog. This is the more dangerous of the two typos. A bad claim name in an obligation becomes a visible coverage_obligation_invalid; a bad ruleset ref in a profile resolves to an empty slice, and an empty slice has no contradictions in it — so the profile reports clean, indistinguishable from a corpus that has been checked and found consistent. Only rulesets a rule actually belongs to are offered, too: a ruleset comes into being when a rule is authored into it, so naming one does not create it, and one mistyped ref cannot become a permanent option in every profile editor. A ref a profile already carries is still shown so it can be seen and unticked, marked as naming nothing.

Should a profile end up resolving no rules anyway — the last rule of its ruleset was deleted, say, or its scope tags exclude every rule the ruleset holds — verification says so: the report carries an empty slice finding instead of reading clean, and the headline names it rather than reporting "No contradictions in the checked scopes" over nothing. The finding distinguishes the causes, because they need different fixes: a ruleset that does not exist is a typo in the profile, while rules that exist and are out of scope are a scope the profile did not ask for — and being told the second as though it were the first sends you to open a ruleset that turns out to hold rules.

Publish gate is the switch worth pausing on: turning it on means a verification error in this slice stops anything from publishing, so enable it once the slice's rules are settled rather than while they are still moving. A publish-gate profile whose slice holds no rules never passes the gate — a gate over nothing would let everything through while reporting clean — and that is decided from the resolved slice rather than from a stored report, so a report from before the rules went cannot go on satisfying it.

Deleting a profile. The editor carries Delete, behind a confirmation that states what goes with it. A profile is the subject its verification reports are about: once the combination is gone nothing can re-run it or say whether what it found still holds, so its reports go too, along with the decisions recorded against findings that survive in no other profile's report. Decisions about findings another report still carries are kept. The page reports the counts rather than leaving them implicit.

Supplementary: declaring a profile over the API

The same declaration is a POST to the scope-profiles endpoint — see the Corpus API. Nothing on this page requires it.

Preflight: Checking While You Write

The same checks run against a draft rule or axiom before it is saved, in a panel docked beside the editor — both the axiom editor and the rule editor. The same check backs two of the Analysis questions — the one about a proposed rule and the one about a possibly-redundant rule.

The panel shows only what your draft introduces. Pre-existing findings in the same scope are collapsed to a single count rather than mixed in. That is correctness for the surface rather than an optimization: an author editing one rule needs to see the findings their edit caused, or the panel becomes noise they learn to dismiss.

Findings are grouped by severity, errors first, each rendered as prose with the DSAIL and the raw core available behind a disclosure, and the pre-existing count links to the full report. The header also shows the vetting ladder and a publish-gate badge, which reads Gate not run until a publish attempt has actually been refused. The draft is never persisted, and the check does not block editing while it runs.

Preflight models the save it precedes. An @namespace.name the registry does not hold is not a source that will not load — saving mints it as an unreviewed draft claim — so preflight reports it as vocabulary a save would create, names it, and says that nothing has been written yet. Where the name sits one edit from a claim the registry already holds, it names that claim too, from the same matcher the save receipt uses. This is the earlier and cheaper place to catch a typo: before the claim and its review-queue entry exist, rather than after. A source that genuinely will not load — a syntax fault, a type error, an undeclared bare name, which is local by definition and cannot mint — is still reported as an error, and preflight still stops before solving.

The subtraction needs a current report

"What this draft introduces" is computed by subtracting the last stored report for the current slice. If the corpus has changed since the last verification run there is nothing to subtract against, and a pre-existing finding can read as one your draft caused. Run Re-verify first when the result surprises you.

The Publish Gate

Moving a rule or an axiom toward authoritative is gated on verification, which turns "check before it is used" from a procedure into a structural fact. Five conditions, all of which must hold for every scope profile flagged as a publish gate:

1. The profile's current slice resolves at least one rule. A gate over nothing passes every check below it vacuously, so it would let everything through while reporting clean. This is read from the resolved slice rather than from a report, so a report stored before the rules were removed cannot go on satisfying it.
2. A verification report exists whose slice hash matches that profile's current resolved slice.
3. That report ran after the newest coverage obligation declared against the profile's scope. Declaring an obligation leaves the slice hash identical, so without this clause the gate would clear on a run that never checked the requirement.
4. That report has zero error findings.
5. Every warning implicating this exact rule or axiom version has a recorded disposition.

A deployment that has declared no publish-gate profile has declared no gate, and the check passes by construction.

Marking rulesets pass a second version of it

A platform ruleset that declares a Mark target solves a level out of these rules and hands it out as a determination, so publishing one is gated here too — from the same profiles, the same reports and the same obligations clock. What differs is the subject, and three things follow from that:

• The ruleset names its own slice. A version declares the corpus rulesets it answers to, and the gate asks whether a publish-gate profile covers those. A ruleset that declares a Mark target but names no corpus ruleset is refused: there is nothing to verify. So is one whose cited rulesets no publish-gate profile names — an empty gate blocks here rather than passing, because the mark's authority is the verification of exactly the rulesets it cites.
• Warnings never block it, and a dispositioned error does not either. A ruleset appears in no finding's core, so condition 5 has no analogue. Errors block until the finding is dispositioned — unlike a rule's own transition, where they are never waivable — because the ruleset publish takes no override, and a block with no way through at all is the one that gets routed around outside the system.
• The rules a run would actually use are checked, not just the ruleset names. A profile pinned to scg.alpha@1 while the ruleset cites scg.alpha (every version), or scope tags that drop a rule a run keeps — a run resolves its marking slice under no scope filter — leaves rules in the mark's program and out of the proof. The gate names them.

The blockers and their exact remedies are in the Rulesets API; the semantics of the mark itself are in Runs.

Clearing it

Failing the gate refuses the transition and names every blocker inline. Each blocker says which of the five conditions failed:

Blocker	What to do
empty_slice	Follow the cause the finding names — fix the ruleset ref, or widen the profile's scope to the tags it reports — or clear its publish gate. A gate whose slice resolves to no rules checks nothing and would pass anything — decided from the resolved slice, not from a report, so a report stored before the rules went cannot satisfy it.
no_report	Re-verify the profile. Its slice has changed since the last report.
stale_obligations	Re-verify the profile. A coverage obligation was declared after its last report, so that report never checked it.
open_error	Fix the error finding, or dispose of the thing causing it. Errors are never waivable by disposition.
undisposed_warning	Record a disposition on the named warning — with a rationale, as always.

The normal path is: Re-verify → clear the errors → dispose of the warnings that implicate your rule → set vetting to authoritative.

Overriding it

An override is permitted and never silent. Supply both an override reason and an approver with the vetting transition and it proceeds, writing the reason and the approver against each blocking finding, where they show on the object from then on.

That is a deliberate trade. A hard block with no escape hatch gets routed around outside the system — someone ships the rule as a "temporary" ruleset instead — which is strictly worse than recording who signed off and why.

Related Concepts

• The Corpus — claims, the @ sigil, axioms, scopes, slices, ordered verdicts, and the vocabulary these checks verify
• Vocabulary Workbench — the registry, the merge queue, promotion, and where axioms are authored and preflighted
• Analysis — the data-dependent counterpart, and the surface that asks these same questions about a project's runs
• Corpus API — verification, preflight, dispositions, obligations and scope profiles
• SCG Portion Marking Tutorial — a walkthrough that deliberately produces the contradiction above and decides what to do about it