I think it provides best bang for buck when the annotation is "obviously correct" but the implementation is complex. For example if you are trying to prove tha

I think it provides best bang for buck when the annotation is "obviously correct" but the implementation is complex. For example if you are trying to prove that your new sorting algorithm yields sorted list for all inputs. If there is as much annotations as there is code, then testing is better tool for the job than verification.