Guide

Advanced Topics

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

Codegen with IR

The final build phase, codegen, drives a coding agent to generate your software. The agent does not work from the spec alone: the verified IR is mounted read-only in its sandbox, and the prompt tells the agent to treat it as authoritative. This page shows what the agent actually sees, and how the rustdis example pushes the idea further by turning IR nodes into an executable property-test suite.

What the codegen agent sees

Each spec's codegen run gets a sandbox with the working directory at /code (writable), the project at /project and specs at /specs (read-only), and the IR at /ir (read-only). The standard prompt template (codegen/auto) sets the ground rules, and a per-spec preamble points the agent at the checked model:

Your current working directory is /code and it is writable: write all
generated files under /code.

The project repository is mounted read-only at /project, specs at /specs,
and IR at /ir. Read them for context but never attempt to modify them.

Formal constraints for this spec are under /ir/001-proxy/ (ir.yaml and
consistency.smt2). Treat them as authoritative.

Specs build on each other: spec #0002's agent starts from the code that #0001 produced, staged in a cache directory and snapshotted as a file set between steps. On success, the final snapshot is synced cleanly to dirs.code. You can inspect or swap the prompt with overplane prompt show codegen/auto and overplane build --prompt <collection/name>.

Case study: IR-derived property tests

Because the IR is a machine-readable inventory of every claim in your specs, a later spec can consume it. rustdis (a Redis-compatible server written against seven specs) dedicates spec #0006 to exactly this: it instructs the agent to walk the IR of specs #0001 through #0005 and derive a proptest suite from it. The spec is itself a prompt, and its key fragments show the technique:

Turn the formal IR that Overplane raised from specs #0001-#0005 into an
executable property-based test suite. The IR directories are mounted
read-only at /ir/<spec-file>/ (ir.yaml, consistency.smt2); treat them
as the authoritative source of properties. Do not invent properties that
have no IR node, and do not skip IR nodes that are runtime-checkable.

* Traceability is the point. Create tests/ir_properties.rs where every
  property test is named prop_<spec>_<ir_node_id> (e.g.
  prop_0003_no_resurrection) and carries a doc comment quoting the IR
  node's description and assertion.

* Every runtime-checkable IR node id from specs #0001-#0005 appears either
  in tests/ir_properties.rs or in the VERIFICATION.md SKIPPED table:
  no third bucket.

The generated suite delivers that traceability. Here is the property derived from the #0003 IR node no_resurrection, whose IR description reads "Once a key is unobservable because now >= deadline, it stays unobservable for every later monotonic instant":

/// IR #0003 `no_resurrection` (invariant): "Once a key is unobservable
/// because now >= deadline, it stays unobservable for every later monotonic
/// instant ... No read may observe the old value after expiry."
#[test]
fn prop_0003_no_resurrection(
    ttl in 1u64..10_000,
    advances in prop::collection::vec(1u64..5_000, 1..8),
) {
    let mut s = manual_store(); // virtual clock: expiry is deterministic
    real_reply(&mut s, &[b"SET".to_vec(), b"k".to_vec(), b"v".to_vec(),
                         b"PX".to_vec(), ttl.to_string().into_bytes()]);
    s.advance(Duration::from_millis(ttl)); // reach the deadline
    for a in advances {
        let got = real_reply(&mut s, &[b"GET".to_vec(), b"k".to_vec()]);
        prop_assert_eq!(&got, &RespValue::NullBulk,
                        "expired key must never resurrect");
        s.advance(Duration::from_millis(a));
    }
}

A second example, from the #0004 collections IR, checks the invariant that an empty collection is never observable (draining a list or set deletes the key):

/// IR #0004 `empty_never_observable` (invariant): "An empty collection is
/// never observable ... Deleting the last element deletes the key."
#[test]
fn prop_0004_empty_never_observable(elems in prop::collection::vec(arb_val(), 1..6)) {
    let mut s = Storage::new();
    let mut push = vec![b"RPUSH".to_vec(), b"l".to_vec()];
    push.extend(elems.iter().cloned());
    real_reply(&mut s, &push);
    real_reply(&mut s, &[b"LPOP".to_vec(), b"l".to_vec(),
                         (elems.len() as i64).to_string().into_bytes()]);
    prop_assert_eq!(real_reply(&mut s, &[b"EXISTS".to_vec(), b"l".to_vec()]),
                    RespValue::Integer(0));
    prop_assert_eq!(real_reply(&mut s, &[b"TYPE".to_vec(), b"l".to_vec()]),
                    RespValue::SimpleString("none".to_string()));
}

Beyond single-node properties, the suite includes model-based testing: random command sequences run against both the real store and a naive BTreeMap reference model, asserting identical replies. The result is a verification chain with three links, each mechanical and auditable: spec sentence to IR node (the rationale field), IR node to SMT assertion (the :named labels), and IR node to property test (the prop_<spec>_<node> naming convention).

Caching and cost

Codegen steps are cached like raise steps, with one addition: the cache key includes a content hash of the accumulated output from all prior specs. Edit spec #0003 and rebuild, and specs #0001 and #0002 restore instantly from cache while #0003 onward re-run. Failed agent runs are never cached, so a retry always re-executes. Recorded alongside each cached step are the original run's token usage and cost, which is how the example walkthroughs report their build spend without re-running anything.