Twelve Puzzles, Each With a Proof
Breakout's difficulty was tuned statistically: a bot played ten thousand games and the clear rates said whether the levels were fair. That works for an arcade game, where difficulty is a distribution. It does not work for a puzzle game. A Sokoban level is not 15 percent solvable. It is solvable or it is broken, and if it is broken, the player you fooled into trying it will not come back.
So game five changes the question again. Posts one through four asked whether the AI's code was correct and whether its tuning was fair. This one asks whether its content can be trusted, and answers with the strongest tool there is: a proof. Every level in the game below ships with a machine-checked certificate that it can be solved, plus the minimum number of pushes it takes. The HUD shows you that minimum while you play, which is either encouragement or taunting depending on how your attempt is going.
arrows / WASD or swipe · Z undoes · R restarts · the title screen is the solver playing its own solution
The solver
Sokoban is a classic search problem, which is exactly why it fits this series: correctness you can enumerate. The solver Claude wrote is about eighty lines of breadth-first search with two ideas that matter.
First, it searches over pushes, not steps. Walking does not change a puzzle's state in any way that matters, so the player's position is collapsed into "which region can they reach," normalized to one representative cell. What is left is a graph where a state is the set of box positions plus a region, and an edge is a single push. The branching factor drops from four walk directions to only the pushes that are actually possible.
Second, it prunes stillborn states. A box pushed into a bare corner is never coming out, so any state containing one is skipped without expansion. With those two tricks, the hardest level in the set proves out in under half a second, and a level with no solution exhausts its entire state space and comes back with the other kind of certainty: provably impossible.
That second kind turned out to be the important one.
A third of the levels were broken
Here is the honest part. Claude was the level designer too, and it worked the way a human designer drafts: sketching wall shapes that felt like puzzles, placing boxes and goals, trusting its read of the geometry. Twelve levels came out of that. Then it ran make solve on its own work.
Four of the twelve came back provably unsolvable. A 33 percent defect rate, from the same session that wrote the working solver, and the rejects were not the ambitious ones. Two were levels the model was confident enough about that, without the gate, they would have shipped.
The traps were geometric and invisible to a read-through. The best one: a map with two wall stubs that split it into halves, connected through a single doorway cell. The intended solution parked a box on that doorway's far side, which worked fine, except the parked box then sealed the only route to the position needed for the final push. Every playthrough of that level would have ended one move from victory, staring at a box that could never turn the corner. Claude initially disputed its own solver's verdict, re-traced the geometry step by step, and conceded: the level it designed and believed in was impossible.
The other failures were the same species: a goal column enterable on only one row, mirrored goals where each one's final push required the other to be empty first. Plausible shapes, dead geometry. The fix loop was mechanical: adjust the layout, rerun the gate, read the verdict. The gate exits nonzero if any level lacks a proof, so an impossible puzzle cannot ship without deliberately breaking the build.
The proof table
make solve prints this, and it is the level select screen's source of truth:
| # | level | boxes | min pushes | states explored |
|---|---|---|---|---|
| 1 | First Push | 1 | 1 | 2 |
| 2 | Side by Side | 2 | 2 | 12 |
| 3 | Around the Post | 1 | 3 | 10 |
| 4 | Pivot | 2 | 4 | 38 |
| 5 | Storeroom | 2 | 4 | 41 |
| 6 | Corridor | 2 | 6 | 36 |
| 7 | Three Shafts | 3 | 6 | 1,538 |
| 8 | Three Crates | 3 | 7 | 935 |
| 9 | The Hook | 2 | 8 | 81 |
| 10 | Detour | 2 | 10 | 200 |
| 11 | Warehouse | 4 | 11 | 14,809 |
| 12 | The Vault | 3 | 21 | 3,928 |
The ordering is the solver's. Claude's draft ordered the levels by feel, and feel was wrong twice: a six-push level sat in slot four and a ten-push level ran ahead of an eight. Minimum pushes is not a perfect difficulty measure (states explored says Warehouse makes the search sweat hardest, and it is genuinely the meanest level in the set), but it is a measured one, and measured beats vibes for the third post running.
One more honest touch: the demo playing on the title screen is not a recording. It is the solver's own solution path, replayed move by move, for a different level each time it loops. The thing that proved the levels plays them for you while you decide whether to.
Two kinds of confidence
This series has now used the harness two very different ways. Breakout's tuning was statistical: thousands of noisy games, confidence as a percentage. Sokoban's gate is logical: exhaustive search, confidence as a yes or no. Most real software verification lives on exactly this spectrum, load tests on one end and type systems on the other, and the interesting engineering judgment is knowing which end your problem belongs to.
Puzzle content belongs to the proof end. A clear rate cannot tell you a level is impossible, only that nobody happened to clear it yet. The solver can say never, and it said it four times about levels designed by the same model that wrote it, before a single player was harmed.
Five games in, that is the series' actual finding, restated once more: the code was never the hard part. The hard part is building the instrument that tells you the truth about what you made.