Interestingly, important parts of the Linux kernel are proven correct (e.g. the scheduler). But yeah...not the whole thing.