Given that hypervisors are essentially 4th generation microkernels plus some hardware emulation slow-path code to handle the cases where the OS kernel isn't paravirtualized to use upcalls, it would be interesting to see RISC-V boards that shipped that boot directly to seL4 from ROM as their firmware. All OS kernels for the platform would be paravirtualized.

L4 provides a pretty minimal and stable interface as a paravirtualization target. If a software ecosystem arose where a hypervisor was always present, you could get away with never implementing all of that attack surface/potentially buggy code in the hardware emulation portions of the hypervisor. The Alpha AXP showed that this sort of arrangement can be very high performance. Hopefully the RISC-V virtualization extensions would provide features (like shadow registers / separate register bank) for very light-weight transitions into and out of hypervisor mode.

In a sense, the Alpha AXP's firmware (PALCode) was a minimalist hypervisor that only supported a single guest OS. The PALCode always handled the lowest-level details, such as lowest-level interrupt handling, exception handling, and TLB / cache management. All OS kernels for Alphas (VMS, Windows NT, Tru64, Linux, etc.) were in a sense paravirtualized for the PALCode, although there were different versions of the PALCode for running VMS and Tru64 / other POSIX-y kernels. My guess is that Windows NT for Alpha AXP ran on the VMS PALCode, given Dave Cutler's role in both the NT and VMS kernels.

RISC-V booting directly to seL4 would look something like UNSW's L4/Alpha project. L4/Aplha was a port of L4 at least partially ran as Alpha AXP PALCode, replacing the normal firmware. Of course, you couldn't run VMS, Tru64, etc. on top of L4/Alpha, but L4Linux is a port of Linux to run on top of L4.