Comment by adyavanapalli

Two days ago, Anthropic published an article about formally verifying software and producing something like 180 million lines of Rocq in just a couple of weeks. I think build and formally verifying an entire OS kernel might be within its reach in a couple of months.