Maybe. I'm happy to run any formally verified C as my basement, for example the seL4 kernel, or for C to be used as an intermediate language. Especially as there should be less code at the bottom of the stack. But C++ seems worse, it's a far more complex language, designed and built to try and scale C to building applications. This creates a far larger attack surface.