> A missing specification in the proof of lean-zip, a lean component, is a real problem to the philosophy and practice of software verification.

Every time someone makes this point, I feel obliged to point out that all alternatives to software verification have this exact same problem, AND many, many more.