In formal verification, "the specification" means the encoded claims that will be proved, i.e., the lemmas and theorems to which the proofs directly correspond. When we use proof assistant languages (e.g., Rocq, Lean) to accomplish the verification, this means the specification is given as a type.
I think this is not what the parent comment had meant by "specification"; it seemed to me that they meant that word to refer to the human-accessible document that states what the program ought to do.
The translation of an informal (human-readable) specification into a formal specification is not always straightforward, often due to issues on either (or both) end(s) of the process. You can write Rocq code that type-checks and thus "is verified" in the sense that the type-checked code conforms to the formal specification, but if the claims you proved are not what you had intended to claim, then that verification is not very helpful.
So that is where the parent comment introduces "validation" to mean (in my words) the process of ensuring that your formal specification matches the informal specification, such that any formal verification that occurs is useful and meaningful.