How do I get and/or verify a formal Grammar for a given formal Language?
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).