Formal results are scoped to the declared abstraction, configuration bounds, exact checkpoint hash, enabled properties, solver settings, and finite horizon. The initial focused family combines complete left-engine failure, partial aileron effectiveness loss, bounded crosswind, bounded actuator delay, and bounded sensor errors.
The existing one-step runtime check remains an online assurance mechanism; it is not described as multi-step closed-loop verification. Recovery-envelope results must keep unsafe, timeout, conservative-unknown, and outside-validity cells distinct.