E525 promises a runtime termination check that is never emitted — a non-terminating program passes check, passes verify, and hangs

`E525` tells the user a termination metric "will be checked at runtime". Nothing checks it. A non-terminating program passes `check`, passes `verify`, and runs forever. Found by the VeraBench v0.0.18 sweep — `VB-T4-006`, Claude Opus 4.8 — and reproduced minimally below. ## What actually happens The static tier behaves correctly. It **declines** to verify the measure and says so: ``` warning: [E525] Termination metric in 'spin' cannot be statically verified yet. Contract will be checked at runtime. ``` and the obligation stream is honest about it: ``` decreases tier3 @List.1 ``` So this is not a false Tier-1 claim, and the headline "termination checking let it through" undersells what is wrong. The static tier did its job. **The Tier-3 fallback it promises does not exist.** ## Reproduction ```vera private data List { Nil, Cons(Int, List) } private fn spin(@List, @List -> @List) requires(true) ensures(true) decreases(@List.1) effects(pure) { spin(@List.1, @List.0) } ``` The recursive call passes its arguments straight through, so no measure decreases under any reading. ``` $ vera check spin.vera OK $ vera verify spin.vera warning: [E525] ... Contract will be checked at runtime. OK Verification: 7 verified (Tier 1), 2 runtime checks (Tier 3) $ vera run spin.vera (still running after 30s — killed) ``` ## Why the runtime check is absent `decreases` has no runtime lowering. Grepping `vera/codegen/` and `vera/wasm/` finds the identifier only inside comments about evaluating contract *predicates* — there is no measure-tracking or termination guard anywhere in emission, and the WAT for the program above contains none. This is a gap specific to `decreases`. Its Tier-3 siblings do deliver: `E521`–`E524` fall back on `requires` / `ensures`, which lower to real runtime assertions. `E525` is the one member of that family whose fallback has nothing behind it, so the sentence it shares with them — *"Contract will be checked at runtime"* — is true for the others and false here. ## Why this matters more than an ordinary gap A verifier is allowed to say "I could not prove this". That is the tiering design working, and the whole point of Tier 3 is that a declined proof degrades to a guard rather than to nothing. What it must not do is claim a check it never performs. A user who reads the E525 warning is told the program is protected at run time; it is not, and the failure mode is a hang rather than a diagnostic. The narrow reading is that one diagnostic overstates. The broader one is that the tier boundary is only trustworthy if every Tier-3 promise is backed by emitted code, and nothing currently enforces that correspondence. ## Directions Any of these closes the honesty gap; they are not equivalent in cost. 1. **Emit the guard.** Track the measure across recursive calls and trap when it fails to decrease. Genuinely delivers what E525 promises; the most work, and needs a decision about measures whose ordering is not obvious at run time. 2. **Extend static coverage.** The warning says the measure "cannot be translated to Z3" — an ADT argument reached by a `match` is structurally decreasing in the cases the conformance suite already covers, so some of these could move to Tier 1 rather than needing a guard at all. 3. **Change the wording, as a stopgap.** If no guard is emitted, E525 should say the metric is *unchecked*, not that it will be checked at runtime. Cheap, honest, and does not pretend the hole is closed. A gate belongs with whichever is chosen: a check that every Tier-3-capable diagnostic has a corresponding runtime emission, so the next code added to that family cannot inherit the same empty promise. The existing verifier↔codegen differential (#813-era) is the closest precedent for that shape. ## Environment Vera v0.1.8, macOS 15, Python 3.14.