Surfaced by the independent multi-agent review of PR #756 (part of the #747 narrowing-obligation work). Two @Nat narrowing positions are not statically obligated by the verifier, so a vera verify-clean program can store/return a negative @Nat. Both are pre-existing — reproduced on v0.0.172 (base 7fb53ac), not introduced by #747/#756 — but #747 generalized the binding-site obligation and its docs implied completeness, so these are the remaining holes. Documentation softened in #756 to stop claiming universal soundness and to point here.

1. Function return position (confirmed firsthand)

public fn to_nat(@Int -> @Nat) requires(true) ensures(true) effects(pure) { @Int.0 }

vera verify → OK: 4 verified (Tier 1), no E503/E504. At runtime to_nat(0 - 5) returns -5 through the @Nat slot, no trap. The narrowing walker _walk_for_nat_binding_obligations (vera/verifier.py) walks the body for binding sites but never treats the function's own return slot as a narrowing site, and codegen emits no return-coercion guard. The implicit @Nat result invariant is enforced only if the author writes ensures(@Nat.result >= 0) explicitly.

2. Value-position tuple / constructor components (confirmed firsthand)

public fn mk(@Int -> @Tuple<Nat, Nat>) requires(true) ensures(true) effects(pure) { Tuple(@Int.0, 5) }

vera verify → OK: 2 verified (Tier 1), no obligation on the @Int.0 -> @Nat first-component narrowing. The per-component @Nat target of a Tuple(...) / constructor call built in value (return / argument) position is not threaded down to the call's arguments, so the field-narrowing loop never fires. (Contrast the let-destructure path, which is obligated.)

Fix sketch

Both are statically checkable today via the existing checker→verifier side-table (expr_semantic_types / expr_target_types):

• Return slot: in the narrowing walker, treat the function's declared return type vs. the body tail-expression's result type as a narrowing site (mirror the existing binding-site obligation + the Tier-3 runtime guard).
• Value-position components: consult the side-table for a ConstructorCall / Tuple(...) expression's resolved (instantiated) type and obligate each component whose target is @Nat but whose argument is @Int — the same shape already handled for let-destructure and for ADT sub-patterns.

Until fixed, vera verify-clean is not a guarantee of "no negative @Nat" for functions that narrow at the return slot or build a @Nat-component tuple/constructor in value position.