Hi,
Regarding OKL4: http://www.ok-labs.com/products/
1. Is OKL4 is a commercial implementation of L4?
2. Is OKL4 based on the L4.Pistachio code base and still open-source but with a separate source tree?
3. The OKL4 roadmap http://www.ok-labs.com/products/product_roadmap mentions "High-security API" and "Formal correctness proof".
Does this mean that L4.Sec may or is already getting implemented in OKL4?
Thanks Shams