Z3
SMT proofs establish named propositions for deliberately encoded finite models. Their assumptions and mapping to production code remain separate review objects.
Bounded verification map
Different tools establish different properties.
LawVM combines CI checks, runtime contracts, generated tests, bounded model proofs, experimental independent checking, and case-specific external review. Each conclusion stays inside its mechanism and scope.
Maximum claim: this public projection maps named mechanisms to bounded properties. A formal certificate, complete test inventory, external audit, and frontend-by-frontend gate evidence require additional artifacts.
Property → tool → gate
What runs, what blocks, and what remains bounded
| Mechanism | When | Blocking? | Establishes | Outside this mechanism |
|---|---|---|---|---|
| Ruff and Ty | CI | yes | Declared lint and type properties | Replay or legal-state correctness |
| Runtime construction contracts | Construction / runtime | yes | Named carrier and tree-operation invariants | Complete jurisdictional semantics |
| Property, stateful, metamorphic, and exhaustive tests | CI / selected suites | yes | Named properties over real code, generated cases, and bounded spaces | Proof over every input or source universe |
| Z3 models | Manual | no | Temporal, occupancy, and precedence properties for exact encodings | Model-to-Python refinement |
| TLA+ temporal-overlay model | Not TLC-run in current harness | no | An inspectable finite abstraction and invariant vocabulary | Current implementation conformance; the model is structurally stale |
| Executable temporal mirrors | CI | yes | Selected temporal invariants against the real selector | Complete legal-time doctrine or every model invariant |
| Experimental structural / trace checker | Repository fixtures | no | Bounded roots, links, and declared transition folding | Source-language entailment, authority, or a stable certificate product |
| External publisher or expert review | Case-specific | outside CI | Disposition of the exact reviewed case | Global accuracy or completeness |
Model-to-code drift
Executable tests check the current selector.
TLA+
The temporal-overlay source model preserves invariant vocabulary. Later expiry, tombstone behavior, and a regime-handoff rule remain to be incorporated.
Hypothesis mirrors
Generated tests call the actual selector for selected invariants, so implementation drift can fail CI. They still cover declared properties rather than all legal-time semantics.
Proof boundary
Open end-to-end proof obligations.
Refinement gap
A formal map from the TLA+ and Z3 abstractions to the production Python implementation remains open.
Amendment-semantics gap
Arbitrary legislative prose still requires a general formal semantics and independent entailment checker.
Profile-specific enforcement
Mutation observation, receipts, admission, and blocking differ by frontend, family, profile, and lane.
External audit gap
A complete audit would need independent review of the implementation, source universe, evidence plane, and release process.