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