Rubik

A 3×3×3 cube solver written in Rocq with a machine-checked proof of correctness, extracted to C++ with Crane, and rendered in the browser through raylib and WebAssembly.

Rocq Crane C++ extraction raylib Emscripten Kociemba two-phase
Loading…

Playing

  • Click a face button, or press U R F D L B.
  • Shift inverts a turn, Alt makes it a half turn.
  • Drag to orbit, scroll to zoom, Home to recentre.

What is proved

Any sequence the solver returns really solves the cube, and on a cube a real scramble can produce it always returns one. Both are proved in Rocq, with nothing assumed.

In the browser

  • Searching runs on the drawing thread, since worker threads need headers that static hosting does not send.
  • The page stops painting while Solve works. The desktop build searches in the background.