L4 implementations

[Shams]

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