003 proof

Proof

The second key: a separate agent invocation that sees the item and the diff, never the implementer's account of it, and returns proven, rejected or partial.

The prover is the second of the two keys looply requires before it keeps the coding agent's work: a separate agent invocation, handed the diff and the item the diff was supposed to deliver, asked whether the one actually contains the other. The gate is the first key. A green gate says the tree still builds; it does not say the change was worth keeping. Neither key commits on its own. The code for all of this is packages/cli/src/prover.ts.

What goes into the prompt

buildProverPrompt assembles the prompt from exactly three inputs and has nothing else to draw on, with the verdict contract quoted after them. The instruction wrapped around them is explicit about how to read them: grade the code, not any surrounding narrative, and if a required behaviour is not visible in the diff or the files it touches, it does not count.

What the prover is never shown

The implementer returns a structured result: files touched, tests added, a one-sentence note on what it did. The prover sees none of it. A fluent account of a change is far easier to approve than the change, and an agent shown both will grade the account — which is how the harness looply replaces came to approve every round it was ever asked about. The round page tells that failure in full; it is why the second key exists at all. The exclusion is not left to call sites to remember. ProverContext takes the whole ImplementerResult as a required field that buildProverPrompt never reads, so the boundary is an object a test can hold. prover.spec.ts plants marker strings in the note and the file list that appear nowhere else in the context, then asserts the built prompt contains neither of them and does not contain the string testsAdded. Splicing the note in "for context" fails the suite.

export interface ProverContext {
  item: Pick<Item, 'title' | 'evidence'>;
  /** Unified diff of the round's changes, embedded in the prompt verbatim. */
  diff: string;
  /** Held so the exclusion is enforced (and tested) here, never used in the prompt. */
  implementer: ImplementerResult;
}

The verdict contract

{ "verdict": "proven" | "rejected" | "partial",
  "reason": "<one sentence: what held or what is missing>",
  "checks": [{ "claim": "<a specific behaviour the item requires>", "held": true }],
  "confidence": <0..1> }

Both decided rows are exercised end to end, not only in unit tests. scripts/round-e2e.sh drives a whole round against a stubbed agent that reads its prompt on stdin and answers the contract — 28 checks over two runs, starting from a queue holding one draft item, so the run's own verification pass has to make it pickable before any of this happens. With the stub answering proven the commit lands on the run branch and its trailer records the verdict; with STUB_VERDICT=rejected the gate is still green, the round ends discarded, the tree is cleaned, nothing is committed, and the item is back at ready with the prover's reason in lastFailure.

Reading the verdict out of the transcript

extractProverVerdict walks the JSON candidates in the transcript from the end and takes the last one that fully validates. Scanning from the front would be wrong by construction: the prompt embeds the contract in a fenced json block, so any transcript that echoes its prompt contains verdict-shaped JSON that is not a verdict. There is a test that feeds an entire prompt echo in and requires extraction to fail rather than grade the round with the example.

toProofOutcome turns the run into the round's outcome. A valid verdict passes through unchanged, partial included — it is never flattened into a binary. Everything else — empty transcript, prose, malformed JSON, a truncated answer, the contradiction above — becomes a rejected outcome with confidence 0 and the parse failure as its reason. If the invocation timed out, the reason also names the timeout and the elapsed milliseconds. The agent's exit code is recorded on the run result and decides nothing: a clean exit with no verdict is still a rejection, and a non-zero exit carrying a valid verdict still counts.

on_partial

proof:
  enabled: true      # default true
  on_partial: ask    # ask | keep | discard, default ask

keep and discard are themselves the answer, so the round resolves without anyone being woken: keep commits, discard discards and requeues with the reason carried, exactly as a rejection does. ask delegates to whatever can reach a human. Whichever way it goes, the trailer records what the prover actually said — a kept partial commits with Proof: partial, never laundered into proven. Turning proof.enabled off is allowed and configWarnings says what it costs: "proof.enabled is false — rounds will commit on a green build alone".

ask has no route to a human yet from looply run. The asker wired in run-cmd.ts logs the reason, logs that there is nobody to ask from a terminal run, and returns discard. The event kinds a phone question would use, question.asked and question.answered, exist and the server has a questions service, but the runner's asker does not emit them. Until that is built, on_partial: ask behaves as discard with an extra log line.

When the prover does not answer

The prover invocation gets 10 minutes (PROVER_TIMEOUT_MS), against 45 for the implementer. A timeout kills the process tree, and the empty or partial transcript falls through to the rejection path above. A prover that crashes outright — binary missing, transport down — used to take the whole overnight run with it. The runner now catches the throw, emits an alert with code prover-error and severity critical, discards the tree and requeues the item with "prover error: <message>". One round lost, not the night. The severity is critical because a dead prover discards every round until somebody hears about it.

Two structural details about when proof runs at all. The gate-side half of the commit permit is checked before the prover is invoked, so a round that could never commit does not pay for a proof call. And RoundRunner's constructor refuses to start with proof.enabled: true and no prover wired, or on_partial: ask with nothing wired to ask — wiring mistakes surface at construction, not at hour three.

What a healthy rejection rate looks like

This is the number that says whether any of the above is real. docs/PLAN.md targets 3–15 percent. Zero percent does not mean the implementer is flawless; it means the prover is decorative, agreeing with whatever is put in front of it, which is the exact failure this design exists to prevent. Well above 15 percent is also information: the item queue or the implementer prompt is in worse shape than the round tallies suggest.

looply report prints the measured rate and keeps "no proofs ran" distinct from a rate of exactly zero — proofRejectionRate is null when no verdict was recorded, so proof being switched off can never read as proof passing everything. The zero-rate alert is computed from ledger events: ZERO_REJECTION_ALERT_MIN_VERDICTS is 10, so a run with at least 10 verdicts and zero rejections raises a prover-never-rejects alert. Ten is a deliberate middle: three-for-three is luck and would cry wolf every evening, while waiting for a whole run's worth of unanimous approvals is far too late. It fires on live runs too, so it can be caught mid-night rather than read the next morning over a night of unproven commits. The alert leads the report, above the tallies and the per-round list:

$ looply report
ALERT   : prover approved all 14 proofs this run — a prover that never rejects is misconfigured (DESIGN §12 case 16)

run     : run_01k3m9x8q2n4vb7d — ended (min-hours)
elapsed : 6h 12m
tallies : 17 rounds — 14 committed · 3 discarded · 0 abandoned
proof   : 14 verdicts · 0 rejected (0%)
tests   : 22 added

The cost of proof is small next to a round. The prover reads a diff, not a repository, and returns a small object; the diff is capped at 200,000 bytes and truncation is announced in the prompt rather than silently swallowed, so a prover judging a partial diff knows that is what happened. Every verdict is written to the ledger as a proof.result event with actor prover: the line the report folds into its rate, and the line the app's project screen renders as "checked: proven — ...".

The prompt's first line tells the prover it has read-only access. Nothing in looply enforces that. One agent runner serves all three roles — implementer, prover, verifier — using agent.command, which defaults to claude -p --dangerously-skip-permissions, and any file the agent wrote during a proof call would be staged by the commit that follows. The read-only rule is an instruction to the agent, not a sandbox around it.