I've run into (multiple) compiler bugs in certified C and C++ compilers, I know how difficult this is. But still a much larger percentage of bugs I've seen was

I've run into (multiple) compiler bugs in certified C and C++ compilers, I know how difficult this is. But still a much larger percentage of bugs I've seen was introduced by the developers. Which is why I said even now Rust would probably beat MISRA C++ in terms of total amount of bugs. I do think Sealed Rust has a bit of a way to go, but it would be a worthy investment. Seen from the point of total risk, the compiler errors are much harder to find, but the developer errors can still kill you. In any case SPARK is indeed even farther ahead in terms of having a reliable toolchain paired with a language that makes safe code easier to produce.