Seems like there are certain fundamental limits to what can be done here though. Much of the advantage to using these models is being able to come up with a vague/informal spec and most of the time have it get what you mean and come up with something serviceable with very little effort. If the spec you have in mind to begin with is fuzzy and informal, what do you use to perform verification?

After all, whether a result is correct or not depends on whether it matches the user's desire, so verification criteria must come from that source too.

Sure there are certain types of relatively objective correctness that most of the time will line up with a user's desires, but this kind of verification can never be complete afaict.