> Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.

Is it possible that the spec could be factorised into something higher-level and more modular? If not, can you give a flavour of the type of unavoidable esoteric detail? (One area I can see lots of complications is when dealing with versioned data, especially in multiple interacting systems -- naively, correctness needs to be proven for every combination of versions, even if some are never seen.)