Doesn’t NASA have an incredibly strict, specific set of standards for writing safety critical C that helps with writing programs that can be formalized?
C and C++ always defaults to minimum amount of safety for maximum allowance of the compiler interpretation. The priority of the language designers of them is keeping existing terrible code running as long as possible first, letting compilers interpret the source code as freely as possible second.
That's why many military and aerospace code actually uses much safer and significantly more formally verifiable Ada.
If you assume the entire lang, yes. If you use a large subset, no. Furthermore, compiler interpretation might actually be sane! There are more compilers out there than GCC, Clang or MSVC. I suspect many assumptions are being made on this claim.
But a memory-safe program != memory safe language. Memory safe language helps you maintain memory-safety by reducing the chances to cause memory unsafety.