Before discussing any of the technical issues associated with your question: Yes, in order to ensure that a statement (about numbers) is true (in the standard model), we currently do not have any procedure other than exhibiting a proof. (In fact, most mathematicians would argue that this is the only way to meaningfully discuss truth.) If the statement is unprovable in $\mathsf{PA}$, such a proof by necessity is in a stronger system, typically a fragment of set theory, $\mathsf{ZFC}$, sometimes a fragment of second order arithmetic, $\mathsf{Z}_2$. But sometimes we go beyond $\mathsf{ZFC}$. The typical extensions we consider usually assume large cardinals. There is a well justified body of evidence indicating that it makes sense to say that proofs of arithmetic statements in these systems are indeed true (I link to a small discussion on these matters near the end).
(Since proof is at the heart of this discussion, you may be interested is a series of essays by computer scientists, mathematicians, and philosophers, on The nature of mathematical proof that was published in the journal Philos. Trans. R. Soc. Lond. Ser. A Math. Phys. Eng. Sci, vol 363, No. 1835, Oct 15, 2005. Sadly, the only link I have is behind a paywall.)
There is a technical difference between the sentences produced by Gödel's techniques (or Rosser's) and sentences such as the strong Ramsey theorem that the Paris-Harrington theorem discusses. (For additional examples, see here and the references listed there.)
Gödel's statement is $\Pi^0_1$, that is, it has the form $\forall n\,\psi(n)$ where $\psi$ is a recursive statement (in the language of arithmetic, all its quantifiers are bounded). The strong Ramsey theorem is $\Pi^0_2$, that is, it has the form $\forall n\,\exists m\,\psi(n,m)$, where $\psi$ is recursive.
$\Pi^0_1$ are meaningful statements even by strict finitistic standards (see for example Richard Zach's dissertation and his discussion of Tait's analysis of Hilbert's program). They are true if they are unprovable (in fact, $\mathsf{PA}$ proves every sentence $\phi$ that is true of the natural numbers and such that $\lnot\phi$ is $\Pi^0_1$): If $\exists n\,\psi(n)$ is true, then for some number $m$, we can prove this statement simply by verifying $\psi(m)$ which, being a recursive statement, has a straightforward verification -- informally, we run a computer program that is guaranteed to halt, and check that the program outputs $\mathtt{Yes}$.
On the other hand, $\Pi^0_2$ statements cannot be called finitistic. If unprovable, this does not automatically ensure their validity (or falsehood). However, they admit a natural interpretation: They state that certain recursive function is total (if the sentence is $\forall n\,\exists m\,\psi(n,m)$, the function $f(n)=m$ assigns to each $n$ the least $m$ such that $\psi(n,m)$), that is, they state that certain computer program will halt, no matter its input. Typical independent $\Pi^0_2$ statements have the peculiarity that the corresponding recursive function is fast growing (see for example this discussion, or my article on Goodstein sequences). By a theorem of Wainer, there is a standard mathematical approach to verifying their unprovability, namely, one checks that the function $f$ under discussion eventually dominates the first $\varepsilon_0$ functions in a fast growing hierarchy.
One could consider Gödel statements and the like as first generation independence statements, and the more "combinatorial" $\Pi^0_2$ statements that followed as second generation. The mathematical arguments involved in either case are really very different. A third generation family of independence statements would be $\Pi^0_1$ combinatorial statements, so they are finitistic in the sense of Hilbert's program, but they have immediate, apparent mathematical (as opposed to meta-mathematical) meaning. Such a family of statements is considered of great interest. Remarkably, recent work of Harvey Friedman has produced such examples, see for example his book on Boolean relation theory, available at his page.
This is by no means the end of the story. For example, we now have a whole family of independent meta-mathematical statements of increased complexity of which $\mathrm{Con}(\mathsf{PA})$ (the sentence in the second incompleteness theorem) is but the weakest possible. See for example Aspects of Incompleteness by Per Lindström, or Metamathematics of first-order arithmetic by Petr Hájek and Pavel Pudlák. In the context of set theory, we can go further, as the completeness theorem tells us that set theory is consistent if and only if $\mathrm{Con}(\mathsf{ZFC})$ holds. We can go beyond this and require the existence of an $\omega$-model (one whose set of natural numbers is isomorphic to the standard model) or even stronger, the existence of a $\beta$-model (that is, a well-founded model). Woodin has explained how his $\Omega$-logic provides in a sense an ultimate extension to this process.
We also have families of $\Pi^0_2$ statements whose truth is harder and harder to verify. For example, the Paris-Harrington theorem gives a result that is not only independent of $\mathsf{PA}$ but also independent of the theory obtained by adding to $\mathsf{PA}$ all true $\Pi^0_1$ statements. But it is easy to verify once we go beyond this theory. On the other hand, Friedman identified a finite form of Kruskal's tree theorem that cannot be verified by so-called predicative means, which means that adding it to $\mathsf{PA}$ gives us a system with consistency strength significantly higher than that of $\mathsf{PA}$ with, say, Goodstein's theorem.
And we can go beyond, as Friedman has examples of $\Pi^0_2$ statements whose proof requires assumptions of a large cardinal character (typically, the existence of Mahlo cardinals of all finite orders, but recent examples go much further).
In set theory we study the consistency strength hierarchy, and have identified remarkable structure, starting with the identification of the large cardinal hierarchy. For a brief and somewhat technical discussion of these issues, see here. The point is that we can see these results as extending significantly beyond arithmetic the realm of what is true but unprovable (in specific formal systems).
About 1., Gödel's First Incompleteness Theorem is a ingenious exercise of "coding" formal properties and relations regarding a theory $F$ with "a certain amount" of arithmetic inside $F$ itself.
This exercise ends with the definition of the so-called provability predicate $Prov_F(x)$ which holds of $a$ iff there is a proof in $F$ of the formula $A$ with "code" $a$.
To complete the proof, [it is used] the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that
$⊢_F G_F \leftrightarrow ¬Prov_F(\ulcorner G_F \urcorner)$ [where $\ulcorner x \urcorner$ is the "code" of formula $x$].
Thus, it can be shown, even inside $F$, that $G_F$ is true if and only if it is not provable in $F$.
Thus, "reading" the above proof, we can "know of" the truth of $G_F$ (provided that $F$ is consistent) simply because $G_F$ is not provable in $F$ and $G_F$ is equivalent to the formula $¬Prov_F(\ulcorner G_F \urcorner)$.
About 2. :
Why doesn't the fact that $G$ is true constitute a proof of $G$ ?
Because a proof in $F$ of $G_F$ is a precise formal objcet and G's Incompleteness Th shows that such a proof in $F$ cannot exists.
Thus, the conclusion of G's Incompleteness Th is twofold :
For 3. :
By Gödel's Completeness Theorem, there are formal systems in which G is false. How can this not cause a contradiction ?
NO; by G's Completeness Th there are models of $F$ in which $G_F$ is false.
G's Completeness Th, prove that a formula provable in a theory $T$ must be true in all models of $T$.
Thus assuming that $\mathbb N$ is a model of our theory $F$ containing "a certain amount" of arithmetic, we have that all theorems of $F$ (i.e. formulae provable from $F$'s axioms) must be true in all models of $F$.
But $G_F$ is not provable from $F$'s axioms; thus, it must be not true in some model of $F$.
The proof of G's Incompleteness Th give us the insight that $G_F$ is true in $\mathbb N$; thus, it must be false in some model of $F$ different from $\mathbb N$, i.e. in some non-standard model of arithmetic.
Best Answer
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.