Audit Finding

Currently 10 of 13 example programs fall to Tier 3 (runtime check fallback) because the SMT translation layer only handles the decidable QF_LIA + Boolean fragment. Programs involving recursion, pattern matching, generics, quantifiers, or effect operations cannot be statically verified.

What falls to Tier 3 today

• Recursion — factorial, mutual_recursion, list_ops
• Pattern matching — match expressions in function bodies
• Generics — forall type parameters
• Quantifiers — forall/exists in contracts
• Effect operations — custom effect handlers

What Tier 2 would add

• Inductive proofs for recursive functions (using decreases clauses)
• Match arm translation to Z3 (case analysis)
• Generic instantiation at verification time
• Bounded quantifier support

Roadmap

Incremental across C6-C8. The Tier 3 fallback with runtime checks is the correct architecture for now — this issue tracks expanding what can be statically verified.