Ah yes, the totally-valid use case of ensuring that a third party has properly compiled source code that you don't have access to. I'm sure this comes up in industry all the time.
Can you provide an example of a ZKP of memory safety of a compiled output that would be less computationally expensive than static analysis of the binary?