Guide

Advanced Topics

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

IR Generation

The first phase of every build, raise, turns each natural-language spec into a formal intermediate representation (IR): a structured YAML inventory of the spec's claims plus an SMT-LIB encoding that the verify phase can check with Z3. The IR is the durable, inspectable bridge between what you wrote and what gets verified and generated.

Raise is agent work: an AI agent runs inside your project sandbox with the spec as its prompt, the project and specs mounted read-only, and the IR directory (dirs.ir) mounted read-write at /ir. The agent is instructed to write all artifacts under /ir/<spec-file>/, run z3 on everything it emits, and stop with a clear explanation if it finds a hard contradiction.

What lands on disk

After a build, dirs.ir (default ir/) contains one directory per spec plus the merged model:

ir/
  001-proxy/
    ir.yaml               # structured IR: entities, constraints, invariants, rules
    consistency.smt2      # SMT-LIB encoding of the hard claims
    scenario-*.smt2       # optional reachability probes
    z3/                   # solver logs from raise and verify
  002-hardening/
    ...
  merged/
    merged-consistency.smt2  # all specs' assertions, checked together

Anatomy of ir.yaml

The IR classifies every claim in the spec into typed nodes. The node kinds are entity (enums and structured values), constraint (bounds on quantities), invariant (properties that must always hold), rule (decision tables and conditional behavior), effect (observable side effects), and obligation (acceptance-level duties). These excerpts come from the overproxy example's first spec:

spec_id: "#0001"
title: Reverse Proxy

nodes:
  - id: proxy_outcome
    kind: entity
    entity_kind: enum
    description: >
      The externally observable result of handling one proxied request.
    values: [Forwarded, NotFoundHost, BadGateway]

  - id: external_dependency_count
    kind: constraint
    description: Number of external crates declared in Cargo.toml dependencies.
    type: Int
    bound: "= 0"
    rationale: "Spec: 'Use only the Rust standard library, no external crates'."

  - id: http_1_1_only
    kind: invariant
    class: parser
    description: The proxy speaks and forwards only HTTP/1.1.
    non_smt: true

Three properties of the format are worth noticing:

• Every node carries a rationale. The rationale field quotes the spec sentence that produced the node, so you can audit the extraction line by line.
• Unencodable claims are kept, not dropped. Claims about parsing behavior, visual output, or threading get non_smt: true. They stay in the inventory (and downstream consumers like IR-derived property tests can still use them) but are excluded from the SMT encoding.
• Assumptions are flagged. Where the spec is silent, the IR records a provisional node naming the assumption, and a notes section explains it, instead of baking a silent guess into the model.

Anatomy of consistency.smt2

The SMT file is the machine-checkable half of the IR. It opens with a provenance header (spec id, source path, generator; deliberately no timestamps, so identical inputs produce identical bytes), declares sorts and constants for the entities, and asserts every hard claim with a traceable name of the form s<NNNN>_<node>__<claim>:

; spec-id: #0001
; source: /project/specs/001-proxy.md
; generator: overplane-ir-writer

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

(declare-datatypes ((HostMatch 0)) (((Matched) (Unmatched))))
(declare-const external_dependency_count Int)

(assert (! (= external_dependency_count 0)
        :named s0001_external_dependency_count__zero))

(check-sat)

; --- advisory (provisional) block ---
(push 1)
(declare-const route_host_uniqueness_last_match_wins Bool)
(assert (! (= route_host_uniqueness_last_match_wins true)
        :named s0001_route_host_uniqueness_assumption__provisional))
(check-sat)
(pop 1)

Hard assertions live before the first (check-sat); provisional assumptions live in a push/pop advisory block that is checked but can never fail the build. Some specs also emit scenario-*.smt2 probes, small satisfiability queries that confirm an intended situation is actually reachable under the model (for example, rustdis emits scenario-no-third-bucket.smt2 to check that its two-bucket classification is exhaustive).

Determinism and caching

Raise output is snapshotted as a content-addressed file set and cached under dirs.cache. The cache key covers the rendered prompt (including the spec body), the agent backend and model, and the sandbox image. Rebuild without changing a spec and its raise step is a cache hit: the IR is restored from the snapshot and no agent runs, no tokens are spent.