The WHUTS project is collecting space-filling tilings of those octocubes that are nets of the hypercube, generally using a pictorial demonstration of the tiling. However it occurs to me that it should be possible to write a formal rigorous proof of that octocube #192 tiles space, something like this:
Consider the octocube consisting of the unit cubes at the following positions: (0, 0, 0), (0, 1, 0), (1, 1, 0), (1, 2, 0), (1, 2, 1), (1, 3, 1), (2, 3, 1), (2, 4, 1). This octucube can be used to tile space. Proof:
The unit cubes of the given octocube satisfy the property that no two cubes have the same parity, and because there are conveniently 8 unit cubes then all possible parities in all three dimensions must be exactly accounted for. This means that given a unit cube at position (x, y, z), exactly one unit cube of the octocube has the same parity, and therefore there exists a unique translation of the form (2a, 2b, 2c) that translates the octocube to cover the unit cube at (x, y, z). The set of translations of the form (2a, 2b, 2c) therefore tiles space.
Is this proof rigorous, or can it readily be made so?
Yes, this proof looks correct. Here is essentially the same argument in slightly more formal language (though I think the wording of your original post is fine):
Let $S$ be the set of integer positions of the cells of the octocube, and $2\mathbb{Z}^3$ the set of coordinates whose positions are all even integers. Then the claim is that every triple of integers is uniquely representable as a sum of an element of $S$ and an element of $2\mathbb{Z}^3$. As you observed, we make note of the fact that $S$ contains every possible triple of parities exactly once.
To see that such sums cover every point at least once, we can just exhibit a constructive algorithm: given an arbitrary point $P = (a,b,c)$, we choose an element $s\in S$ with the same parity, and then $P-s \in 2\mathbb{Z}^3$ as desired.
To see that they don't hit any point twice, suppose that $s+e_1=t+e_2$, where $s,t\in S$ and $e_1,e_2\in2\mathbb{Z}^3$. But then $s-t = e_2-e_2 \in 2\mathbb{Z}^3$, so $s$ and $t$ have the same parity, which means $s=t$, so subtracting we also have $e_1=e_2$, and thus the two sums come from the same two elements.