SeL4 is a formally verified operating system

I saw this mentioned in the article "Prediction: AI will make formal verification go mainstream"[1] and thought it is worth its own post.

Does anyone have any experience with SeL4 that they would like to share?

[1] https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...