Not sure what you mean by "well-served"? In terms of design, I've seen attempts at proofs discover attacks that likely would not have been otherwise found durin

Not sure what you mean by "well-served"? In terms of design, I've seen attempts at proofs discover attacks that likely would not have been otherwise found during development. In that case the proof served the designers in building a more secure protocol. Some of the early kerberos work could have benefited from making the designers prove or at very least justify their claims (say the use of xor fan-folding as a one-way function). Does a proof increase your confidence in an algorithm? As someone that worked on MD6's proof of differential resistance it certainly increased my confidence in the protocols ability to resist certain types of attack. By ad-hoc do you mean people selecting algorithms without a contest? If so I would counter with the following incomplete list of broken ad-hoc standards: DTD-1, FEAL, WEP, A5/1, A5/2, KASUMI, GOST 28147-89, Cryptomeria cipher, CCS, SHA-0. The crypto that has held up, has generally held up and most of the other ones that haven't we don't use, so we may be biased toward remembering good ad-hoc crypto and forgetting the bad.