Skip to content

The realization ladder — one workflow, four rungs

Audience: developer who has written a CONTRACT and now wants an implementation for it — synthesized, generated, or hand-written.\ Normative source: the Realization Ladder ADR owns the decisions; this document explains them and does not restate their rules.\ Language Reference: CONTRACT, ASSURANCE, BY.\ Related: Synthesis · EXTERN trust model.

The problem the ladder solves

You declare what an output must satisfy. Someone — or something — must produce an implementation, and zqel must be convinced it is correct. There are several ways to produce that implementation, and they differ enormously in how much they cost you and how much trust they demand.

Without a common structure, each way becomes its own workflow with its own syntax, its own artifacts and its own idea of what "accepted" means. The ladder exists to prevent exactly that: one contract, one request, one feedback vocabulary, one acceptance decision — four ways to arrive at a candidate.

A rung is not something you write in a source file. Rungs are states of a workflow. The contract you declare is identical on every rung; what changes is who produces the candidate and what evidence accompanies it.

The four rungs

flowchart TD
    C(["CONTRACT"])
    C --> R1["rung 1 — internal synthesis"]
    C --> R2["rung 2 — a language model writes zqel"]
    C --> R3["rung 3 — a language model writes free code + evidence,<br/>bound to a model"]
    C --> R4["rung 4 — the developer writes artifact + evidence"]

    R1 -- "search bound exhausted" --> ART
    R2 -- "ProofFeedback" --> ART
    R3 --> ART
    R4 --> ART

    ART["the <b>same</b> registered EXTERN artifact<br/>+ BY (explicit consent)"]
    ART --> ACC(["accepted realization"])

Rungs 3 and 4 are one semantics, not two. They produce the same registered artifact and differ only in authorship. Trust follows the evidence, never the rung number — a hand-written artifact enjoys no privilege over a generated one, and a generated one carries no stigma.

Rung 1 — internal synthesis

The compiler searches for an implementation that satisfies the contract, within a static bound (AST nodes, expression depth, operator count). Every candidate it finds is proved before it is accepted, so a successful synthesis needs no external trust at all.

The bound is the point. A search without a limit would turn compilation into an open-ended question; a search with a limit gives a definite answer in finite time — either an implementation, or synthesis-bound-exhausted.

Reading the exhaustion correctly matters. It says this search did not find an implementation within this bound. It does not say the contract is unsatisfiable, and it does not say no implementation exists. It is the ladder's signal to climb, nothing more.

Rung 2 — a language model writes zqel

The contract goes to a model as a typed request; the model answers with a zqel candidate. The candidate is then compiled and proved exactly like hand-written zqel — no shortcut, no special status.

This rung costs little trust: the answer is in the language, so the ordinary proof machinery applies unchanged. What the model buys you is search, not authority.

Rung 3 — a language model writes free code plus evidence

Sometimes the implementation cannot be expressed in zqel's synthesizable subset, or the numerics demand a specific floating-point form. Then the model writes Rust or ST directly and supplies evidence.

This is where the ladder becomes dangerous without care, and where its soundness is decided. A model can hand you code A together with a perfectly correct proof about expression B. Each artifact is plausible; together they are worthless. Rung 3 therefore exists only as a binding chain:

  1. the artifact is translated into a canonical machine model — or checked against one;
  2. a checker proves the artifact implements exactly that model;
  3. the numerical proof addresses exactly that bound model;
  4. contract, artifact, model, recipe and evidence digests are sealed together.

Every link is mechanical. The chain, not the rung, is what makes generated code acceptable.

Rung 4 — the developer writes the artifact

Identical to rung 3 in every respect except authorship. The same registration, the same binding chain, the same warrants. A developer is not trusted more than a model; both are checked the same way.

What every rung shares

One request. The contract is the task. The typed request contains the block, its contract clauses, transition clauses, assurance policy and the input/output signature — and a task_digest that identifies the task independently of any realization. Switching from one rung to another does not change it.

One feedback vocabulary. Whatever fails, it is reported in the same closed union, so the next attempt — on any rung — is guided by the same language:

Variant Meaning
ConcreteCounterexample a model or trace violating an obligation
UnprovedObligation a goal that could not be discharged (with the best bound proved so far, if any)
InvalidCandidate syntax, type, or forbidden-surface refusal
RequirementViolation proof succeeded, but the proved bound exceeds the declared threshold
UnsupportedCapability the rung cannot express the construct
ToolFailure timeout, crash, unknown, version mismatch

The distinction between UnprovedObligation and RequirementViolation is deliberate: the first says we could not prove it, the second says we proved it and the answer is not good enough. Confusing them would hide an engineering decision behind a proof failure.

One acceptance decision. Climbing a rung means accepting a different kind of evidence, and that is a decision a person makes, not a fallback the tool performs silently. Registering an EXTERN artifact requires explicit consent, recorded in the acceptance record.

How a candidate is actually requested

Rungs 2 and 3 need someone to write the candidate, and zqel can ask a language model for it — but it is worth being precise about what is automated today, because the surface is not yet uniform.

zqel guided --agent codex|claude --out <dir> is the automated path. It renders the request into a prompt, runs the agent's CLI as a subprocess with a JSON output schema, validates the answer against that schema, materializes the candidate and drives the proof chain. What it automates is the untrusted proposal — not acceptance: proof replay and the acceptance record stay separate steps, and a candidate that fails its proof is discarded no matter who produced it.

zqel realize --request-only --json is the uniform entry into the ladder, but today it only builds the typed request. It does not yet reach the agent path above. Anyone using it therefore transports the request to a model by hand — which works, and the proof chain is unaffected, but it means the automated acquisition is not exercised. Closing that gap (zqel realize --agent … as the canonical end-to-end entry, with guided kept as a compatible adapter) is tracked as an open finding.

Agents are opt-in in both cases. CI never calls one — see below.

Where the candidate comes from does not matter

A candidate is untrusted input, exactly like an artifact from a registry. This is why the pipeline can run in continuous integration without any model service: CI checks frozen candidates with local tools (Z3, Gappa, CBMC, matiec). The generating step belongs to a developer tool, never to the gate that decides acceptance.

Accepted candidates are cached under the declaration — comments and formatting do not invalidate an accepted result, but a changed contract does.

What the ladder does not promise

  • It does not promise that a rung succeeds. Rung 1 may exhaust its bound; rung 2 may return an invalid candidate; rung 3 may fail its binding chain.
  • It does not promise that climbing is automatic. Offering the next rung is a convenience; consenting to a stronger trust assumption is not.
  • It does not turn a rung into syntax. There is no keyword for "rung 3"; there is a contract, and there is an accepted realization.

Worked signal: PumpBank

The PumpBank example in the how-to guide selects which of three pumps run, from a demand, per-pump health and per-pump operating hours. Its contract is relational — several RULEs that together pin the output — and rung 1 deterministically answers synthesis-bound-exhausted on it.

That is the ladder working, not failing. The bounded search gives a definite, reproducible answer, and the workflow continues on rung 2 with the same contract and the same request. The interesting engineering question is not "why did synthesis not find it" but "which rung is the cheapest one that supplies acceptable evidence".

A note on reproducibility. For a time this very example answered inconsistently — sometimes synthesized, sometimes exhausted, on identical bytes. The cause was that counterexamples were not chosen canonically, so the example set the search learned from depended on process state. A statement about a rung is only worth documenting once it is reproducible; the selection is canonical now, and the answer above is stable.