Hi, Robigalia lead dev and seL4 proof engineer here.
about seL4 proofs
The proof is not wishful thinking. There are ways of satisfying or validating each of the assumptions:
assembly: the proofs are being updated to include this
hardware: some verified hardware exists, but this is always an assumption in high-assurance applications, so no sleep lost there
hw management: some of this (eg TLB behavior) is being added, but this is indeed a source of bugs in seL4 for some SoCs. Fortunately it's relatively small and people review it
boot code: this was part of the proof once, and is being added back again.
virtual memory: this is pretty bulletproof, but the complications it mentions do apply.
DMA: a problem in any high-assurance application. IOMMU solves this.
timing channels: this will be mitigated in the near-future with temporal partitioning.
What is the goal of the proof, anyway? The proof provides evidence of correctness, to a high degree of assurance. This is not an absolute thing, as you mention, the proof has some assumptions that need to be validated before you can apply its conclusions. But seL4 is the most extensively validated kernel, formally or otherwise, and important investments by government and military groups show that they want the sort of assurance seL4 provides.
So, Robigalia is about creating a persistent capability-based operating system. By "secure POSIX-compatible userland", I mean that it is confined and can't violate integrity or confidentiality of the rest of the system. This is accomplished quite easily using the guarantees provided by seL4 about confinement and information flow security. Of course, POSIX itself isn't terribly trustworthy, so anything running inside a POSIX "container" is somewhat suspect. But things inside the "container" won't be able to break out of it.
Safety in the Rust sense has nothing to do with the security of Robigalia, really. It does help with ease of implementation, but the security comes from the inherent properties of pure capability systems. It's baked into the architecture.
why redox shouldn't port seL4
rewriting it in anything but C is stupid. the proofs won't apply and the C is already fine.
why redox shouldn't use seL4
it's much more interesting to have a pure-Rust kernel, and gives you more design flexibility