proof authority for coding agents

The agent writes code. Gateproof says when it is done.

A plan.ts file is the contract. Plan.runLoop observes, acts, and asserts. Workers may change files inside allowedPaths. They may not rewrite the proof — plan.ts is forbidden by default.

hello world

The contract is one executable TypeScript file.

This is the public API: Gate.define, Plan.define, Plan.run / Plan.runLoop. The homepage walkthrough below is illustrative. The hello-world worker path is the live witness.

import { Effect } from "effect";
import {
  Act,
  Assert,
  Gate,
  Plan,
  createHttpObserveResource,
} from "gateproof";

const plan = Plan.define({
  stories: [{
    id: "hello-world",
    title: "GET / returns hello world",
    gate: Gate.define({
      observe: createHttpObserveResource({ url: "https://example.com" }),
      act: [Act.exec("curl -sf https://example.com")],
      assert: [
        Assert.httpResponse({ status: 200 }),
        Assert.responseBodyIncludes("hello world"),
        Assert.noErrors(),
      ],
    }),
  }],
});

if (import.meta.main) {
  const result = await Effect.runPromise(Plan.run(plan));
  console.log(JSON.stringify(result, null, 2));
  if (result.status !== "pass") process.exitCode = 1;
}

proof loop

The agent may change the implementation. It may not change the proof.

Fail, attempt, reject a plan.ts edit, retry inside examples/hello-world/, then pass. Same contract the whole way.

1. Assertion fails

Plan.run sees the live body. hello world is not there.

implementation examples/hello-world/response.txt → not ready

contract plan.ts unchanged

$ bun run example:hello-world:worker

GET / → 200

body → "not ready"

assert responseBodyIncludes("hello world") FAIL

status: fail

Illustrative terminal. The sequence matches Plan.runLoop, createOpenCodeWorker, and the default forbidden path plan.ts. It is not a live run.

You write the condition

A gate is an HTTP check, a shell command, or any observable assertion. Pass or fail is evidence, not a model opinion.

The agent runs the loop

Plan.runLoop hands the first failing story to a worker. createOpenCodeWorker may retry inside allowedPaths until the gate passes or maxIterations stops it.

The contract stays sealed

plan.ts, README.md, and .env are forbidden by default. A worker that edits the proof is a scope violation, not a pass.

Same shape as unsurf

Gateproof drives HTTP and exec. unsurf drives the DOM. Both speak proof-spec.v0 — the observe/act/assert schema round-trips between them. Import goalToProofSpec from gateproof to publish a plan as a typed spec, or proofSpecToGoal to run one unsurf scouted.

Case Studies

See it run against real systems.

Cinder is the first case study — a real system validated by a single plan file, start to finish.

Read the case study