Hi I am new in seL4. It is really interesting OS. I would like to ask some questions even though the FAQ explains many things. 1. How different is seL4+VMM with OKL4 or codezero? If there is some performance gap between them, I am curious where the overheads are for? 2. I am wondering how well seL4 can support virtualization services. Can seL4 supports more than two linux simultaneously on the VMM layers? Moreover, can it execute different kind of guest OSes at the same time? What about RTOS? A RTOS can be executed with keeping their real time property on the seL4+VMM?? Lastly, I would like to know when new version of the VMM for A15 support will be released. 3. Did you use a code generator when you hit the steps for “Specification”, “Haskell Prototype” and “C code” In the Proof Processing? If you did it using any automatic tool, I am so curious how you verified and validated the codes. 4., According to the FAQ, current multicore support is through a multikernel configuration. Do you have any plan for one seL4 kernel to manage several processors? Thank you much in advance. Regards, Joe.