That would help with things like the memory safety of the daemons you run, but that hasn't been the problem when Tor has failed its users.
Tor has failed its users because the idea of running a public Tor cloud with volunteer entry, onion, and exit nodes is ludicrous. It means that the entire network is under surveillance all the time, the exact opposite of what you want. There has been widespread confirmation that the data you transfer via the public Tor cloud is being passively surveilled at the endpoints and actively modified when you, for example, download software. This makes it incredibly dangerous to use, likely more dangerous than just using the regular internet.
There are many other problems (like the fact that .onion sites are a dirty hack and likely have many undiscovered weaknesses like the ones CMU found) but nearly all of them are either deployment or architectural issues, not code security issues.
Yes, I agree. When I wrote the parent comment I was thinking more about implementation detail correctness: memory safety, protocol implementation correctness, etc.
Like you said, Tor has architectural issues. Tor would be fine if it were low-profile, but it's not, and that's a major part of why the architecture is breaking down - it doesn't scale well with increasing users/publicity/nation-state-interest.
I think most proof-verifiable languages are too limited to prove many types of security correctness valuable to tor users.
For example, side channel attacks. A classic attack on computerized cryptography. I don't know of any proof language that can protect against side channel attacks.
If you look online there are a few lists of tor attacks. The attacks include: snooping on exit relays, application issues, traffic correlation, website fingerprinting, congestion attacks, blocking tor access (declining to extend). Most of these are issues in the design of the tor system, not something I think source code proof systems are capable of preventing.
what property would you prove, though? you could create a memory safe program that does not provide anonymity. how do you represent "anonymity" in the proof system?
That would be pretty cool, since anyone could prove source correctness automatically.