Re: Alleged "microkernel mathematically proven to be bug free"

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?