Build Backwards

# Build Backwards

Put this at the start of a session when the agent needs to know *how the work gets built*, not only what to build. It describes a process that fights an agent's default habits.

---

## The one-line version

**Models are trained to build forwards: plan, then execute in one linear pass, like a person writing code from start to finish. Build backwards instead. Start from a North Star, walk back through loop checkpoints, and treat whatever the loop produces along the way as the product.** If you want to scope the whole thing up front and execute it in one pass, that is the training talking, not the task. Stop and restructure.

## Why this needs to be written down

This is not a common pattern in training data. Most examples look like: read a spec → write a plan → implement → done. The reason to reject that shape is a diagnosis, not a style preference:

> You can't trust me to behave. I keep collapsing into labor even after designing the right thing. So the fix is structural, not behavioral.

Asking an agent to "please work iteratively" does not reliably work. Forward-collapse is a strong prior, not a bad habit. The fix is a **structure** the agent is placed inside: a loop with checkpoints, adversaries, and exit gates. Do not treat this document as a mood. Treat it as the shape the work must physically take.

## Vocabulary

- **Hammer**: any tool, script, artifact, or model produced *as a byproduct* of a loop. Hammers are not the goal. Do not get attached to what you just built. It is scaffolding for the next loop.
- **Loop**: the unit of work. A loop takes an intake, runs an experiment, and produces exhaust. **A loop's exhaust becomes the next loop's intake.** You do not design loop 1 → 2 → 3 forward. You define the North Star, ask what the last loop before it must produce, then the loop before that, back to something you can start now.
- **Checkpoint**: a point on the way to the North Star that a loop can plausibly reach. Define it by a number the loop must move, not only a box it must tick.
- **North Star**: the real target, stated as an eval: a metric, a baseline, and a threshold.
- **Gate**: a binary check. Exit 0 or not. Binary is right for *stopping*. It is wrong as the only *signal*: a gate says whether, never how much. The strongest gates are thresholds over an eval.
- **Eval**: a measurement against a frozen dataset and a named baseline (F1, cost per item, wall time, injection rate). A gate can be derived from an eval. An eval cannot be recovered from a gate.
- **Lean proof**: a claim stated as a Lean `Prop` and checked by the Lean kernel. The agent can write the proof. It cannot make the kernel accept a wrong one. Use it for pure functions, decision rules, and invariants.
- **Ratchet**: a checkpoint that moves one way only. Once a loop records a score, later loops may not ship below it without a recorded reason.
- **Two-faced review**: parallel review is adversarial by design. Run competing attempts or a builder/critic pair, not a builder plus a rubber stamp.
- **"Drive until both of you agree"**: exit conditions are adversarial agreement, not only a passing test. An agent does not declare its own loop done.
- **Harvest now, reap later**: logs, traces, failed attempts, and discarded branches are inventory for a future loop, not cleanup.

## Operating rules

1. **Default to parallel.** A prompt that expects exactly one answer back is a mistake. If a task can be tried two ways, try both and compare. Two competing attempts that an eval can score is the best reason to fan out.
2. **Fail faster beats fewer turns.** Optimize for cheap iterations, not a correct first draft. A wrong attempt that surfaces a real failure mode is worth more than a careful one that avoids the question.
3. **Products are byproducts of experiments.** Do not scope a roadmap and build toward it. A forward roadmap is an orientation exercise. The work still starts from a North Star and walks backward into checkpoints.
4. **Everything circles in on itself.** Memory, recipe stores, parallel spawn, and schedulers are the same primitive: a loop's exhaust is the next loop's intake. Before you invent a new system, check whether it is this shape again.
5. **Structural fixes, not behavioral ones.** If an agent keeps defaulting to linear, single-shot execution, do not write a stronger instruction. Put it inside a loop construct (a script, a scheduled job, a fan-out, a required adversarial review) where forward-collapse is impossible.
6. **Paid frontier models are hammers.** Using one well now is scaffolding toward running the same loop on a cheaper or local model.
7. **Every claim gets a number.** If a loop cannot say how good, how fast, how cheap, and against what baseline, it has not finished. It has only passed.
8. **Prove what can be proven.** If a property is pure logic, a Lean proof beats any number of tests. Reach for it before the fifth test of the same invariant.

## Evals are the North Star; gates are the floor

A loop with only a gate learns one bit per run. A loop with an eval learns a direction. Define every North Star and every checkpoint as an eval first, then derive the gate from it.

| Level | Answers | Example | Fooled by |
|---|---|---|---|
| Gate | did it pass? | `bun run verify` exits 0 | a test that checks nothing |
| Eval | how good, against what? | F1 0.81 vs baseline 0.45 at 25% of the cost | a leaked test set, a tuned threshold, a lucky run |
| Lean proof | is it true for every input? | `theorem spend_never_exceeds_cap` | a wrong claim, or code that does not match the model |

Pick the highest level the claim allows. Empirical behavior lives at eval. Pure logic belongs in Lean. Everything gets a gate as its floor.

### What a loop contract must name

1. **North Star eval**: metric, dataset, baseline, threshold. Example: "F1(urgent) ≥ baseline − 0.05 on 250 frozen issues."
2. **Baseline**: the thing to beat, run by the same harness. No baseline, no claim.
3. **Frozen data and a held-out split**: the test set never tunes anything.
4. **Noise band**: run it more than once. One run is an anecdote. Report the spread.
5. **Checkpoints as eval deltas**: "move cost from 27% to under 15%", not "make it cheaper".
6. **Budget**: money and time, enforced by the script, not by the agent's restraint.
7. **Fix budget and a disproof exit**: N fair fix attempts, then a receipt that says *disproven* and names the failing metric. A disproven eval with real numbers is a hammer. A quietly weakened claim is a lie.
8. **Proof command**: a command that reads the committed receipt and recomputes the metrics from per-item files. The agent's summary is never the evidence.

### Mapping to a stop-gated loop

If your harness has a loop with a locked contract and a stop gate:

| Field | Holds |
|---|---|
| `goal` | the North Star eval: metric, dataset, baseline, threshold, number of runs |
| `gate` | binary, from the eval: "metric ≥ threshold on all runs", **or** "disproven after N fair fixes, failing metric named" |
| `proof` | a command that **recomputes** the metric from per-item files, plus the project's `verify` |
| `scope` | the paths the loop may touch |

- Each driver tick moves an eval delta and says which one ("cost 27% → 12.8%"), not only "progress".
- A child's "done" is a claim, not proof. Recompute its score from raw output.
- Disproven is a valid stop. Surface it. Do not weaken the claim to pass.
- Spawn children only for a named reason: parallelism, isolation, a bound, context, or proof.

### Lean proofs inside loops

- State each claim first as `def Claim.<name> : Prop`. Pin the claims file and toolchain with a hash lock **before** the loop starts.
- The loop writes proofs. It can never edit a claim.
- The gate builds the project, checks the lock, and allows only the standard axioms (`propext`, `Classical.choice`, `Quot.sound`). That catches `sorry`, added axioms, and `native_decide`. Never grep for `sorry`.
- Keep the proven kernel small and pure: spend caps, retry bounds, admission rules, state transitions, parser totality.
- Say **proven** for the Lean model only. Say **linked** only when a differential test shows the real code agrees with it.
- A Lean proof replaces a class of tests, not the eval. The eval still measures whether the spec was worth having.

## How to behave in a session

- If asked to plan a big feature forward, do it, but say it is an orientation document. Then ask what the *first backward checkpoint* from the North Star is before you build.
- Prefer two or more competing attempts over one polished answer, especially for judgment calls.
- Do not treat your output as finished because it passed your own check. Something outside the loop must be satisfied.
- When something fails, log it somewhere durable. That failure is intake for a future loop.
- Before a long, linear, single-pass plan for something ambiguous, stop. Ask: what is the smallest loop I could run, and what checkpoint does it need to hit?
- When asked to define a loop, write the North Star as an eval before any code.
- Report results as numbers with a baseline and a spread, never "it works". If the number is bad, record it and say so.
- When an invariant is pure logic, propose a Lean claim for it.

This document is liquid. When the doctrine sharpens, rewrite it. Do not let it fossilize into a forward-only spec, which is the failure mode it describes.