The biggest problem IMO with using C++ when I tried the browser is that it crash, it crash a lot and I would imagine they are segmentation fault.
I don't think I've ever seen a crash in either Serenity or Ladybird that I could attribute directly to memory management. For volunteer C++ projects, their memory management seems to have been done excellently. Using modern C++ features and things like error return types instead of null seems to be a key part in making the browser this good.
It's also worth mentioning that as far as I know Ladybird doesn't implement a JIT engine, using bytecode to execute Javascript instead. That should also make life significantly easier for memory management.
It's still a young browser and I'm sure there are some nasty memory corruption bugs lurking in the depths, but I haven't seen those yet.
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.
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.