Which exact artifacts were used?
Canonical identity, manifestations, availability, roles, and roots bind a claim to declared inputs. Source correctness additionally requires authority and content review.
Bounded assurance for legal text-state
Check the derivation behind the answer.
Within a declared scope, LawVM identifies source artifacts, accounts for source effects, records typed operations, compares declared writes with independent observations where a profile wires that check, preserves unresolved residuals, and exposes what a separate checker can and cannot validate.
Claim boundary: this assurance is compositional and artifact-scoped. Legal meaning, source completeness, institutional authority, and end-to-end compiler verification require separate evidence.
Read a result correctly
An invariant supports one scoped conclusion.
An invariant is a named property checked over a declared source bundle, profile, time scope, and frontend. A result is meaningful only with its disposition and enforcement mode.
| Crosswalk | What to ask | Result |
|---|---|---|
| Invariant | Which property was checked—source accounting, target and mutation, temporal selection, or projection? | Only that property, within the declared scope. |
| Disposition | Is it established within scope, qualified, blocked, unresolved, invalid, uncheckable, or not claimed? | Missing proof is not a clean result. |
| Frontend maturity | Is the check observe-only or strict-blocking on this lane? | Observe-only records a finding; strict-blocking can prevent scoped promotion. |
| Result | What source, profile, time, and residual account accompany it? | A bounded text-state or review result, never a legal-authority badge. |
UK example: the current UK lane supports target-specific source-chain and comparison review. A universal publication gate or broad consolidation claim requires wider source and manual-compilation coverage.
Source readiness is a prerequisite: missing identity, closure, or coverage produces a blocked readiness account. LawVM returns read-only evidence for institutional disposition.
Seven questions
How a legal text-state claim earns its wording
source identity→declared universe→typed operation→phase-local admission→observed mutation→temporal state→bounded checker
Did anything silently disappear?
A checked universe partitions effects into emitted operations, typed rejections, typed observations, residuals, or violations. Universe completeness additionally requires source-closure evidence.
What typed operation crossed the boundary?
Closure requires named target, payload, source anchor, time, and family-specific fields. Source-language entailment requires an independent semantic check.
Why could it execute?
Permission stays phase-local: a scoped phase validates the exact operation and state head. Enforcement maturity varies across frontends.
What actually changed?
A receipt records writer testimony; a separate tree diff can observe the landed footprint and compare it with the declared target and named allowances.
Why is this the selected state?
Effective time, expiry, temporary overlays, occupancy, identity, branch, and authority regime are distinct. Complete jurisdictional doctrine remains a legal-review question.
What can another program reconstruct?
Experimental read-only checkers validate bounded structural roots, links, and declared transition folding. A stable certificate product requires frozen schemas, release packaging, and ownership.
What remains blocked or unresolved?
The account preserves missing proof as blocked, unresolved, or uncheckable; contradictions as invalid; and work outside the profile as outside scope.
Different mechanisms, different conclusions
Verification has several independent dimensions.
| Mechanism | Can establish | Additional evidence required |
|---|---|---|
| Hashes and roots | Declared artifact identity, integrity, membership | Legal correctness or corpus completeness |
| Typed closure and conservation | Missing states remain represented; declared populations balance | Correct interpretation of the source |
| Observed mutation audit | Actual tree changes agree or disagree with declared footprints | That the source legally justified the declaration |
| Independent trace fold | Declared transitions and roots reconstruct consistently | Source-language entailment or institutional authority |
| Z3 / model checking | Named properties over the encoded model | End-to-end refinement of the production compiler |
| Corpus or publisher evidence | Behavior or adjudication for exact cases | Universal system correctness |
Future strict authoring
Conditions for a future compiler theorem.
Strict authoring is a future direction for legislation represented in a formally specified, machine-checkable language.
For a theorem, the dossier would need a frozen and complete authoritative source bundle; correspondence between human-approved text and its machine artifact; formal grammar, semantics, and rejection rules; sound and complete lowering to typed operations; exact target, identity, and temporal rules; replay and materialization refinement; end-to-end implementation evidence; an independently implemented checker; intact content-addressed artifacts; live guards; and closure of every blocking residual.
Conditional theorem: under those conditions, a clean dossier could establish that generated text-state matches the declared formal semantics for every accepted input in its jurisdiction, profile, and time query. Unsupported or ambiguous input would be rejected or blocked. The institution would retain authority over source status, legal judgment, and publication.
Current gap: end-to-end source-language entailment and implementation-refinement proofs remain open. Current frontends and checks therefore stay scoped, qualified, residual-preserving, or observe-only where their profiles say so.
Progressive disclosure
Enter at the depth you need.
1. Plain-language account
Use the seven questions above to understand the reliance boundary without compiler terminology.
2. Synthetic dossier lab
Compare exact, blocked, violated, and uncheckable teaching fixtures. No certificate claim is attached.
3. Specifications and evidence
Continue into architecture, repository specifications, benchmark artifacts, evidence cases, and formal-model boundaries.
Institutional and reviewer surfaces
Use the assurance case, challenge it, or carry it into a decision.
Institutional assurance brief
A printable account of the bounded claim, pilot formats, outputs, outcomes, and reliance boundary for publishers, ministries, funders, and standards teams.
Verification map
Separate CI gates, generated tests, bounded model proofs, the stale TLA+ abstraction, experimental checking, and external adjudication.
Auditor and reviewer guide
Challenge source scope, accounting, semantics, admission, mutation, time, checker assumptions, and public framing through a structured review sequence.