Summary

Functions using handle[State<T>], handle[Exn<T>], and other effect handlers cannot have their postconditions verified by Z3 — they always fall to Tier 3 (runtime checks). This is documented behaviour ("constructs outside the decidable fragment"), but it means the verification system provides zero compile-time guarantees for the most complex Vera programs.

Evidence from VeraBench

In vera-bench#14 we strengthened postconditions on three State-handler problems:

All three are trivially correct, but Z3 can't verify any of them because the function bodies use handle[State<Int>].

Why this matters

Tier 5 is the most important tier for real-world Vera programs — multi-function programs with effects are the target use case. But it's also the tier with the weakest verification guarantees. The contract system is most valuable where it's least capable.

Possible approaches

1. Abstract interpretation of handlers — reason about the handler's state transitions without translating the full effect system to SMT
2. Handler-specific axioms — for well-known patterns like handle[State<T>], generate SMT axioms that model get/put semantics
3. Tier 2 hints for handlers — allow assert statements inside handler bodies that the verifier can use as assumptions
4. Accept Tier 3 — document that effect-heavy code relies on runtime checks and focus verification effort on pure helper functions

This is a long-term research challenge, not a near-term fix. Filing to track the gap.

Relates to

• vera#427 — Tier 2 verification (could help with approach 3)
• vera-bench#14 — postcondition strengthening that exposed this gap