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 assert
s 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.