----------------------------------- btiffin Tue Jun 24, 2014 4:39 pm Read about this on news.ycombinator.com ----------------------------------- seL4, supposedly a proven bug-free microkernel. About to go open. http://sel4.systems/About/ (The home page had 34 days left on the countdown to release timer when I looked) Completely unique about seL4 is its unprecedented degree of assurance, achieved through formal verification. Specifically, the ARM version of seL4 is the first (and still only) general-purpose OS kernel with a full functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. In short, the implementation is proved to be bug-free. This implies a number of other properties, such as freedom from buffer overflows, null pointer exceptions, use-after-free, etc. I'm old now, but I find this hard to believe, also lazy enough to have not read the formal theory or proof papers. Cheers