Problem is, some undefined behaviors are actually correct. Some are documented extensions (a concept straight out of ISO C), and some are just nonportable situations that empirically work.

These could be handled in the prover; you just need an extended language definition. Or maybe not. Depending on what is being relied upon, it could be difficult.

In any case, a prover based on equating "correct" with "strictly conforming ISO C" is going to be of severely limited use. It might be good for some module-level assurance, like that some linked list or hash table module is perfect or whatever.