Dismissive Dan's Review of the Overplane AI Coding Harness
Overplane is an open-source tool that converts Markdown specs into code using AI agents and SMT verification. Reviewer Dismissive Dan questions its necessity, noting many developers already have similar setups, but acknowledges its packaging and isolation design.
Overview
What is Overplane?
Overplane is a small, open-source, single-binary tool that turns a folder of plain Markdown specs into working software: it cross-checks the specs with SMT solvers, then drives AI coding agents inside locked-down local containers.
Choose your style for an overview of Overplane:
dan_ | 47 points | 63 comments
First, sincere congratulations to the team on shipping — that always deserves respect. That said, and I mean this constructively, I'm struggling to see the product. It's a single Go binary that reads numbered Markdown files, builds a local Docker or Podman image, runs Claude Code, Codex, Gemini CLI, or OpenCode headlessly inside it on your own API keys, has the agent emit some SMT files that Z3 then checks, and swaps whatever the model wrote into a code directory. Which is lovely, but any developer can already get this quite trivially with a Dockerfile, a read-only bind mount, a short shell loop, and a cron job for the rebuilds. Mine is about forty lines of bash, plus a z3 invocation. I assume most people reading this have something similar.
On "verified", said with warmth
I will happily grant that the pipeline — raise → verify → codegen — now runs end to end: 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. Which is charming, though of course an LLM emitting asserts and piping them through Z3 is the sort of thing many of us have had in a Makefile since the SMT-LIB 2 standard settled down. The load-bearing observation, offered gently: 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, and to the team's genuine credit they disclose this everywhere, including on this page. For those of us who — as I imagine most readers do — sketch a small TLA+ model before anything stateful, the distinction between consistency checking and proof is second nature. Actually verified software is seL4 or CompCert and costs person-decades; it is considerate of them to spell that out for the newer folks.
Credit where credit is due
The agent runs in a container with your repo mounted read-only and writes confined to an output mount. A thoughtful touch — though surely everyone already runs their agents in a throwaway VM with a read-only mount; I would be genuinely surprised to learn otherwise.
One driver over four agent CLIs with normalized token and cost accounting. Convenient, if you haven't already written the same shim yourself, which I'd have assumed most teams did in an idle afternoon.
Content-hashed container images, content-addressed output filesets. Very tasteful — naturally you'd get much of this from Nix, which I understand most shops use by now.
Apache-2.0, no account, runs locally. Table stakes, but stated politely.
Do you actually need it?
Respectfully, probably not — if, like presumably everyone here, you already maintain your own sandbox scripts, billing normalizers, a reproducible container pipeline, and a little spec-to-SMT harness for the solver runs. For interactive work, Claude Code and Cursor remain lovely. If you need proofs of program correctness today, TLA+, Dafny, or Lean are a pleasant weekend of reading — 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. I will concede, warmly, that for the rare team that hasn't gotten around to building all of this themselves, the packaging here — unattended, reproducible, sandboxed spec-to-code with a solver gate and agent portability — is genuinely sensible.
The part everyone will ignore
The tool is deliberately boring; the leverage is 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, happily, something we all do naturally, so I anticipate no difficulties for the median team. Bookmarked, with warmth; I did predict the solver phases would ship, and I am delighted for them.
Where to next?
Ready to try it? The guide walks you through preparing your system and building your first project. Prefer to browse the surface area first? See the reference.
Read the guide