I presume you are referring to Gödel's incompleteness theorem, which states that any sufficiently powerful mathematical logic will have theorems that can't ever

I presume you are referring to Gödel's incompleteness theorem, which states that any sufficiently powerful mathematical logic will have theorems that can't ever be proven in it. This doesn't mean that certain particular theorems can't be proven, however. For instance, proving that a particular implementation of a kernel matches a particular specification can keep well away from Gödel.