Computer Science Canada :: View topic - Read about this on news.ycombinator.com

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.

Author:	btiffin [ Tue Jun 24, 2014 4:39 pm ]
Post subject:	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) Quote: 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