Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built for your car, delivering you bug-free driving and unparalleled safety behind the wheel."

Seems like a dumb approach that only marketing would come up with.

The challenge is SDC is AI, not correctness of the kernel that the AI stack runs on. Is an SDC based on a formally verified OS but using logistic regression safe?

A verifiably correct kernel is a necessary, but not sufficient condition for a self-driving vehicle to be trustworthy.

It's at least safe from someone hacking into it and intentionally (or accidentally) causing harm.