[enmand]

Summary

Stacked on #25, which carries the checks that run unattended. These three run inside an agent workflow, where a person or a reviewing agent acts on the output.

Packet check (tools/check_packet.py) — before approval. Structure is read in code: required sections, rows in the assumptions and test-matrix tables, cited invariant IDs that exist. Each binding statement is then asked whether an implementation producing the same observable behaviour by another route would still violate it. A yes means mechanism stated as contract, which forbids the idiomatic substitutions implement-contract.md explicitly allows. One further question asks whether the packet presents parity behaviour as normative DWN semantics.

Change check (tools/check_change_quality.py) — before handing off, and during review. Per changed file, in whatever language it is written in: unfinished behaviour behind a finished-looking surface, behaviour no test exercises, a dropped or panicking failure path, mechanism fighting the local idiom, and work beyond the intent. --intent carries the approved packet and the issue, so scope and coverage are judged against what the change is for rather than against its own commit messages. --questions asks the change's own questions, derived from the packet's test matrix; a file-scoped question rides with the built-ins at no extra request.

This does not replace cargo clippy, cargo test, tsc or eslint. Both playbooks say to run those first, because they decide their questions exactly. These are the questions those tools cannot see.

Coverage check (tools/check_invariant_coverage.py) — what the suites actually reach. Tests naming an invariant are found in code, candidates by name overlap are judged by name, and the best are judged again with their source in view, always against the same question: would this test fail if the rule were violated?

What the first real run found

Across 8,347 tests and 56 invariants: 28 tagged and judged covering, 9 tagged but not judged covering, 7 untagged but judged covering, 12 with nothing found.

Reading the nine overclaiming tags by hand:

• Four — DWN-ENC-001, DWN-ID-001, DWN-REC-001, DWN-AUTH-003 — state distinctions rather than behaviours ("verification does not by itself authorize"). No single test can fail because two concepts were conflated in the abstract, and their tags mark the area instead. DWN-AUTH-003's ten tagged tests assert signature rejection and grant-authorized visibility; none asserts the Author stays the grantee.
• Three are compound statements where one clause is proved exactly and another is not addressed, so a whole-statement answer lands mid-range.
• One, DWN-REC-005, is genuinely covered and the judgement was 0.02 under the line.
• One, DWN-AUTH-006, looks like a real gap: replication bypass is testable, and its 11 tags sit on neighbouring admission tests.

Seven invariants have coverage nobody tagged, including DWN-AUTH-007 at 0.84 by a test currently tagged DWN-AUTH-003.

Source / provenance checklist

• I identified whether this change is normative, implementation, or decision knowledge — tooling and process only.
• Spec-derived claims checked; no spec-reviewed date changed.
• Implementation-derived claims checked; no upstream-baseline or reviewed date changed.
• TypeScript reference behavior and Rust behavior are distinguished where they differ — the coverage check searches both and reports each test by path.
• Known divergences linked rather than presented as resolved.
• No review date or baseline updated without re-checking the source.

Behavior-change checklist

Not applicable. No engine behaviour changes, and no invariant statement is edited. The coverage findings above are reported, not acted on.

Drift

• A tag is a claim and a probability is a judgement; only a failing test proves coverage. The report keeps the columns apart and says so, and nothing here should be read as evidence of conformance.
• The 0.6 threshold is too blunt: four of the nine sit in 0.5–0.6, where partial and compound coverage lands. Three bands would report better than one cutoff.
• Compound invariant statements are judged whole, so a half-covered statement scores mid-range. Per-clause judging is the fix, and is not implemented.
• The registry findings above — mis-tagged tests, framing invariants that no test can prove, one real gap — are left for a follow-up rather than changed here.

[enmand]

Closing unmerged. The checks here judge rather than verify, and their errors correlate with the agent writing the code, so they are not verification. Invariant coverage produced real findings as triage — a mis-tagged DWN-AUTH-003 test, seven untagged-but-covered invariants, four invariants that state distinctions no test can prove, and a probable gap in DWN-AUTH-006 — and those are recorded here for whoever acts on them. The deterministic path to the same goal is the cross-runtime corpus in enbox-rust-core#252 and enbox#1660.