Comment by adyavanapalli
5 days ago
I don't understand why this is even a problem. If current models can formally verify vast amounts of software, couldn’t you use it to build a sandbox with formally verified guarantees against leaks?
5 days ago
I don't understand why this is even a problem. If current models can formally verify vast amounts of software, couldn’t you use it to build a sandbox with formally verified guarantees against leaks?
Do the agents build the IP networking stack from scratch? What about the operating system? What about the microprocessor? You can’t formally verify everything.
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.
seL4