Speaking of Miri, is the long term goal to say for certain whether or not a program execution encountered UB? (Which is, of course, different than verifying it before execution at compile time.)
As I understand it, Miri would like to be certain about the presence/absence of the UB of any particular program execution, but there will probably always be some cases it can't catch.
That's more than a long term goal, that's the present behavior, to the extent that the UB rules are defined in the first place. Miri will tell you when it has to make approximating assumptions (e.g. accessing FFI or using nondeterministic operations), and it doesn't happen very often. This is very much the intent of the tool.