On Jul 29, 2014 6:14 PM, "Georgi Guninski" <[1]guninski@guninski.com>
   wrote:
   >
   > >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?

   Isn't that the whole idea? It would really change the thing up if
   there's a backdoor!

References

   1. mailto:guninski@guninski.com