On: Verifying ARM processors against the official ARM ...

[femto]

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 → femto]

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 → happypanther]

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.