l4 – keeping simple

A claimed validated operating system.

September 16, 2014 vy operating systems, systems

The claim: we have demonstrated the comprehensive formal verification of the seL4 microkernel, with a complete proof chain from precise, formal statements of high-level security