Follow-ups from the independent type-design review of PR #756 (#747). None affect correctness today — the @Nat guard machinery is sound (every parallel-structure drift is contained by a bounds check and an independent static obligation) — but three invariants are defended in code rather than expressed in the type, so a future change could reintroduce a gap silently. Each is a small, self-contained hardening; theme: one fact, one home, drift caught by a gate.

• Enforce the nat_fields / field_offsets length invariant. ConstructorLayout (vera/codegen/api.py) carries nat_fields: tuple[bool, ...] parallel to field_offsets. For user constructors the two are appended in the same loop (airtight), but the built-in MdHeading layout (vera/codegen/registration.py:170) hand-authors nat_fields=(True, False) as a separate literal — nothing enforces it stays length/order-aligned with the sibling field_offsets literal. Add a __post_init__ assertion that nat_fields == () or len(nat_fields) == len(field_offsets), converting "correct by inspection" into "fails loudly at construction" (~3 lines; layouts are built once, so zero hot-path cost).
• Single-source the expression span key. The checker hand-rolls the verifier's 4-tuple span key (line, column, end_line, end_column) at three write sites (vera/checker/expressions.py:60, vera/checker/calls.py:122) while the verifier has its own _span_key (vera/verifier.py:101). A shared span_key(node) constructor consumed by both sides makes the key format single-sourced, so a change to its shape can't drift the two halves apart.
• Populate the side-table consistently for ability-op calls. _check_ability_op_call (vera/checker/calls.py) synthesises arguments with a bare _synth_expr(arg) (no expected=), so it skips the expr_target_types write its sibling _check_op_call performs. Currently inert (ability-op narrowings aren't obligated by the walker yet), but if ability-op obligation is added later, a generic ability-op formal fixed to @Nat would silently miss because its target was never recorded. Mirror the expected= write pre-emptively.

Surfaced by the multi-agent review of PR #756. The deeper refactor — fold is_nat into a per-field record so the parallel-tuple length invariant becomes structurally unrepresentable — is noted but out of scope here (it touches every field_offsets consumer).