What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. They can be reintroduced into seL4 too. Jus

What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. They can be reintroduced into seL4 too. Just have an amendment to the specification adding a new feature say the bug is okay without anyone realizing it does. Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way. The proof itself proved something other than what was advertised, which allowed for this issue to exist. If you look at the bug tracker, it appears that this has happened more than one time. While seL4 is an amazing achievement, it is clear that it is not the bulletproof software that people thought it was. There is no proof that the specification is problem free after all. Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. This is a gross misrepresentation of what I said. Having an objective evidence based opinion that seL4 is not as good as advertised has nothing to do with people dying. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land. seL4 does not achieve this. It is the equivalent of less than 0.001% of all of the code run on machines. It makes no guarantees that the >99.999% that people use is okay.