empirically untrue. several projects exist that bolt on extra safety to unsafe languages or unsafe parts of language. SeL4 for C, MIRI for rust unsafe. i guess ada/spark for ada too, is the OG, spark being added to ada 4 years after its first release

Hardening is definitely possible, we've had sanitizers in C/C++ for a long time. It's not full memory safety though. Miri is the same.

SeL4C is formal verification, and while it can prove memory safety (and much more) it is much more difficult, to the point that you're basically programming in a different language.

Ada/SPARK is your best example, and also the example I know the least of, so I won't comment on.