There are some languages that can be formally verified, and have themselves been formally verified.

Formal verification is a complete pain in the ass to do and there's a reason it's mostly done only in the most critical of systems, but if a program passes 100% formal validation, you're as close to crash free as you can possibly be.

I believe Ada and some other lesser used language sport well supported formal verification methods. You won't be able to use C/C++/Java/Rust it you're going for 100% formal verification though. There are attempts to bring the concepts to more commonly used languages (Frama-C, for example) but in my experience they're stuck in PhD-ware hell, great for writing papers but terrible for writing actual software.

Frama-C is used in production to meet normative requirements for critical software at least at Airbus (DO-178C), THALES (CC EAL6/7), EDF (ISO 60880). I think that they use actual software in production.

For example C/C++, with the help of something like: https://www.absint.com/astree/index.htm

But there are actually other languages that are better suited to such methods: More or less everything from the functional space is quite well applicable to those.

Any language that enforces memory safety is unlikely to crash because of a segmentation fault.

They will instead crash because of an uncaught exception or a panic handler - end result is the same.

By removing segmentation fault crash you have removed a large portion of unwanted crashes, the end result is very different.

But the crashes doesn't get removed, they get transformed into error types or exceptions and you still crash when you don't handle them.

This is only true if the language does not employ static analysis.