You can only _add_ jitter. So presumably you make people think you're farther away than you really are. I guess if you're especially clever, you can manufacture responses to packets you haven't sent yet to throw people off.
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.
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.
> Claude can write a proof showing that a compiled program’s behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can’t tell you whether your spec matches reality.
reply