In this case limiting complexity would have worked: don't support frivolous amounts of image codecs (like the fax format here), just support 1-2, and make sure there is high assurance of the safety using known methods (security oriented code design, memory safe language, fuzzing, and sandboxing).
Things like image format decoders are easiest to produce formal analysis and proofs for. It's sadly still too expensive and slow to produce.
Fuzzing as a mandatory testing step could be useful in some cases.
I agree about bugs in specifications though :(