Dismantling the seL4 team is the result of two things: simple lack of vision from CSIRO leadership (who seem to think that cybersecurity and formal verification don't have much overlap), and the long-standing one-upmanship and antagonism between the fields of AI and formal methods.
> Is seL4 proved secure?
> This depends on what you mean by secure. [answer continues...]
The leadership team would need to be truly inspired to take that sort of thing seriously. It sounds like madness.
[0] https://docs.sel4.systems/projects/sel4/frequently-asked-que...
"In the interpretation of classic operating system security, the answer is yes. In particular, seL4 has been proved to enforce specific security properties, namely integrity and confidentiality, under certain assumptions."
The SeL4 FAQ has this gem
As others also point out, security is conditional on various things, including, in this case, what you consider a valid flow of information and what you don't. For example if an OS allows user-mode to read AES-encrypted kernel-mode data then that would be insecure if you had an unrestricted attacker (who can brute-force AES) but secure assuming polynomial attackers (under standard hardness assumptions for AES). To add insult to injury, we don't in fact know if the standard hardness assumptions actually hold for AES.