Do you think anything could be done to mitigate or fix that? I've only recently started digging into seL4 so I don't know if this is an unavoidable problem (in

Do you think anything could be done to mitigate or fix that? I've only recently started digging into seL4 so I don't know if this is an unavoidable problem (in terms of proving correctness) or if it even needs to be solved in-kernel.