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.