An unsolvable puzzle cannot ship

Axiom is a puzzle game for Android whose puzzles are theorems: you grow a proof tree by hand, and a verification kernel on the phone decides whether you have proved anything. The kernel is one file, web/js/kernel.js, 758 of the 3,113 lines of JavaScript in web/js and tools/ as I cloned it on 12 October 2026, and nothing outside it is trusted. Before a release, tools/par.js runs the kernel's own solver over all 44 theorems, replays and re-verifies every proof it finds, writes the results to pars.js, and exits with status 1 if a single theorem could not be finished. An unsolvable puzzle cannot ship, not because somebody re-read the content, but because one script runs the player's own checker over all of it, and its exit status is the gate. The lesson is older than the app: keep the checker small enough to read, derive everything through it, and make one script prove the content before it ships.

A small language and a smaller parser

The kernel is an engine for classical natural deduction, which the Stanford Encyclopedia of Philosophy describes as "a type of logical system described initially in Gentzen (1934) and Jaśkowski (1934)". Its language is first-order, with a grammar that fits in six lines of comment above the parser: implication is right associative and binds loosest, then disjunction, conjunction and negation, and a quantifier takes one or more names and a dot. Negation is not a connective of its own; ~P is parsed as P -> false. The lexer is thirteen lines, the recursive-descent parser under forty, and a name is a variable only when a quantifier in scope has bound it. The 44 theorems in content.js and the 39 axioms, which the app calls tools, are text run through that parser, such as all X Y. eq(X,Y) -> eq(Y,X).

Dragging a tool onto a goal is one-way matching: strip the tool's leading universals, peel off as many premises as possible, and match the conclusion against the goal, binding each metavariable once and refusing a second binding that differs. Variables bind on the tool's side only, which makes it matching rather than unification. A slot the match leaves open is filled by the player from a pool of at most fourteen ground terms, and the premises become new goals.

Nothing in the interface is trusted

The header of board.js says it plainly: "this file never marks a goal closed on its own". Every move goes through Kernel.apply, and a step the kernel refuses produces a toast rather than a change. The rules live in one function, children(), which returns the child sequents a rule demands, or null. It has ten rule tags: split, suppose, pick, cases, contradict, induct, fix, fixEx, witness and use. apply() and verify() both call it, so the interface cannot invent a step the kernel would not sanction.

verify() is the part I would keep if I had to throw the rest away. It walks the finished tree from the root and re-derives every child, and it fails for nine named reasons, among them a node reached twice, a step that does not follow from the rule it claims, a goal altered after the step that made it, and detached nodes. The victory card appears only when it returns "checked from the root", and prints that phrase. The shape is the one Robin Milner's LCF gave proof assistants in the early 1970s, where "theorems are derived using only the inference rules given by the operations of the theorem abstract type". A closed goal in Axiom is a flag that only kernel.js ever sets; the board only draws it.

The solver is the rules run forwards

The solver, solve(), is in the same file because it uses the same rules. It is depth-first iterative deepening: one move, then two, and so on up to a maximum, with a budget per depth of 400,000 calls; a depth that runs out is abandoned and the search moves on to the next. Richard Korf's 1985 paper showed the method "asymptotically optimal along all three dimensions for exponential tree searches", time, space and the cost of the solution path, and the third is what matters here: the first proof found is the shallowest, and the shallowest proof is par. Three cheap prunings keep it inside the budget: give up when there are more open goals than moves left, remember each set of open sequents at each remaining depth, and try the moves that create the fewest new goals first.

The exit status is the gate

tools/par.js is 49 lines. For each theorem it calls solve() with a maximum depth of 11 and the 400,000 budget, then does what a quicker script would skip: it builds a second fresh state, replays the proof with applySeq(), runs verify() and checks that no goal is open. A proof that does not replay counts as a failure. The lengths go to web/js/pars.js, and the process exits with status 1 if anything failed. The README says the build fails; strictly, nothing in the repository runs the script for you. The Gradle build does nothing with web/ but copy it into the app's assets, so the gate is the exit status, read before gradlew bundleRelease. Ignore it and the failed theorem ships anyway: pars.js is written without it, the board shows a question mark for par, and store.js scores the player against their own length. The header of content.js says the rest: "Every par in this file is produced by the kernel's own solver in tools/par.js, never typed by hand."

The file it writes has 44 entries between 1 and 10. The single 1 is the first theorem, a segment is equal to itself; the single 10 is the induction proof that every number is even or odd. Crowns are scored against par: gold needs no hints and a proof no longer than par, silver is within two moves, and the victory card says what gold means, "This matches the shortest proof the kernel can find." Leaderboards were left out because they need a server, and rather than fake them the game scores against its own solver.

What the gate does not prove

The gate proves derivability, not truth. The 39 tools are axioms, and a wrong one would let a false theorem through with a clean verify() and a par. So the trusted base is the kernel plus those 39 formulas, plus the parser's reading of them: if -> associated to the left, every theorem would say something else, and par.js would cheerfully prove the something else. That is why the grammar is written down and the parser is under forty lines. The LCF entry notes that the compiler underneath "adds to the trusted computing base"; here that is the WebView's JavaScript engine, which I cannot shrink. The kernel is a quarter of the app's JavaScript, and the other three quarters can be wrong without producing a false "proved".

Par is also only as good as the solver's caps: fourteen candidate terms, eight bare names for a tool with two open slots, and 400,000 calls per depth. A shorter proof that needs a term outside that pool would not be found, nor would one hiding at a depth the solver had to abandon, and a player who found either would beat par, which is why the victory card says the shortest proof the kernel can find.

The rule

Freek Wiedijk's comparison of seventeen proof assistants lists a "small proof kernel" as a property a system either has or lacks, and footnotes it: "This is also called the de Bruijn criterion." A game is an odd place to apply it, but the reason it holds is the same. A player's trust in "you proved it" is worth exactly as much as the smallest piece of code that can say it, and 758 lines is small enough to read in an evening. Then point the same code at the content. If the solver cannot prove a puzzle with the checker that will judge the player, the script says so with its exit status and the puzzle does not ship. What has to be remembered is one command and its exit status, not forty-four proofs.

Axiom is on Google Play and the source is on GitHub.