Comment by adyavanapalli
5 days ago
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.
We literally can do this already. It's been done. seL4
Worth taking a closer look at what they actually were able to formally verify. No doubt a massive achievement, however after seeing several demos poke holes through it I don’t think they’ve done the level of “formal verification“ that you may be inclined to think they have.