@rzeta0 @sel4

The functional correctness proof is what you described, that the actual implementation behaves as specified.

Now, the specification has certain properties (that can be mathematically proven). For example, that memory can’t be accessed or processes can‘t communicate without authorization.

One of the topics still being worked on is protection against covert channels (like Spectre).

I recommend reading https://sel4.systems/Info/more-research.html