I've been beating the drum about this to everyone who will listen lately, but I'll beat it here too! Why don't we use seL4 for everything? People are talking about moving to a smart grid, having IoT devices everywhere, putting chips inside of peoples' brains (!!!), cars connect to the internet, etc.
Anyway, it's insane that we have a mathematically-proven secure kernel, we should use it! Surely there's a startup in this somewhere..
Almost all vulnerabilities are in apps and libraries which seL4 does little or nothing to solve. The only solution is secure coding across the entire stack which will reveal that much of the existing code is so low-quality that it just has to be thrown away and rewritten.
Anyway, it's insane that we have a mathematically-proven secure kernel, we should use it! Surely there's a startup in this somewhere..