That is very common for something given in the industry. It is our job as programmers to first figure out what the customer really wants, and then create enough of the requirements/spec to deliver it. That is one of the reasons for Agile vs Waterfall processes: nobody really knows what they want in the first place so you deliver something that you think is close and work with them to come up with something acceptable (acceptable covers both it does what they want, and also the cost to make it better). Any formal spec needs to be adjustable as we figure out requirements.

OTOH, we can probably call a much less formal spec good enough. Just that it doesn't write past the end of buffers would be very helpful. We can also throw a bounds in - if we can't prove it in X iterations then call it false (expect to adjust X to very large)

Not that vague first you need to know what the customer means by good. I was not making claims on the applicability of formal methods any way, only the point I was making about the primitives.