> Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program.

Which semantics? The ISO C semantics is rather lacking; "undefined behavior" lurks around every corner.

A C compiler that correctly implements all ISO C requirements is a fine thing, and certainly better than one which gets some of that semantics wrong, but doesn't achieve all that much in the big picture.

If the verified compiler actually provides extended semantics beyond ISO C that eliminates much of the undefined behavior, such that programmers using this dialect can rely on a safer language, then we're talking.