We consider the problem of gathering in finite time and at the same location, not known beforehand, a set of deterministic semi-synchronous robots, starting from an arbitrary initial configuration that may even be bivalent (that is, a configuration where the robots are evenly split on two different locations). This problem is known to be unsolvable when the robots are oblivious, that is, when they cannot remember their past actions. We present a deterministic gathering algorithm where robots may remember and communicate one bit of memory. This bit may be arbitrarily (and adversarially) set in the initial configuration. Our solution is thus memory optimal and self-stabilizing. Its proof of correctness is formally certified by the Coq proof assistant using the Pactole framework.