Do we need to switch to seL4 type verified kernels? There's no way we can secure millions lines of code, the attack surface is too big?