Hi Horace, 1) Is there a mechanism for inter VM communication with seL4 as a hypervisor? There is a vchan (virtual channel) mechanism that, in our example VMM, is used to communicate between the VM and other components. If you had configured two VMMs to have two VMs then if you connected both of them to vchan then the VMs would be able to talk to each other. 2) If the VMMs run in kernel mode (PL1), as I was told, does it mean they use hvc commands instead of swi/svc commands when sending messages to seL4 as hypervisor? All native seL4 threads (including the VMM) run in user mode and perform swi/svc operations which then trap and get delivered to seL4 in hypervisor mode. Threads such as a VM need to have a VCPU to run in modes other than user. Adrian