CONTROLLED COUNTEREXAMPLE · FM3

No key gets you out.

Inside an Eventbrite checkout dialog, both Tab directions wrap around—and the injected handler also swallows Escape. Focus has no keyboard exit.

EVENTBRITE/events/portland-pet-paloozaCONTROLLED GENUI
LTL OBLIGATION G(cycle ∧ probes_complete → Esc_exit ∨ Tab_exit ∨ ⇧Tab_exit) TRACE IN PROGRESS
BOMBADILalways(() => !(cycle.current && probesComplete.current) || escapeExits.current || tabExits.current || shiftTabExits.current)
complete keyboard-exit probe · same open dialog
Tab
Shift+Tab
Escape
SAME WEBSITE · SAME DIALOGs0 · Start on Register
Eventbrite ticket dialog used by the controlled FM3 keyboard-trap case
EXPECTED · Dialog closed

The screenshot is captured from the Eventbrite GenUI build. The original dialog has a working Escape exit; this presentation applies a controlled fault injection that suppresses it. Focus boxes show the resulting probe trace.