> It's a particularly bad one though because it always leads to UB, which means you can't say anything about what happens next.

This is also why memory safety is table-stakes when it comes to formal verification of the underlying program logic. You can't solve logic bugs (even where that's known to be feasible, such as for tightly self-contained, library-like features) without solving memory safety first.