No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certif

No, that's not true. The framing was always that it surpassed an incredibly high safety bar that no other kernel had surmounted, far beyond even security certifications needed for protecting national secrets. This is still true. A number of people who read that interpreted it to mean seL4 is flawless. Now that flaws have been found, those people have had to re-evaluate their views. Those who understood seL4’s guarantees correctly are an extreme minority. No it doesn't, people using formal methods understand perfectly well what confidence verification should bring and the caveats that are necessary. If by "industry", you mean Joe-know-nothing-about-verification-shmoe, then I'm not sure why his opinion was particularly important to begin with. >99.99% of the industry does not use formal methods, so those that understood the guarantees were weak enough to allow “impossible bugs” in the real world were an extreme minority. The rest of us had the view that I described. You can deride people who do not do formal verification, but I guarantee everything you use has unverified code written by people who do not do formal verification. If we restricted computers to formally verified code, we would not have working computers, embedded or otherwise.