I'm aware of that post! I did a video looking at the GNU Hurd and I believe it came up there.

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.

I've worked a fair amount with LLMs from a code generation perspective, and to be honest, I find them often to be better at reading and explaining code to a human than generating good code.

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.