Approach: replaying a counter until a regrouped digit halts it

Left of the head is a counter written in three-cell digits; right of it is a long "bell", a row of 001 blocks with one odd block, 0001, inside. Each round, the head adds 1 to the counter, walks out to the odd block and moves it one block closer to the counter. When it arrives, the bell bites a few cells off the counter's low end, and the odd block starts over near the bell's far end: one cycle.

The key idea: most rounds are plain counting. On digits whose middle cell is 0 ("clean" digits), a round adds 1 in base 4, each digit standing for −1, 0, 1 or 2, so long stretches of rounds reduce to arithmetic. The surprises come from bites: a bite usually removes a number of cells that is not a multiple of 3, so the remaining cells regroup into new digits, each made of the end of one old digit and the start of the next. That can create "dirty" digits (middle cell 1), which counting never makes and later carries usually clean up.

Why it halts: the machine stops when a carry reaches a dirty 110 while the next higher digit ends in 1. Over 611,578 cycles, a 110 or 111 appears right after a bite only 369 times, and only in the last cycle does the next higher digit end in 1. There a carry turns the 111 into 110 (round 3,339), and the next carry to reach it (round 7,435) hits the missing instruction. Summing exact per-cycle step formulas, in three independent counts, gives about 1.8 quintillion steps (1,816,824,067,232,869,945).

In Rocq (busycoq), clean rounds are proved lemmas applied in batches, and all other rounds run on a verified simulator. A checker, proved correct once, replays the run from step 288 in 4,942,483 checked moves; this proves halting, not the step count.