From a logic viewpoint, verifying a proof is a syntactic business, also known as symbol pushing, whereas understanding a proof is a semantic matter. I cannot resist giving a layman analogy as an appetizer: Many people can follow a recipe to bake a cake, but not as many can design the recipe or know how to tweak it to make something else.

Many of the best examples involve the proof of an existential statement that requires constructing a complicated witness for it. You may be familiar with the construction of the reals via Dedekind cuts of rationals or via Cauchy sequences of rationals, and these proofs can be easily checked step by step by any student who understands some basic mathematics, but how many students truly understand these constructions? Do they know that the Dedekind cut approach extends to completion of linear orders, while the Cauchy sequence approach extends to completion of metric spaces? Do they get some sense of wonder that both ways happen to produce the same result in the case of completing the rationals?

In a similar vein, one can construct the complex numbers by defining them to be the set $C = \mathbb{R}^2$ with $+,·$ defined by $(a,b)+(c,d) = (a+c,b+d)$ and $(a,b)·(c,d) = (ac-bd,ad+bc)$, and then checking that $(C,+,·,(0,0),(1,0))$ is a ring and that $(a,b)·(\frac{a}{\sqrt{a^2+b^2}},-\frac{b}{\sqrt{a^2+b^2}}) = (1,0)$ for every $(a,b) ∈ C ∖ \{(0,0)\}$. But in my view this proof ought to feel mysterious and unsatisfying unless you actually understand the motivation for these definitions and know the construction via field extension (i.e. $R[X]/(X^2+1)R[X]$). This is because there is a priori no reason at all for the above definitions of $+,·$ to make $·$ associative and distributive over $+$, unless you already understood that the reals can be extended to a field with some element $i$ such that $i^2+1 = 0$, and that the resulting field must be a vector space over the reals with dimension $2$, which together force $+,·$ to necessarily obey those definitions! Otherwise, you would be totally in the dark as to why those definitions should work, even though you can plainly see that they do.

These are examples from basic mathematics, but I hope it demonstrates how an existential statement might have a proof that does not in itself provide any understanding of the proof, in the same way you might observe that the cake mixture rises upon baking without having a clue why it does...

As for personal experience, there is one particular proof that I have never felt I really understood, even though I have a solid grasp of the formal proof itself: $ \def\pa{\text{PA}} $

Theorem: Let $T = \pa + \{ \ c>1 \ , \ c>1+1 \ , \ c>1+1+1 \ , \ \cdots \ \}$, where $c$ is a fresh constant-symbol. Then $T$ is conservative over $\pa$.

Proof: Take any arithmetical sentence $Q$ such that $\pa ⊬ Q$. Then $\pa+¬Q$ is consistent and so has a model (by completeness), which clearly finitely satisfies $T+¬Q$, and hence $T+¬Q$ has a model (by compactness). Thus $T ⊬ Q$.

Although I completely understand the completeness and compactness theorems, I somehow cannot intuitively understand how this proof works. Why should we have to invoke models? Can we instead directly show that every proof of any arithmetical $Q$ over $T$ can be converted into a proof of $Q$ over $\pa$?