I will say this. The seL4 developers made the strong claim. Evidence that it is not as strong as people who heard about it thought is not a strong claim. It is

I will say this. The seL4 developers made the strong claim. Evidence that it is not as strong as people who heard about it thought is not a strong claim. It is just being realistic. The seL4 developers themselves say that the properties they list are things that come out of the proof and your approach of looking for properties that they promise is a backward way of going about things, since they did not claim to exhaustively list all properties. If you want to understand things to your satisfaction, read the proof and figure it out yourself. I have already understood things to my satisfaction and the double digit number of upvotes that I have received suggests to me that my explanation was to others’ satisfactions as well. You likely have many days or weeks or work ahead of you to answer a passing curiosity of yours whose precise answer is not going to change anything for anyone. Have fun.