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

Write the claim in plan.ts as a list of stories. Each story has a gate: observe, act, assert. The agent may change code inside the story's scope. It may not change plan.ts.

View on GitHub Read the docs

one story

The contract is one executable TypeScript file.

Plan.define checks the stories. Plan.run runs them once. Plan.runLoop hands the first failing story to a worker and runs again.

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: "http://127.0.0.1:3210/" }),
        act: [Act.exec("curl -sf http://127.0.0.1:3210/")],
        assert: [
          Assert.httpResponse({ status: 200 }),
          Assert.responseBodyIncludes("hello world"),
          Assert.noErrors(),
        ],
      }),
    },
  ],
});

const result = await Effect.runPromise(Plan.run(plan));
if (result.status !== "pass") process.exitCode = 1;

To run it: clone the repo, bun install, then start the server with bun examples/hello-world/server.ts

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. Step 3 shows what happens if a worker edits plan.ts. The real script picks its own ports.

What Gateproof does today

stories

Stories with scope

Each story limits what a worker may change: allowed paths, forbidden paths, file and line budgets. plan.ts is forbidden by default.

dependsOn

Stories in order

A story can list earlier stories in dependsOn. If one of them ran and did not pass, the story fails without running. Plan.define rejects cycles.

lean

Lean as the judge

A story can pass only when the Lean kernel accepts a theorem. The example keeps sorry and axiom cheats red.

workers

Workers propose, gates decide

Use the built-in worker, one bounded turn on filepath, or your own function. A change outside scope is rejected.

deja

Memory between runs

Deja recalls learnings before each iteration and stores new ones after. A memory error never fails the run.

proof-spec.v0

Same schema as unsurf

planToProofSpecs turns stories into proof-spec.v0. Gateproof runs HTTP and shell. unsurf runs the browser.

lean gate

The kernel judges. The agent cannot fake it.

One story runs lean on an honest proof. Two stories depend on it and pass only when the sorry and axiom cheats are rejected.

Gate a Lean proof →

$ bun run example:hello-theorem

honest-kernel Claim.lean lean accepts pass

sorry-is-red cheat-sorry.lean check rejects pass

axiom-is-red cheat-axiom.lean check rejects pass

status: pass · 3 stories · cheats stay red

a few minutes with Bun

Run your first gate.

Clone the repository, run bun run example:hello-world, and break it on purpose.

Start the tutorial GitHub