Gremlin | Devpost

Inspiration

Compilers optimize code by applying rules a human wrote down. We wanted to know what happens if you throw the rulebook away and just search — give a machine the observable behaviour of a function and let it hunt for any program that reproduces it.

That reframing is the whole project. A compiler asks "how do I transform this code?" Gremlin asks "what code has this behaviour?" The answer doesn't have to resemble the original, and often shouldn't. This is program synthesis, not decompilation.

What we built

Gremlin searches for small integer programs that match a function's input/output behaviour. It evolves candidates, scores them on a GPU, and returns the winner as readable source in its own language.

The contract is deliberately narrow, and the narrowness is what makes it tractable: $0$–$4$ integer arguments, one integer return, widths of $8/16/32/64$ bits, and 27 operators. No memory, no floats, no I/O — not "unimplemented", but outside the contract by design.

Five live experiments run the real engine on a real GPU from the browser:

Shader Detective — recovers a hidden colour transform from input/output pairs alone
Shader Sculptor — turns an image into a layered drawing program
Tiny Robot — evolves a maze controller with three sensors and one bit of memory
Landing Lab — searches for a spacecraft landing controller
Orbit Forge — invents a numerical solver for Kepler's equation

How we built it

The engine is Rust: a parser, a validated IR, a reference interpreter, and an evolutionary search. Candidates are evaluated in parallel by a CUDA kernel on an RTX A4000. Selected programs can be lowered through LLVM to native code, checked against a formal model with Z3, or run against a real binary inside a Bubblewrap sandbox with empty mount/network/user/PID namespaces and a default-deny seccomp filter.

The site is Astro + Starlight with Preact islands. Each experiment ships with a recorded run you can replay instantly, plus a Run button that dispatches real GPU work.

The hard part was the boundary. A public page that can spend GPU time is an obvious abuse target, so the browser can never reach the GPU:

island → job routes (Vercel) → Queue → Tailscale Funnel → GPU worker → signed callback

The worker accepts only a short-lived OIDC token for one exact production subject, binds to loopback, runs one job at a time, and holds no Blob, Queue, or cloud credential of any kind. Tailscale Funnel dials out, so the GPU host never opens an inbound port and its address is never published. The browser gets one capability per job that reads or cancels only that job. An unauthenticated request to the worker gets 401, and there is no reduced-isolation fallback — if the sandbox can't be established, the run fails.

Challenges we ran into

The GPU is slower. On small workloads, end to end, the CPU wins — there isn't enough work to amortize setup. We kept the measurement and published it rather than quietly picking favourable batch sizes. At larger workloads the picture flips: Landing Lab measures $44\times$ on the search phase, Shader Detective $2.78\times$ with a bit-identical search state on both devices.

A compare-and-set that could never succeed. Job state lived in blob storage, rewritten on every progress callback with an ETag precondition. The ETag read back was stale within milliseconds at that rate, so the conditional write failed indefinitely rather than resolving on retry. Every run reached the browser as a lone start event while the worker recorded it as failed. The fix was to stop pretending storage was a database: the worker already stamps a monotonic sequence on every update, which is the correct ordering guard for at-least-once queue delivery anyway.

Staying inside a free tier. Blob allows 2,000 writes/month, and one write per engine event meant a single Shader Detective run cost ~150 of them — about 13 runs before the store cut off. Batching progress into at most one callback per second cut that to 19 writes per run with every event still delivered.

Charting the wrong quantity. Orbit Forge's error curve rose once and then went flat, which looked like a search getting worse. It wasn't. A solver only has to stay inside the tolerance budget; accuracy beyond that is surplus the search spends on speed. Generation 1 held an accurate, slow solver at 345.7 iterations; generation 2 found one at 307.6 that still sits well inside budget. We were plotting error when the thing being minimized was work.

The experiment that failed. We tried to synthesize the full POSIX cksum CRC byte update and it did not converge within budget. Isolating the conditional feedback term made a subproblem small enough to find, which we then assembled into the eight-round update. The failed searches are documented in the repo. A synthesis project that only publishes its wins isn't reporting results.

What we learned

Behavioural equivalence is not structural equivalence. Shader Detective's hidden transform is

$$f(x) = \big(\mathrm{rotl}(x, 8) \oplus \texttt{0x0055aa33}\big) + \texttt{0x00102030}$$

and the search rediscovered exactly that — same three operations, same constants, from nothing but colour pairs. But it didn't have to. Tiny Robot's controller is a 16-entry decision table, one row per combination of three wall sensors and one memory bit; with 8 possible actions per row the space is $8^{16} = 2^{48} \approx 2.8\times10^{14}$. It found a table solving $128/128$ training rooms and $512/512$ rooms it had never seen, in 12 generations and 425,984 simulated episodes — and the table looks nothing like anything we'd have written.

Search invents methods, not just code. Given Kepler's equation

$$E - e \sin E = M$$

Orbit Forge returned a starting point, an update rule, a stopping threshold, a guard and a step cap — six decisions a numerical-methods engineer would make. It chose Halley over Newton and capped itself at 3 iterations. Compiled through LLVM with Clang 18 and timed against a hand-written double-precision reference, it ran $1.53\times$ faster while matching the interpreter across all 65,536 grid points.

Be precise about what a result claims. Every page separates tested from proven. A normal result is evidence from a holdout set, and says so. Z3 can prove things about a reference model — but proving something about a model proves nothing about the binary it came from, and we refuse to let that gap blur. It would have been easy to write "verified" everywhere. It would also have been false.