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

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.