>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?
