It should be noted that KVM supports many different archs, and it lives inside the mainline Linux kernel while VMware's kernel modules are out-of-tree. I think this fact is an important difference (also that qemu-system-* are open-source, while vmware is not).

Why is a type 1 hypervisor instantly considered more secure though? I'd assume using Linux, instead of rolling your own code to interface with hardware, would make you more secure?

In the Linux vs Xen example, the TCB is much bigger with Linux. The idea is to keep the TCB as small as possible, with an emphasis on restricting the code size that's actually running privileged.

sel4's virtualization support make it a type 2 hypervisor. Akaros too, which IMO has the right model for virtualization with it's 'VM threads' concept. All 'type 2' really means is that the kernel directly supports running threads in ring 3 in addition to ring 0.

I guess it's your use of 'proper' that bugged me.