On Monday March 6th, a new project was announced which makes it possible to run rumprun unikernels on seL4. My hope is that the mirage-rumprun port of mirage can be made to target the seL4 root task used by rumprun seL4 demo apps. It may also be reasonable to extend Solo5 to target the provided seL4 root task.
From About seL4:
seL4 is a high-assurance, high-performance microkernel developed, maintained and formally verified by NICTA (now the Trustworthy Systems Group at Data61) and owned by General Dynamics C4 Systems. It is a member of the L4 family of microkernels, and is the world's most advanced, highest-assured operating-system microkernel.
seL4's implementation is formally (mathematically) proved correct (bug-free) against its specification, is proved to enforce strong security properties, and its operations have proved save upper bounds on their worst-case execution times.
All of this makes seL4 an ideal target for running unikernels.
Please contact me via this repo if you are interested building systems with mirage and seL4. Thanks!