Alleged "microkernel mathematically proven to be bug free"

[guninski@guninski.com (Georgi Guninski)]

>These proofs tie a meta-specification to the actual code. Look into the
>sort of proofs they use. Basically they're saying "the code does what we
>said it has to. Only if we accidentally told it to go skynet on us, it will
>work perfectly". Things like segfaults would be pretty clearly not as
>specified.

By browsing the proofs, I have the impression
they don't depend on the C code (and Isabelle
parsing C appears not very trivial, though 
possible).

If I backdoor the C code of the kernel, will
the proof fail?