How do I get and/or verify a formal Grammar for a given formal Language? I was given the Language $L=\left \{ a^nb^na^nb^n |n\epsilon \mathbb{N} \right \}$ and I'm supposed to find a Grammar that generates that Language.
After some trying and fiddling I found one that I think works. The question is how do I verify it? On paper it looks fine, but are there some tools check this for me? Also are there easier methods than trying out by hand or brute force?

The Grammar I found is as follows:

$S\rightarrow aB_{1}A_{2}B_{2}|aB_{1}PA_{2}B_{2}$

$P\rightarrow A_{1}B_{1}A_{2}B_{2}|A_{1}B_{1}PA_{2}B_{2}$

$B_{1}A_{1}\rightarrow X_{A1}A_{1}$

$X_{A1}A_{1}\rightarrow X_{A1}X_{B1}$

$X_{A1}X_{B1}\rightarrow A_{1}X_{B1}$

$A_{1}X_{B1}\rightarrow A_{1}B_{1}$

$B_{2}A_{2}\rightarrow X_{A2}A_{2}$

$X_{A2}A_{2}\rightarrow X_{A2}X_{B2}$

$X_{A2}X_{B2}\rightarrow A_{2}X_{B2}$

$A_{2}X_{B2}\rightarrow A_{2}B_{2}$

$aA_{1}\rightarrow aa$

$aB_{1}\rightarrow ab$

$bB_{1}\rightarrow bb$

$bA_{2}\rightarrow ba$

$aA_{2}\rightarrow aa$

$aB_{2}\rightarrow ab$

$bB_{2}\rightarrow bb$
You don't really need the various $X$ nonterminals, just use rules $B_iA_i\to A_iB_i$ instead. 

For correctness, use induction to show (1) that you can reach $aB_1(A_1B_1)^k(A_2B_2)^{k+1}$, and from there $a^{k+1}b^{k+1}a^{k+1}b^{k+1}$, for all $k\ge 0$, and (2) that all generated words have the required form. For the second part, try to find some auxiliary conditions (e.g. numbers of $A_i,B_j$ match; if a factor $B_1A_1$ is not rewritten to $A_1B_1$ before the $B_i$ is replaced by $b$, the derivation gets stuck; etc).