"Vulnerable to traffic analysis, I'm sure certain organizations wouldn't mind seeing that vulnerability include cleartext."

Well, certainly. Depends on what this guy's role is supposed to be in the organization. One can always relegate the riskier people to stuff that can't harm them much. In any case, NSA can already do what you mentioned given leaks mention active targeting. Catalog includes regular malware, 0-days on stuff, and implants. Tor is the LTD they aim at themselves with optional LGB's following from QUANTUM and such. So, it would be a matter of already-vulnerable people or services getting more so.

"I've never seen an Underhanded Ada Contest, but I'm pretty confident that a bad actor could still introduce vulnerabilities that would pass a reasonable code review and be deniable"

Well, sure. Just remember, though, that what you're saying already applies to the Tor project. Any of the contributors, maintainers, relay hosts, and so on might be malicious. That's why A1 class called for protection throughout whole lifecycle which my framework below expanded on. SAP security guides showed most areas requiring protection. Examples below:

http://pastebin.com/y3PufJ0V

http://www.dss.mil/documents/odaa/nispom2006-5220.pdf

Now, from here, we have to ask what can be done to mitigate potential exploits. Well, we know the protocol itself is subject to strong, peer review by parties more than willing to publish problems and organization that corrects them. The main problems occur in crypto libraries, protocol engines, interfaces, type checks, memory errors, parsing, handling time, and error handling. A type-safe, memory-safe, low-level language along lines of Ada/SPARK, Go, Rust, or Modula-3 plus specific libraries and guidance on aforementioned can knock out vast majority of the risk. Well, that along with parser/protocol generators already available in academia with hand-checked code and design-by-contract to encode constraints. OpenBSD people probably do considerably more work on their code than what would be necessary to take care of this in safer language while focusing on areas most likely to be hit.

So, I think we can get plenty mileage without full, formal verification. There will be flaws just as there are in protocol itself. Yet, it will work most of the time with people finding problems so long as plenty are on it motivated to do so.

" I think a good half measure would be: fully spec'd pure functions don't need human code review - just feed patches to the theorem prover and regression tester, all the trusted human labor can then focus on things that touch global state."

They still need review. You have to specify what you're going to do, what security properties it maintains, how it maintains that, and the implementation correspondence. Usually also show compiler didn't screw it up. That's tricky. Pure functions are fine but covert channel analysis means it's going to be an imperative language for final implementation. Old model was basically decomposing functional components into state machines representing every permissible state. Can check by eye that they either should work securely or fail-safe. Still keeping my eye out for CompSci tech that can derive imperative from simple, functional languages in human-readable form.

"Thought getting people to trade C performance was tough? Try getting them to intentionally delay all comparison operations... in the entire software stack :)"

Oh my god, I've been there. Mainstream INFOSEC totally ignored that problem saying it was unnecessary until recently rediscovering it under "side channel" label. Running wild with it. I called out Freenet on Schneier's blog as probably having plenty due to use of Java. Meanwhile, old methods of handling timing channels were reducing precision, fixed-rate, maximum-time, turning off caches (extra painful on Core i7), masking, and my favorite being asynchronous, randomized execution. I was going to put the latter in a CPU then found someone else already did that. Clever. Partitioned caches are another popular strategy. I just stick with Red/Black model in my designs with trusted part being dedicated chip with timing mitigation for just needed part. Still performance hit no matter what.

Anyway, I did a write-up for someone on how to secure a service like Tor here:

https://www.schneier.com/blog/archives/2014/09/identifying_d...