Why we don't run Lean on the web server.

ProofGarden Lean Judge follows a one-line rule: the web server never executes user-supplied Lean. All real type-checking happens inside GitHub Actions on GitHub-hosted runners, in a clean container, with a pinned lean-toolchain.

Defence in depth

1. Static filter.A first-pass scan rejects bodies that contain tokens that don't belong in a tactic block (sorry, admit, axiom,def, theorem,#eval, native_decide, …).
2. Server-generated file. The user only submits the proof body. The Lean file (imports, namespace, theorem header,#print axioms line, terminator) is rendered server-side from challenge metadata.
3. Branch isolation. The generated file lands on a fresh submission/<id>branch. The judge repository's mainis protected; the workflow filters on a specific path glob, so user-pushed branches can't bypass it.
4. Pinned toolchain. The judge repo carries the only allowed lean-toolchain andlakefile.lean. Users cannot edit them.
5. Commit-SHA verification. Both the webhook and the polling refresh refuse to accept a run whose head_shadiffers from the SHA we recorded when we pushed the file.
6. Append-only ledger. Every Seed change writes aLedgerEntry and increments the balance in a single Prisma transaction. Awards for a given submission are idempotent.

Full threat model: docs/SECURITY.md.