Is there actually some way of formal verification of software that is driven mostly by machine learning? I imagine there's a small core of code that runs some trained models, but how are they being formally verified? How do we know there's not a blind spot in that model that turns out to be fatal under certain conditions?

The problem is that perfectly-working software can easily get you in an accident. "Well, the bus didn't yield, and the programming said it would"

It's not quite possible to write a car that avoids ALL accidents because a car has a speed and a turning radius and breaks only work so fast.

The problem with formal verification of systems like this is that checking whether software matches the specification or whether the specification is self-consistent is not the interesting problem. Whether specification matches the real world is the interesting problem and there is no formal way to verify that.

I think that the other part with insurance is that insurers have no idea what the risk involved actually is (since it's not been around long) so they aim way high to cover themselves.