Yes, I do. I know they are very different from real correctness verifiers, but it's not like the people only using the compiler has no way of preventing trivial UB bugs. UB also is really only a language concept and nobody is writing code for the abstract C machine.