# Evolution 7 limitations

- decide() conformance is exhaustive over a modeled fault lattice, not over all inputs.
- The attenuation proof assumes one lemma (str.rstrip semantics) that z3 could not close; it is covered by bounded enumeration and an encoding differential.
- Trace properties are random testing, not proof.
- The E3 forecast gate and the E8 commit boundary are not modeled.
- Nothing here is deployed; it is a CI/offline gate.