AI is getting good enough to help with the verification process and having a hardened kernel would guard a bit better than the current strategy of using containers everywhere.
There's Genode[0]. Relative to the hurd, its design is much more advanced and it supports a range of modern microkernels including seL4.
Many stories around using Genode in the Genodians[1] blog.
https://www.gnu.org/software/hurd/history/port_to_another_mi...
Neal Walfield was working on a new microkernel as well: https://www.gnu.org/software/hurd/microkernel/viengoos.html
It definitely would not be a trivial amount of work.
Honestly, I think the downvotes were for mentioning AI may have a role in validation. LLMs are increasingly being explored in the theorem prover space, but it's still controversial to talk of them approvingly on some HN threads.
It's an interesting idea to think that LLMs could be used to not only explain the code but test the potentially tricky corner cases.
I'm pretty sure LLMs are here to stay, and we're just going to have to learn the best ways to work with them.