One thing that seL4 requires is an mmu in order to support the isolation claims. The intel me type cpu would need to have some of these features that micorcontrollers don't usually have.
That's not necessarily true. There are VMM or hypervisor projects that utilize seL4 for x86 and ARM [1][2][3]. In this situation there isn't really one that is in "control". You could also have other threads or components that have higher privileges that can maybe do other monitoring or control activities.
It does say this: The hypervisor extension has been designed to be efficiently emulable on platforms that donot implement the extension, by running the hypervisor in S-mode and trapping into M-modefor hypervisor CSR accesses and to maintain shadow page tables. The majority of CSR accessesfor type-2 hypervisors are valid S-mode accesses so need not be trapped. Hypervisors can supportnested virtualization analogously.
Is the ports system similar to Gentoo's portage/ebuild system? I can get sources, configure the build, or get binaries (for some things) pretty easy through it.
I think one of the big things here is that the refinement proofs from the models for isolation, IPC fast path, capability access control, and scheduling to C source to binary are strongest when the kernel is built with a particular configuration on particular hardware. When all of these are satisfied and you are on a trusted platform, you have very very strong guarantees that what is modeled is what you get. But it's not like this is hidden. They have make it pretty clear what the verified platforms and configurations are[1].
You should take a look at the verification chain though[1]. It is fairly extensive. It's not like they proved just a small part of a system in a general way.
