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.