Statement provable for all parameters, but unprovable when quantified

Great question! Yes, there are specific examples. One of the most famous is Goodstein's theorem. If $A(n)$ is the statement that Goodstein's sequence starting at $n$ terminates, then it is known (via stronger theories than PA, namely use of a clever ordinal argument) that $\forall n \; A(n)$ is true.

Moreover, for a specific $n$, given that $A(n)$ is true, it must be provable: just write out the finite sequence, and that gives a proof that it terminates. (Once you get to $n = 4$ or larger, it will be a very very long proof -- one that we humans cannot actually have the space or memory to write down.)

However, $\forall n \; A(n)$ is known to be unprovable in PA.

Possibly the easiest example is to let $A(x)$ say that $x$ is not the Gödel number of a proof of $0=1$ from the axioms of PA.

Because there is no such proof, $A(0)$ is true, $A(1)$ is true, etc., and because of their syntactic form each of these is provable in PA.

However, $(\forall x)A(x)$ is the statement $\text{Con}(\text{PA})$ which the second incompleteness theorem shows is not provable in PA.

There are other examples, as well. Some are related to the Paris-Harrington theorem and other independence results; others are related more directly to the incompleteness theorems.

Let $\phi(x)$ be the formula expressing "x is not a code for a proof of '0 = 1' from the axioms of $\textsf{PA}$".

Since $\textsf{PA}$ does not prove that there is no proof of '0 = 1' (that is, $\textsf{PA}$ does not prove that $\textsf{PA}$ is consistent), then it is not the case that $\textsf{PA}$ proves that there is no code for such a proof. But since if there were such a proof, its code could not be standard (otherwise, it'd be a code for an actual proof, which would imply that $\textsf{PA}$ actually proves that it is inconsistent), then we know $\phi(0), \phi(1)$, etc all hold.