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.