seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS

[blahbleh]

If your proofs are instead in tests then it's much easier to modify them, because radical changes aren't required, and the "mathematical proof" is that all branches have been hit.

"all branches have been hit" is nothing mathematical. It means neither fast, nor secure, nor good, nor correct.

[ayumu]

will it save you from browser vulnerability? will you formally verify your browser?

Browsers lean hard on sandboxing for security purposes.

Sandboxes implemented with seL4 have formal guarantees; capabilities are enforced.

Sandboxes implemented on Linux are a joke.