Who says a kernel must have 15 million lines of code? I'm pretty sure there are kernels out there that have been verified correct. Of course the hardware could still be broken (can also be proven correct) or a cosmic ray could flip some bits...