Guide

Advanced Topics

Deeper tooling for verification, IR, sandboxes, and power-user workflows.

Spec Verification

Every overplane build checks your specs for logical contradictions before generating any code. The check is real: the claims in each spec are lifted into SMT-LIB formulas during the raise phase, and the Z3 theorem prover then decides whether those formulas can all be true at once. If they cannot, the build stops with exit code 9 and tells you which claims conflict.

This page walks through what verification does and does not prove, using a real spec from the overproxy example.

What gets verified (and what doesn't)

Verification answers one question: are the requirements in your specs mutually consistent? It is a satisfiability check over the formal claims extracted from the spec text, per spec and across all specs together. It does not prove that the generated code implements the spec; that gap is covered separately, by IR-derived property tests and model checking at the code level (see Codegen with IR and the Formal Verification FAQ for an honest assessment).

Not every sentence in a spec becomes a formula. Claims that are naturally quantitative or relational (counts, decision tables, state invariants) are encoded; claims about parsing quality, visual polish, or timing are marked non_smt in the IR and skipped, with the skip recorded so nothing silently disappears.

From spec prose to formal claims

Here is the mapping in action. The overproxy spec says, in plain English:

* Config file format, one directive per line ('#' comments allowed):
  - listen <addr:port> : the address to bind (exactly one).
  - route <host> <upstream-addr:port> : proxy requests whose Host header
    matches <host> to the upstream (one or more).

* Requests for unknown hosts get a clean built-in 404 page; unreachable
  upstreams get a built-in 502 page.

The raise phase turns each checkable claim into an IR node with an id, a kind, and a rationale that quotes the spec sentence it came from (ir/001-proxy/ir.yaml):

- id: listen_directive_count
  kind: constraint
  description: Number of `listen` directives parsed from the config file.
  type: Int
  bound: "= 1"
  rationale: "Spec: 'the address to bind (exactly one)'."

- id: routing_decision
  kind: rule
  rule_kind: decision_table
  description: >
    Deterministic mapping from (host_match, upstream_reachability) to the
    externally observable proxy_outcome for one request.
  table:
    - when: { host_match: Unmatched }
      then: { proxy_outcome: NotFoundHost }
    - when: { host_match: Matched, upstream_reachability: Unreachable }
      then: { proxy_outcome: BadGateway }
    - when: { host_match: Matched, upstream_reachability: Reachable }
      then: { proxy_outcome: Forwarded }

Each SMT-checkable node then becomes a named assertion in consistency.smt2. The names matter: when Z3 finds a contradiction, it reports an unsat core, the minimal set of named assertions that conflict, and the names trace straight back to spec ids and IR nodes:

(set-logic ALL)
(set-option :produce-unsat-cores true)

(declare-datatypes ((HostMatch 0)) (((Matched) (Unmatched))))
(declare-datatypes ((ProxyOutcome 0)) (((Forwarded) (NotFoundHost) (BadGateway))))
(declare-const listen_directive_count Int)
(declare-fun decide (HostMatch UpstreamReachability) ProxyOutcome)

(assert (! (= listen_directive_count 1)
        :named s0001_listen_directive_count__exactly_one))
(assert (! (forall ((u UpstreamReachability)) (= (decide Unmatched u) NotFoundHost))
        :named s0001_routing_decision__row_1))
(assert (! (= (decide Matched Unreachable) BadGateway)
        :named s0001_routing_decision__row_2))

(check-sat)

Per-spec checks and the merged model

Verification runs Z3 twice over your IR, entirely inside the project sandbox with the IR mounted read-only:

• Per spec: each spec's consistency.smt2 is checked on its own, together with any scenario-*.smt2 reachability probes the raise phase emitted. sat means the spec's requirements can coexist; unsat means the spec contradicts itself.
• Merged: all specs' assertions are combined into ir/merged/merged-consistency.smt2 (declarations deduplicated, per-file check-sat and advisory blocks dropped) and checked as one model. This is where cross-spec conflicts surface: spec #0002 demanding something spec #0005 forbids.

Verification results are cached by content: if the SMT inputs and sandbox image have not changed, the cached verdict is reused and Z3 does not run (see FileSet for how content-hashed caching works).

Reading a failure

A failed verification stops the build with exit code 9 before any code is generated. The verdict is categorized so you know where to look:

• C1: a single spec contradicts itself.
• C2: two or more specs conflict (the unsat core names assertions from more than one spec id).
• C5: a scenario probe expected to be reachable is not.
• C6: Z3 hit a syntax or runtime error in the SMT files; this is reported as a warning, not a spec contradiction.

On failure, Overplane can drive an agent with the verify/explain prompt to translate the unsat core back into plain language, quoting the conflicting spec sentences verbatim so you can fix the requirement rather than decode SMT output. Fix the spec, run overplane build again, and only the affected work re-runs.