The operational semantics for a SafeIO language should always accurately model its memory state. The application should not compute (take a step in the semantics) in a way that exposes corrupt memory or arbitrary undefined behavior. Nor should it violate the memory model.
Moving immediately to the "Terminated" state is fine, whether it be due to out-of-memory, kill -SEGV, cosmic rays, or hardware failure. An FFI call that corrupts memory is bad (may result in arbitrary behavior, not just termination) as is ptrace'ing.
Naturally, all Unsafe code is part of the TCB, as is the OS and GHC, and low-level data structure libs and bindings. It's a big TCB. Still, it's something to be able to write an app that doesn't automatically get added to this TCB just by virtue of being an app (main::IO).