[naasking]

> 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.

[dchftcs]

I don't dispute that verification can be a good tool, but many teams exhaust their time budget at the point of figuring out what to verify, making it less necessary to verify certain things (sandboxing, airgapping, lawyering), writing simple test code, refactoring and carefully rewriting some of the prior test code, designing and realising software architecture that's more testable, etc. A certain portion of that work can use some formal verification, but it's down beneath a long list of things that not many teams manage to get through, whether or not for good reason.