First-class assurance boundary
Proof claims stop at declared boundaries.
A LawVM account establishes bounded properties of a declared derivation. Broader reliance requires source closure, legal interpretation, stable schemas, and the applicable proof artifacts.
Trust boundary
What a checker still has to trust
| Boundary | Current account |
|---|---|
| Assumed from outside LawVM | The declared keeper and source role are appropriate; supplied bytes reflect the intended publications; the source horizon is adequate; local legal assumptions are correct. |
| Currently trusted or not independently reconstructed | Much source-language parsing and jurisdictional lowering; some identity/migration decisions; checker implementation correctness; frontend-specific admission wiring. |
| Independently checkable in bounded experimental fixtures | Canonical roots and links, declared set/delete transition folding, selected coverage/totality relationships, and structural cross-links. |
| External corroboration | Official before/after witnesses, legal-expert review, publisher confirmation/refutation, or a future independent implementation/audit. |
Current proof boundary
Claims requiring additional evidence
Global source completeness
Closure beyond the declared horizon requires an authoritative account of every legally relevant source.
Source-keeper correctness
A hash establishes identity. Publication correctness requires source authority, custody, and content review.
General source-to-operation entailment
Arbitrary legislative prose requires a general independent checker connecting its meaning to the canonical operation emitted by a frontend.
Legal interpretation or authority
Doctrine, constitutional validity, application to facts, legislative intent, and institutional authority remain with competent legal institutions and reviewers.
End-to-end formal verification
Z3 and TLA+ work covers named abstractions. Model-to-Python refinement and a whole-system formal audit remain open.
Uniform frontend enforcement
Receipt, mutation-audit, admission, PIT, and certificate maturity differ by frontend, operation family, profile, and corpus.
A stable certificate product
Production reliance requires frozen schemas, ownership, compatibility, CLI behavior, and release packaging around the experimental checker and bundle machinery.
Comparison-surface authority
Agreement with an official or editorial consolidation is corroboration. Disagreement starts a source review.
UNCHECKABLE. Review resumes when the committed artifact is supplied.The largest open assurance gap
Independently recheck the source-to-operation step.
The highest-value core-repository work is a narrow independent entailment checker for one operation family at a time: confirm the exact source span, grammar version, operative verb, target expression, payload, ambiguity state, and emitted operation without invoking the original lowering implementation.
This roadmap item becomes a public capability after its checker, fixtures, and supported operation-family contract are released.