What is Overplane?

Bottom line up front

Overplane runs AI coding agents inside locked-down local containers to turn Markdown specs into code, and cross-checks the specs with the Z3 SMT solver before generating anything. The solver checks a machine-made formalization, not your intent. Use it for sandboxed, repeatable, consistency-checked code generation. Do not adopt it expecting proofs of program correctness.

Background

Coding agents are effective but hard to constrain and audit. Run directly on a host with full access, their changes are difficult to reproduce, attribute, or bound.

What it does

• One local binary. Each spec passes through a fixed pipeline: raise (an agent lifts the spec into a formal model under dirs.ir), verify (Z3 checks each spec's model, then a merged model of all specs; a contradiction fails the build), codegen (an agent generates code against the checked model). The typical sequence is overplane init, then overplane sandbox build, then overplane spec new, then overplane build.
• The agent works in a per-project container. It reads the workspace read-only and writes to a separate output mount. Results land atomically in the code directory.
• Three supported agents: Claude Code, Codex, OpenCode. You supply the API keys. The agents install inside the container only, never on your machine.
• Container images are content-hashed, outputs are content-addressed, and usage and cost are reported uniformly across agents.

Limitations

• "Verified" means an agent's heuristic translation of your prose, checked exactly by Z3. The solver catches contradictions in the formalization; it cannot catch a faithful formalization of the wrong idea, and it checks the specs, not the generated code. It raises confidence. It does not guarantee correctness or completeness.
• Verification scope is consistency and scenario reachability across specs. It is not a proof of program correctness.
• Output quality tracks the chosen agent on a given day. Review generated diffs before accepting them.

Alternatives

• Interactive development: Claude Code, Codex, or Cursor, used directly.
• Certified correctness now: TLA+, Dafny, or Lean, at substantially higher cost.
• Spec-driven peers: GitHub Spec Kit and AWS Kiro, without equivalent container isolation.

Recommendation

Adopt where unattended, repeatable, sandboxed code generation with automated spec consistency checks is worth having. Your judgment stays in the loop: the specs' scope and wording, the choice of agent (per run via --agent, per spec via the agent_config frontmatter field), and the sandbox's contents (overplane.yaml: base image, packages, installed agents, environment) remain yours to decide.