You were clear, and you were wrong. The annotations are checked like I said, you cannot break the guarantees using them. If they're incorrect they won't pass verification. They just help the verifier.
Programmer intends to write code that does Y, but writes code that does X. Then they make the same mistake again and write an annotation that verifies the function does X.
Verification passes, but the code does the wrong thing.
If it is public API, it indeed can pass. This is similar to theorem provers - if you get your axioms or theorems wrong, you can incorrectly "prove" things. But verifiers are still useful because most of the code has larger internal surface than external surface.