I am following Spivak's Category Theory for the Sciences, and I would like to make sure I understand this proof correctly.
We begin from $C$ and is originally taking $G_1\circ F_1$ (ie. top left corner of the square) to get to $E$. And the argument is, regardless of whether we take the LHS $(\beta_2 \circ \beta_1)\circ(\alpha_2 \circ \alpha_1)$, or RHS $(\beta_2\circ \alpha_2)\circ(\beta_1\circ \alpha_1)$, we still end up at $G_3 F_3$, ie the square commutes.
If we take the LHS, $\alpha_2\circ \alpha_1$ would move $F_1$ down to $F_3$, so we go from $G_1 F_1$ to $G_1F_3$. Then $\beta_2 \circ \beta_1$ move $G_1$ down to $G_3$, so we go from $G_1F_3$ to $G_3F_3$.
Likewise, $\beta_1\circ\alpha_1$ gets us from $G_1F_1 \to G_1F_2 \to G_2F_2$, and $\beta_2\circ \alpha_2$ gets us $G_2F_2\to G_2F_3\to G_3F_3$. Therefore both sides of the iff end up at the same morphism/object in $E$. Is this understanding correct?
Also is this considered a good enough proof by just using a graph? Or is there a more vigorous formal proof available/necessary?
First a small remark about notation. Composing $\alpha_1$ and $\alpha_2$ is a different kind of operation than composing $\alpha_1$ and $\beta_1$. The former is called vertical composition and the latter is called horizontal composition. In the screenshot you posted this difference is indicated by using the circle $\circ$ for vertical composition and the diamond $\diamond$ for horizontal composition (another popular symbol for horizontal composition is $*$). You have written $\circ$ everywhere, this may cause confusion.
The above remark about different kinds of compositions holds for any (strict) 2-category. In this case you are interested in a particular setting: namely the category of categories with functors and natural transformations. The horizontal composition there has a name: the Godement product. Spivak also uses the notation $\diamond$ for whiskering, a way to combine a natural transformation with a functor.
What you have done in your post is correctly identify the possible paths to take, but you have not proved these are equal. Checking this comes down to checking that each of the smaller squares in the screenshot commutes, as written in the screenshot as well. Once you have verified that each of the smaller squares commutes, then you have a rigorous proof.
You can do this all by hand, but we can be smarter about it. Each of the smaller squares corresponds to the horizontal composition of two natural transformations. That is, each of these squares is of the form $\require{AMScd}$ \begin{CD} G F @>{G \diamond \alpha}>> G F' \\ @V{\beta \diamond F}VV @VV{\beta \diamond F'}V\\ G' F @>>{G' \diamond \alpha}> G' F' \end{CD} for functors $F, F': \mathcal{C} \to \mathcal{D}$ and $G, G': \mathcal{D} \to \mathcal{E}$, and natural transformations $\alpha: F \Rightarrow F'$ and $\beta: G \Rightarrow G$. So you only need to check that such a square always commutes. It would be a good exercise to check it (or see below), but it is also already mentioned in Spivak's book. This square is namely precisely the definition of the horizontal composition $\beta \diamond \alpha$, see definition 5.3.2.17 (I think, the numbering in the copy I have differs from yours, for me it is 4.3.2.17).
To check that the above mentioned square commutes, we first briefly recall the definitions of whiskering linked earlier. With the notation from above
So we have to check that $(\beta \diamond F')_X \circ (G \diamond \alpha)_X = (G' \diamond \alpha)_X \circ (\beta \diamond F)_X$, for all $X$. Writing out the definitions, we have to prove $\beta_{F'(X)} \circ G(\alpha_X) = G'(\alpha_X) \circ \beta_{F(X)}$. But this follows directly from naturality of $\beta$, which should be clear when we put it in a diagram: \begin{CD} G F(X) @>{G(\alpha_X)}>> G F'(X) \\ @V{\beta_{F(X)}}VV @VV{\beta_{F'(X)}}V\\ G' F(X) @>>{G'(\alpha_X)}> G' F'(X) \end{CD}