How to prove a LTL formula correct in a specific model?
Your intuition is correct.

Consider an arbitrary path starting from $q_3$: let it be $q_3\, q\, q'\, q'' \ldots$. We need to prove it satisfies $\varphi = (X\lnot a)\rightarrow (FG \lnot a)$.

We proceed by cases on the second state $q$ in the path. It can be  one of $q_1,q_2,q_4$.

If $q=q_4$ then $X\lnot a$ is false in the path, hence $\varphi$ is true in the path.

If $q=q_1$ or $q_2$ then we must have $q'=q''=\cdots=q_2$. The whole path is of the form
$q_3\, q\, q_2\, q_2\, q_2 \ldots$. This path makes $FG\lnot a$ true, since there exists a suffix (namely, $q_2\, q_2\, q_2 \ldots$) where $G\lnot a$ is true ($a$ is false in each state of the suffix). Hence, $\varphi$ is true in the path.

You could make this even more formal by explicitly referring to the definition of validity.