[antientropic]

The vast majority of C programmers do not use a formally verified C compiler, and most of them wouldn't care about that anyway.

From a security perspective, demanding a formally verified C compiler is rearranging the deck chairs on the Titanic. Switching to a safer language like Rust will do much more to improve security, even if the compiler is not verified.