seL4 is a bit more than a hypervisor, but it's definitely very low-level. In terms of a useful seL4-based system, you may want to look at https://trustworthy.systems/projects/LionsOS/ – not yet verified, but will be.
Simpler versions of such devices exist, eg HENSOLDT Cyber markets a secure VPN gateway that is built on seL4. Over the years we've been in on-and-off discussions with vendors of networking equipment, it's always a battle between those in the company who take security seriously and those resisting any rocking of the boat. Having said that, we're presently in such a discussion again and it's looking promising so far.
However, it's entirely possible that someone has already done it and is not talking about it...
In terms of security, the answer is a clear yes. Xen is kernel of 100+kSLOC of unverified code, while seL4 is verified. On top of that, Xen has Dom0 and thus a complete Linux system in its TCB.
What Xen has over seL4 is the management/admin framework.
But there is a project to port Qubes to seL4, waiting for the funding to be cleared.
Re scalability of verification: you don't have to verify everything to get a massive security/safety boost. A well-structured system has a small trusted computing base (TCB), and if you get that right, your system can be pretty secure even if parts of the TCB remain unverified. Eg drivers and network stacks are outside the TCB if you encrypt all data, they can only threaten availability. This was just demonstrated pretty well with AMNESIA:33: for an seL4-based OS, it's just a minor issue, not a critical vulnerability: https://hensoldt-cyber.com/2020/12/08/how-amnesia33-does-aff.... This confirms my analysis from a few years ago, looking at critical exploits in Linux and how seriously they'd be in an seL4-based OS (hint: mostly not at all): https://ts.data61.csiro.au/publications/csiro_full_text//Big...
Thanks for featuring my white paper. Some responses to some of the comments.
"Opinionated": guilty as charged. However, I claim that the opinions are well-grounded in fact.
Deployments: There are seL4-based devices in regular use in several defence forces. And it's being built in to various products, including civilian, eg critical infrastructure protection. And much we only hear anecdotally – that's open source...