It's interesting (and no coincidence?) that the one caveat with the OK Labs (now...

jdub · on July 26, 2016

Nitpick: It was NICTA's (now Data61 at CSIRO) seL4 that was verified, not OK Labs' OKL4. The seL4 copyright is owned by General Dynamics.

femto · on July 26, 2016

Thanks for the correction. I'm curious: what was the exact relationship between NICTA (now Data61) and OK Labs? I thought the verified kernel work was spun off into OK Labs, but that's not the case?

Answering my own question, based on a bit of web surfing: OK Labs was spun out in 2007. The formal proof was completed by NICTA in 2009. This verification work continues today, within Data61.

http://ssrg.nicta.com.au/projects/TS/

happypanther · on July 27, 2016

lets see how much I get right here,

NICTA was the australian government side, OK Labs was private company that spun out of it.

Some early versions of OKL4 were opensource and based on code from NICTA(&others) but there was an internal rewrite that was OK Labs proprietary-only

seL4 is yet another entirely separate codebase, written by NICTA, but where the copyright was given to OK Labs by NICTA.

jdub · on July 27, 2016

The copyright of seL4 was not given (or licensed) to OK Labs AFAIK. It's currently owned by General Dynamics, and OK Labs no longer exists.

monocasa · on July 27, 2016

> Does ARM have a supervisor mode, along the lines of the Intel Management Engine, which would leave a chink in the provably correct operation?

Sort of if you count TrustZone?

sliverstorm · on July 26, 2016

with the new caveat that the EDA tools correctly implement the verilog source?

There are tools for verifying that, too. LEC & LVS