The cheat is
unsatisfiable.

The game.

Automatafl is a turn-based board game where all players move at once. Each player secretly writes a rook-style move; the moves are revealed simultaneously, and if two players grabbed the same piece or aimed at the same square, that's a conflict · everyone involved must re-enter, and the fought-over coordinate is marked off-limits for the redo. Once the round is clean, the moves resolve together, and then the Automaton · a neutral piece with its own convoluted step rules · takes its step. You win by luring the Automaton into your corner.

Simultaneous secret moves, recursive conflict re-entry, and a rule-driven neutral actor: it is exactly the kind of game whose disputes are miserable to referee by hand · and exactly the kind of state machine a proof system can hold whole.

The theorem.

The deployed circuit doesn't merely check moves. The correspondence goes all the way up: a satisfying trace of the deployed descriptor at the real 11×11 board is the game's resolution step. The capstone theorem, turn_sat_imp_roundStep, composes the resolve leg and the automaton leg over a fold-enforced seam · so a proof that the circuit accepted your turn is a proof that the board evolved by the rules, cell for cell.

Conflicts included. The multi-round capstone, braid_sat_imp_runTurn, extends the theorem across conflict re-entry rounds · clash, re-enter, clash again, resolve · with termination proved (a turn ends within n² rounds), and the whole braid folds into one verifying STARK proof. The first full multi-round turn proved end to end took 1,663 seconds of prover time. A real number, from a real fold, at the deployed board size.

Seven wounds.

Proving that correspondence was not a formality, and that's the point of telling it. On the way to the capstone, the correspondence campaign surfaced seven distinct defects in how the circuit's board rewrite and the game's actual rules lined up · a two-cycle that behaved wrong in vacuum, an occupancy-blind swap, a flow-through on exclusive occlusion, four more. Each one was pinned with a machine-verified falsifier: a concrete board where the old circuit and the real game disagreed, checked by decide, flipping green when the fix landed. The audit for an eighth came back clean · identical-move handling was sound as written.

Earlier still, an executable differential between the Lean rules and the original running prototype found four real bugs in the prototype. The spec didn't just describe the game. It debugged it.

The deletion.

Once the proven descriptor held the whole turn, the scaffolding came down · and the commit log says it plainly:

There is no second implementation to drift from the first. The house law behind those deletions is standing policy across the whole project: rule systems are authored in the proof assistant and emitted; nothing hand-written survives beside the proven object as a "fallback," because a fallback is a future disagreement.

What a cheat looks like now.

Remember the conflict rule: after a clash, the fought-over coordinate is marked, and playing it again in the redo round is illegal. In the shipped circuit that rule is not an if statement. It is a gate over the committed marks:

play a marked coordinate in the redo round:
  the legality gate over the accumulated marks cannot be satisfied
  → no witness exists → no proof exists → the turn never happened

forge the middle board between rounds:
  the fold's board-window seam binds each round to the last
  → the forged-mid canary bites · the substitution refuses

The commit that shipped it: "the marked-move cheat is now UNSAT at the deployed prover." That's the whole design in one line. A cheat isn't caught, reported, or punished. It is a statement with no witness · the dishonest game is a board state that cannot be constructed.

The room this lives in.

Automatafl is the sharpest example of a wider room: games as verified state machines. On a live game platform built with a collaborator, seven further playable games consume exact Lean-emitted rule tables · the browser renders and the player plays, but nothing client-side ever scores. Judged play settles as a finalized turn on the same substrate the theorems govern. Places whose laws are theorems · and whose cheats, therefore, are unsatisfiable.