[microkerneldude]

Re scalability of verification: you don't have to verify everything to get a massive security/safety boost. A well-structured system has a small trusted computing base (TCB), and if you get that right, your system can be pretty secure even if parts of the TCB remain unverified. Eg drivers and network stacks are outside the TCB if you encrypt all data, they can only threaten availability. This was just demonstrated pretty well with AMNESIA:33: for an seL4-based OS, it's just a minor issue, not a critical vulnerability: https://hensoldt-cyber.com/2020/12/08/how-amnesia33-does-aff.... This confirms my analysis from a few years ago, looking at critical exploits in Linux and how seriously they'd be in an seL4-based OS (hint: mostly not at all): https://ts.data61.csiro.au/publications/csiro_full_text//Big...