[wmf]

What if the code doesn't rely on undefined behavior?

[regehr]

Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.