Eric Spencer
projects
A Rubik's Snake folds into a ball, a dog, and back into a stick. It is 24 right-triangular prisms strung together on a chain, with 23 joints between them, and each joint clicks into one of four positions (0°, 90°, 180°, 270°). Ignoring physics, that gives 4^23 = 70,368,744,177,664 possible configurations, and somewhere around 13.4 trillion once the wedges are required not to pass through each other. Peter Aylett did the exhaustive backtracking search in C in 2011 and patched it in 2022. This project asks the same question with formal methods instead of brute force, as an offshoot of ongoing AI-for-formal-methods work.
This repository explores formal verification of the Rubik's Snake puzzle in Coq and TLA+. The related-work section covers the puzzle's existing academic literature, including work by Hou, Chen, Li, and the Luxembourg group on its geometry and Eulerian paths.
Two specifications and a Python reference enumerator:
coq/ holds the Coq (now Rocq) formalization. It defines wedges as triangular prisms in a 3D integer grid, joints as one of four rotations, and the validity predicate (no_collision) that says no two wedges occupy overlapping voxels. It proves structural properties: decidability of equality on rotations, completeness of the rotation enumeration, and well-formedness of the snake-construction function. Most of the work is geometric, in an apply_rotation that takes a Direction (one of six axis-aligned 3D directions) and a Rotation and gives the next wedge's position and orientation.tla/ holds a TLA+ spec that models the snake as a state machine. Each action is "pick a joint and rotate it." The invariant is NoSelfIntersection. TLC runs on small instances, and 8-wedge snakes finish in seconds. The full 24 is far past what TLC can model-check, which is part of the point: the general claim needs Coq, and TLA+ gives concrete confidence on the small cases.python/ holds a reference enumerator that sanity-checks the formal specs against Aylett's numbers. For 8 wedges it produces the same valid-configuration count Aylett does, which is evidence against a bug in the wedge geometry.The Coq file opens with a summary of what the rotations are:
(* Each joint has 4 possible rotations: 0°, 90°, 180°, 270° around the shared edge. *)
Inductive Rotation : Type :=
| R0 (* 0° — straight *)
| R90 (* 90° — right angle *)
| R180 (* 180° — folded back *)
| R270 (* 270° — left angle *).
The whole thing is built on a 3D integer grid with 6 axis-aligned directions, so the proof never has to deal with floating-point rotation matrices. Everything is Z-arithmetic, and Lia can close most of the arithmetic obligations.
The count is not proved. Aylett's number (13,446,591,920,995 valid configurations) is established by exhaustive search. Proving it formally in Coq would require either reflecting the enumerator into Gallina and computing it, which is impractical since the search took weeks of CPU time in C, or a combinatorial argument that nobody has found yet. What the repo has is the formal specification of what a valid configuration is. The bridge from spec to count is still empirical.
The symmetry quotient (mirror plus cyclic) that Aylett applies to drop the count from 13.4T to 6.7T is also not fully worked out. The TLA+ spec does not have it at all, and the Coq side has a stub.
It is a hobby-scale formal verification project: small enough to finish, and connected to the AI-for-formal-methods (ai4fm) work going on alongside it. As a project to learn Coq on, the geometry of a physical puzzle is a change from verifying insertion sort. The state space is huge, but every individual piece of reasoning is concrete, and the puzzle can be held in hand and checked against the math.
The README has build instructions for Coq 8.18+ / Rocq and the TLA+ Toolbox.