By corollary does that mean that if there isn't a formal proof of how C compiles to assembly, and how those opcodes are interpreted by a particular CPU model, that C formally isn't specified to have any meaning to a CPU?
For what it's worth, this is a common sentiment people have when they first come to blows with formal. "If you can't verify everything, why verify anything?" is a reasonable question to ask but it's not a practical position to hold since formal does increase the quality of software/hardware. Don't argue for less formal, fight for more!
The point is “undefined behavior” is more about gaps in the standard than bugs in programs.
And not least of all, we've learned more about programming language development than when C was created.