> is that only for some problems is the specification simpler than the code.

Regardless of the proof size, isn't the win that the implementation is proven to be sound, at least at the protocol level, if not the implementation level depending on the automatic theorem prover?