Hacker News new | ask | show | jobs
by regehr 4371 days ago
Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.