Rubik's Snake — Formally VerifiedCoq (Rocq) and TLA+ specifications of the Rubik’s Snake state space — 4^23 configurations, formally