Is my simplified explaination of the XOR swap correct?
Your proof is correct in intention, but the style is not adequate.

Of course, there is no perfect style, and most of us could improve
their style, myself included.

Still, hoping readers will not be too harsh, here is an attempt at
writing it, as an example, following your own proof. It may be too
verbose, one of my own failings. (it is also a bit intentional here)

Actually the style usually depends also on the audience you are addressing. If the intended audience is very competent in the field, you can skip a lot of details. Nevertheless, careful notation always helps (like the indexing $a_0$ below).



The XOR swap is a well-known in-place algorithm to swap two values, by
XOR:ing them bitwise. It goes as follows for two variables a and b, using the notation of the C programming language:

a = a^b

b = a^b

a = a^b


Correctness proof

We note the XOR operation $\oplus$ as is common in mathematical uses. This notation is justified by the isomorphism between XOR on the booleans and the addition in $\mathbb{Z}/2$.

The algebraic properties of XOR extend to bitwise operations on bit
vectors (i.e., sequences of bits) of equal sizes. In particular it
remains associative and commutative, and we have for any sequence $x$
of bits: $x\oplus x=\vec{0}$ where $\vec{0}$ is a bit vector of $0$´s of the
same length, and $x\oplus\vec{0}=x$.

Assume the initial values of a and b are respectively $a_0$ and
$b_0$.

The 3 assigments above are then equivalent to:

a =$a_0\oplus b_0$

b =$(a_0\oplus b_0)\oplus b_0$   which simplifies algebraically to $a_0$ as indicated above

a =$(a_0\oplus b_0)\oplus a_0$   which simplifies to $b_0$

The initials values of a and b have been swapped bitwise. $\;\Box$



Though I may be in some disagreement over this with other users, I do not
see the usefulness for this proof of insisting on the relation between
XOR and addition (other than for justifying the notation). Of course,
the generalized view of Yuval Filmus]1 brings wider understanding, but
the point for me is to have a simple proof, not to write a treatise.

Note that I have been using distinct notation for syntax (taken fron
C) and for the semantics of these operations. This justifies having
two notations for the XOR operator, and gives a cleaner presentation
of the proof, which may sometimes be important.

Of course, one is not always that careful, but it is better to have
these principles in mind, without overdoing it, depending on the
purpose and audience of what is being written. I think the most important here was to distinguish a and $a_0$.

Hoping this version will satisfy most readers. Further comments welcome.

With my thanks to all for all the very useful comments. Perfection is not of this world.