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:

overplane, explained by grug

grug brain developer here. big words make grug tired, so grug explain simple.

you have idea for software. you write idea in plain file called spec — numbered Markdown, lives in git, no magic format. you run overplane build. tool wakes up AI coding agent — Claude Code, Codex, Gemini CLI, or OpenCode, grug picks — and tells it to read spec and write code. agent works inside container, which is sealed box: box can read grug's repo but cannot touch grug's real machine. before code gets written, tool also turn spec into math and make solver check it — grug explain below. when box finishes, new code lands in code folder for grug to read. that is whole loop.

first time only: overplane init make config, overplane sandbox build make box, overplane spec new make next numbered spec file. then overplane build forever.

what "verified" mean (grug not lie)

pipeline has three steps, and all three run for real now — raise (agent turns spec into math: IR file plus SMT formulas), verify (Z3 solver checks the math — each spec alone, then all specs together; if specs contradict, build stops), codegen (agent writes code with the checked math mounted next to it). grug honest twice:

solver part is real and mean. it catch spec that argue with itself, spec that argue with other spec, and scenario where bad thing reachable. build refuse to continue until grug fix spec. this good.
but every arrow still machine guess: spec-to-math is guess, math-check only as good as the math, code-from-math is guess. "verified" mean more confidence, never mean 100% correct. anyone who say otherwise is selling grug complexity demon.

good things grug likes

agent in box cannot delete grug's home directory. this alone worth a lot. workspace mounted read-only; agent writes only to output.
one tool, many agents. grug bring own API keys, grug not married to vendor. token cost reported same way for all of them.
builds repeatable: container image tagged by content hash, outputs content-addressed. same spec, same box, same answer shape.
one small binary. open source. no account. no rug-pull.

when grug should not use it

grug want to chat with agent and poke code by hand? use Claude Code or Cursor directly. is fine. good tools. no shame.
grug need real mathematical proof today? use real formal tools — TLA+, Dafny, Lean — and much patience. overplane solver check spec consistency, not full program correctness.
grug want spec-driven tool from big vendor? GitHub Spec Kit and AWS Kiro exist. grug looked at them. they not put agent in box the same way, but they real.

where grug gets to be clever

spec is just Markdown, so grug decides everything that matters: how big each spec is, what words to use, how much room to leave agent for own ideas. grug picks agent per run ( --agent flag) or per spec (agent_config in spec frontmatter, pointing at named agent in overplane.yaml). grug also decides what goes in box — overplane.yaml picks base image, extra packages, which agents get installed, which env vars pass through. tool stay simple on purpose so grug's project can be the clever one.

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