What is Overplane?

dan_ | 47 points | 63 comments

Congratulations to the team on shipping. I mean that; shipping is work. My confusion is that this exists as a product at all. I had all the pieces working by '97, '98 at the latest: a chroot jail, a Makefile, and a script that read the spec document and did the rest. The vocabulary has changed since then; the shape has not. As far as I can tell, this is a single Go binary that reads numbered Markdown files, builds a local Docker or Podman image, runs Claude Code, Codex, or OpenCode headlessly inside it on your own API keys, has the agent emit SMT files that Z3 then checks, and swaps whatever the model wrote into a code directory. Mine is about forty lines of bash, plus a z3 invocation. I assume most people reading this have something similar.

On "verified"

The pipeline (raise → verify → codegen) does run end to end; I checked, since release notes are aspirational as a rule: an agent lifts each spec into IR and SMT-LIB, Z3 checks each spec's model and a merged model of all of them, and a contradiction fails the build. This is roughly the Makefile several of us have had since the SMT-LIB 2 standard settled down. The observation everything rests on: the pipeline is heuristic at both ends. A solver faithfully checking the wrong formalization of your prose is a very efficient way to feel confident. They disclose this everywhere, including on this page, which is more candor than the genre usually manages. Anyone who sketches a small TLA+ model before anything stateful, as I assumed we all still did, knows the difference between consistency checking and proof. Actually verified software is seL4 or CompCert and costs person-decades; someone should tell the newer folks, and to be fair, they do.

Credit, such as it is

• The agent runs in a container with your repo mounted read-only and writes confined to an output mount. Correct, and also the obvious design; I would have been more surprised by anything else.
• One driver over the three agent CLIs with normalized token and cost accounting. Useful, in the way the shim you wrote yourself in an idle afternoon is useful, except now somebody else maintains it.
• Content-hashed container images, content-addressed output filesets. This is Nix with fewer parentheses. I mean that as a compliment, mostly.
• Apache-2.0, no account, runs locally. As it should be. I remember when this went without saying.

Do you actually need it?

Probably not, if you already maintain your own sandbox scripts, billing normalizers, a reproducible container pipeline, and a little spec-to-SMT harness for the solver runs, which I had understood to be the baseline. For interactive work, Claude Code and Cursor exist. If you need proofs of program correctness today, that is TLA+, Dafny, or Lean and a quiet weekend; what ships here checks spec consistency, not the code. GitHub Spec Kit and AWS Kiro sit in the same spec-driven aisle without the container isolation. If, somehow, you have not built all of this yourself over the past thirty years, the packaging (unattended, reproducible, sandboxed spec-to-code with a solver gate and agent portability) is competently done, which is more than one usually gets, and it will save you the trouble. There are worse fates than being saved the trouble.

The part everyone will skip

The tool is deliberately boring; the decisions that matter are in your specs (granularity, precision, how much latitude you leave the model), in which agent you pin per run ( --agent) or per spec (agent_config in the frontmatter), and in the sandbox you compose in overplane.yaml (base image, extra packages, which agents, env passthrough). Writing specifications precise enough for a solver to check is a skill. I picked it up in '98 and assumed it had caught on. Bookmarked. I did predict the solver phases would ship, for whatever that is worth.