Provably correct microkernel (seL4)

[coley at linus.mitre.org (Steven M. Christey)]

I wonder what would happen if somebody offered $10000 to the first applied
researcher to find a fault or security error.  According to
http://ertos.nicta.com.au/research/l4.verified/proof.pml, buffer
overflows, memory leaks, and other issues are not present.  Maybe people
would give up if they don't gain some quick results, but it seems like
you'd want to sanity-check the claims using alternate techniques.

- Steve