What is Overplane?

Reference Manual

1. Introduction

Overplane is a single-file program, written in Go, that converts a directory of numbered Markdown specification files ("specs") into program source code. It does this by supervising an AI coding agent inside a locally built container. The tool itself runs entirely on your machine; the coding agent contacts its remote service using your own API credentials.

2. Before you begin

Make sure you have:

• Linux, macOS, or Windows with WSL2.
• Docker or Podman.
• An API key for at least one supported agent: Claude Code, Codex, or OpenCode. You do not install the agents yourself; Overplane installs them inside the container.

No account is required and there is nothing to purchase. Overplane is open source under the Apache-2.0 license.

3. Basic operation

1. Run overplane init to create the project configuration file, overplane.yaml.
2. Run overplane sandbox build to build the project's container image. The image is tagged with a content hash and is rebuilt only when its configuration changes.
3. Run overplane spec new to create the next numbered spec file under specs.
4. Run overplane build (dev: overplane build -p codegen -n 1). Each spec passes through three phases in fixed order. Raise drives an agent to translate the spec into an intermediate representation and SMT-LIB files under dirs.ir. Verify (validate is accepted as an alias) runs the Z3 solver on each spec's formal model and on a merged model of all specs together; a contradiction stops the build with exit code 9. Codegen drives the agent to generate code, with the checked model mounted for reference; output lands under dirs.code from overplane.yaml. The container sees your repository read-only; the agent writes to a staging area reconciled on success via content-addressable FileSet sync.

Note: all three phases are operational. Raise and codegen consume agent tokens; verify runs Z3 locally inside the sandbox and consumes tokens only when explaining a failure (suppress with --no-explain).

4. About the word "verified"

"Verified" refers to the following procedure: the spec is translated (heuristically, by an AI agent) into a formal representation; that representation is checked mechanically with the Z3 SMT solver; code is then generated, again heuristically, from the checked representation. The middle step is exact, but it checks the machine's guess at what you meant, not what you meant. The procedure can raise your confidence in the output. It cannot, and will not, establish that the output is correct or complete.

5. Is this the right tool?

Use Overplane for unattended, repeatable generation of code from written specs, with agent isolation, reproducible images, content-addressed outputs, and uniform usage and cost accounting across agents.

Do not use it for interactive editing (Claude Code or Cursor are better suited) or where formally certified software is required, which calls for a dedicated proof assistant such as TLA+, Dafny, or Lean. GitHub Spec Kit and AWS Kiro are comparable spec-driven tools; neither isolates agents in containers in the same way.

6. Making it yours

Three areas are deliberately left to you. First, the specs: their granularity, numbering, prose style, and how much design latitude they leave to the agent. Second, agent selection: name agent configurations in overplane.yaml, pick one per run with --agent, or pin one per spec with the agent_config frontmatter field. Third, the sandbox: overplane.yaml controls the base image, additional OS packages, which agents are installed, and which environment variables pass through.