(sarcasm on)

Woohoo, we're almost all of the way there! Now all you need to do is ensure that the formal specification you are proving that the software implements is a complete and accurate description of the requirements (which are likely incomplete and contradictory) as they exist in the minds of the set of stakeholders affected by your software.

(sarcasm off).

I mean, I don't disagree. Specs are usually horrible, way off the mark, outdated, and written by folks who don't understand how the rest of the vertical works. But, that's a problem for another day :)