> A formally verified program can still have bugs, because the spec (which requires specialized skills to read and understand) may not satisfy the intent of the requirements in some way.

That's not a bug, that's a misunderstanding, or at least an error of translation from natural language to formal language.

Edit:

I agree that one can categorize incorrect program behavior as a bug (apparently there's such a thing as "behavioral bug"), but to me it seems to be a misnomer.

I also agree that it's difficult to tell that to a customer when their expectations aren't met.

In some definitions (that I happen to agree with but because we wanted to save money by first not properly training testers and then getting rid of them is not present so much in public discourse) the purpose of testing (or better said quality control) is:

1) Verify requirements => this can be done with formal verifications

2) Validate fit for purpose => this is where we make sure that if the customer needs addition it does not matter if our software does very well substraction and it has a valid proof of doing that according with specs.

I know this second part is kinda lost in the transition from oh my god waterfall is bad to yeyy now we can fire all testers because the quality is the responsibility of the entire team.

>an error of translation from natural language to formal language

Really? Programming languages are all formal languages, which means all human-made errors in algorithms wouldn't be "bugs" anymore. Some projects even categorize typos as bugs, so that's a unusually strict definition of "bug" in my opinion.