seL4 despite being formally verified contained gnarly bugs, like [1]. Thus, it's not a silver bullet as some people think. Yes, it improves the quality, but only one of the aspects of hardening software, like ASAN, SAST, fuzzing, strict languages, and so on.

[1] https://github.com/seL4/seL4/issues/1199

> Since it is the unverified SMP config of the kernel

I don't disagree with your point (formal verification does not rid you of all bugs), but this is not the subject of the linked issue. This was a bug in an unverified path.