What’s the Job Now? Where LLM Agents, Formal Methods, and Reproducible Environments Could Point the Working Developer.

An LLM agent built a bot that plays Screeps, a strategy game for programmers. It wrote the spec the code is generated from, as well as most of the infrastructure. My job was direction and inspection. . The result fits on one disk image. If you have tmux and QEMU, you can boot it and watch the bot play.

We’ve had large language models for several years now, with all of their well-known shortcomings. The agent that built this bot has them too. It worked because of what surrounds it: a research field converges around exactly that arrangement. There’s no one weird trick to manage klanker slop. It took several tools working in concert. I’d like to take a look at what the confluence of LLM agents, formal methods, and a reproducible environment points to for the working developer.

Can the on-ramp be widened?

dox-populi will be a curriculum: an on-ramp to tools that used to need a specialist. I find that organizing a curriculum around a game is a good way to make it approachable. I chose Screeps because it’s simple enough to pick up, it has a user base, and its tutorial hands us a starting point somebody else defined. Nix makes build and deployment simple. Paradox leverages formal methods: a spec language the agent writes in, a checker behind it, and the decision code generated from the spec that survives.

The LLM agent can also be our tutor. When I didn’t understand what it had built, I asked, and the answers came in plain language. Every post in this series will quote those exchanges from the session transcripts. It also wrote the lines it explains. So my understanding comes from questioning the agent, and verification comes from Paradox. The agent writes a spec of the Screeps bot’s decisions. Paradox checks it with an SMT solver; I inspect what passes, and so will you. What doesn’t hold together never reaches the game.

Formal methods are well-studied, and have been used for years to build software that has to be correct. However delivery is expensive. A spec had to be filled out by someone who knew how to write specs, and that used to be a specialization. The agent is what changed the cost. An LLM samples from the space of plausible programs, and a plausible program can be wrong in ways that don’t look wrong. The spec language narrows what the agent can say down to decision structure. The check rejects a spec that contradicts itself, and a case the agent never considered comes back as a failure with the case named. On its own, the agent’s output is unchecked. On its own, Paradox waits for an expert. Put them together and the on-ramp into formal methods gets wider and less steep. The deep expertise is still where it always was: with the people who built Paradox and the solver under it. This project is one step up the ramp.

But if delivery isn’t reproducible, the whole exercise just becomes something that works on my machine, and a claim you can’t interrogate is a claim you don’t have to believe. This series asks you to reproduce and interrogate. Therefore Nix.

The More Things Change …

The dev cycle starts with infrastructure: a flake that delivers the same shell to every machine. Dox-populi uses DetNix. The development shell contains all the tooling needed to build, develop, and deploy dox-populi. All except one tool, the LLM agent. That’s what you bring.

While dox-populi leverages emergent technology, I try to stay true to established CI/CD principles. The agent increased velocity and allowed my attention to focus on direction. But the agent slops fast, and speed brings errors. I will disguise found failings as ‘exercises for the reader’. Every line still has to get through the same gates. Although some old practices are changing, the code-build-test-fix-deploy cycle survives.

The tooling removes entire classes of possible errors, and can catch most of the rest, but there’s no replacement for a person’s discernment. All the green check means is that a test passed. We’ll see later in the series that the spec can be correct, and tests can pass, and the game isn’t behaving as intended anyway.

Installing dox-populi

Download the dox-populi repo and follow the instructions in README.md.

Klanker Kontext

I cloned several repos and fed them to the agent during the process of building this project. You should do the same.

The Screeps server

backend-local Contains an HTTP server accessed by clients and a CLI server for administration.

driver A link between the environment-independent engine (that is shared for the official server, standalone server, and in-browser simulation) and the immediate environment that hosts the game engine.

render This library is based on PixiJS and contains the renderer engine used in the Screeps game.

tutorial scripts The original tutorial scripts.

typed-screeps Strong TypeScript declarations for the game Screeps: World.

paradox A language for domain specification.

Install and Run

Clone the repo and follow the instructions in README.md.