Agent-written. Compiler-proven.

The AI writes your handler. The compiler proves it's safe.

Describe the handler you want. zigttp's agent writes it in a TypeScript subset narrow enough for the compiler to prove - every path returns, every declared guarantee holds - and rejects any draft that fails. You approve only code that passes.

Try compile-time proof Watch the agent loop

curl -fsSL
              https://raw.githubusercontent.com/srdjan/zigttp/main/install.sh |
              sh

Break while, try/catch, or Date.now() and the compiler tells you why the proof failed.

handler.tsproven

contractsafe_with_additions

witnesses2 pinned

✓

returnscomplete

✓

match coverageexhaustive

✓

no_secret_leakagedischarged

●

ledgerHEAD appended

proof loop handler.ts proof ledger +

src/handler.tssaved 14ms ago

import { decodeJson } from "zigttp:decode";
import type { Spec } from "zigttp:types";

type Guardrails = Spec<
  "idempotent" | "deterministic" |
  "no_secret_leakage"
>;

function handler(req): Response & Guardrails {
  const body = decodeJson("order", req.body ?? "");
  assert(body.ok, Response.json({ errors: body.errors }, { status: 400 }));
  return Response.json({ status: "accepted" });
}

zigttp dev --watchlive

PROVEN 7/7

contractsafe_with_additions sandboxleast privilege binary4.8MB cold start~7ms

$ zigttp dev --watch --prove
verdict: safe_with_additions
ledger: .zigttp/proofs.jsonl
hot swap: allowed

Compiler proof, contract diff, and local deploy receipt in one loop.

The real compiler, in your browser

Prove code before it runs.

The playground runs the real zigts analyzer in WebAssembly, not a mockup. It proves the handler from source, then shows the exact file, line, and reason the moment you add code it cannot prove.

Compile-time analyzer Source stays in page Proof blocks anomaly

import type { Spec } from "zigttp:types";

// All guarantees are enforced by default. This Spec<...>
// narrows enforcement to these three; break one and the card flips red.
type Guarantees = Spec<
  "deterministic" | "no_secret_leakage" | "injection_safe"
>;

function handler(req: Request): Response & Guarantees {
  return Response.json({ ok: true });
}

PROVEN 3/3 specs | 6/7 props compiled from source

+deterministic
+read-only
+state-isolated
+injection-safe
+retry-safe
+idempotent
-fault-covered

declared Spec<> deterministic no_secret_leakage injection_safe

fault-covered stays off until a handler has a proven durable recovery path - see durable workflows.

Press a perturbation, then read the certificate here.

What a third party sees when they verify your deploy:

HTTP/1.1 200 OK
Zigttp-Proofs: deterministic, read_only, injection_safe
Zigttp-Attest: eyJhbGciOiJFZERTQS...

$ zigttp verify https://your-service.dev
  Verified  key 9f2c..a1  3 proven chips

The signature is checked against the public key at /.well-known/zigttp-attest.

Compiler-in-the-loop agent

The compiler won't let the agent guess.

New in v0.1.1-beta: zigttp expert asks for the missing detail when a request is materially ambiguous, then records the proof-loop metrics that show how quickly it reached green.

How the loop runs

01 Clarify
If intent is ambiguous, the agent asks one question instead of guessing.
02 Write
The agent drafts a handler from your confirmed request.
03 Compile
It runs the same proof pass that gates deploys.
04 Repair
It edits against compiler diagnostics and tries again.
Proven
The handler clears the proof loop before you review it.

clarify, write, compile, repair - repeat until proven

Compiler transcript show compiler loop

zigttp expertcompiler in the loop

$ zigttp expert "add auth to the webhook"

[agent] Need one detail: Bearer token, HMAC, or mTLS?
[you] Bearer token

[agent] Writing handler...
[agent] Compiling handler.ts

  error[E0003]: try/catch is not supported in zigts
    --> handler.ts:12:5
    = help: use Result types

[agent] Rewriting with Result types...
[agent] Compiling handler.ts

  PROVEN 7/7 proofs
  Handler ready: webhook-auth (1.2MB)

$ /ledger
  turns: 3
  round-trips to first green proof: 2
  verified edits: 1
  proven-path ratio: 1.00

zigttp expert now stops for one clarifying question when the request is materially ambiguous. After that, it writes code, runs the proof pass, reads the diagnostics, rewrites, and records session metrics so you can see the path to green instead of trusting a transcript by feel.

Ask once before spending proof cycles on a misread.
Compile every patch against the proof rules.
Show turn count, verified edits, and proven-path ratio.

ordinary agent

Guesses through ambiguous requirements and waits for tests or review to find the mismatch.

zigttp expert

Asks one question, compiles each draft, reads proof errors, and reports the proof-loop metrics.

zigttp expert supports Anthropic and OpenAI keys, resume, read-only mode, non-interactive prompts, and per-session session_summary metrics.

Compiler runs locally Provider keys from env Read-only mode available

Durable workflows

Compose handlers. Prove the recovery.

zigttp:workflow composes co-located handlers in-process: call, saga, fanout, resolved by name at compile time, no HTTP hop. zigttp:durable gives a run a stable key, an oplog, timers, and signals. The compiler proves which runs are safe to replay - the runtime refuses the ones it can't.

orchestrator.tsone process, no network

import { run } from "zigttp:durable";
import { call } from "zigttp:workflow";
import type { Spec } from "zigttp:types";

type Guarantees = Spec<
  "deterministic" | "retry_safe" | "idempotent" |
  "fault_covered" | "state_isolated" | "no_secret_leakage"
>;

function handler(req: Request): Response & Guarantees {
  const key = req.headers.get("idempotency-key") ?? "demo";
  return run(key, () => {
    const res = call("greet", { method: "GET", path: "/hello" });
    return Response.json({ runKey: key, subStatus: res.status, sub: res.json() });
  });
}

# resolve every call target by name, then serve durably
$ zigttp link system.json
$ zigttp serve orchestrator.ts --system system.json \
    --durable ./.durable --workflow-queue

There is no workflow DSL - just disciplined naming over primitives. call("greet", ...) runs another handler in an isolated pooled runtime and copies its Response back. run(key, ...) owns the parent workflow and writes every step to an oplog. The Idempotency-Key header becomes the run key; each workflow.call() is a child boundary. Timers and signals are primitives too: sleep, sleepUntil, waitSignal, signalAt.

zigttp link system.json resolves every call, saga, and fanout target by name at compile time.
saga([...]) rolls back completed steps in reverse order when a step returns status 400 or above - each step carries its own compensate.
A panicking sub-handler surfaces as subStatus 599 - the orchestrator answers instead of crashing.

When a step fails

01 Isolate
A panic stops at the handler boundary: the caller gets 500, the pool slot is quarantined, every other worker keeps serving.
02 Prove
Reusing a completed response needs idempotent; retrying an incomplete run needs retry_safe - or a client Idempotency-Key. Unproven replay gets a soft 599, never a silent re-run.
03 Retry
A background scheduler replays the incomplete oplog with jittered exponential backoff.
04 Quarantine
Ten consecutive failures move the run to dead-runs/<id>.json. It survives restart and waits for a human.
Recovered
The run resumes from its oplog - replayed from the log, not re-guessed.

isolate, prove, retry, quarantine - no silent re-run

Most of it is settled before the server starts.

ZTS509: no calls inside steps

workflow.call, saga, and fanout are rejected inside a durable.step() callback - nesting that would silently lose durability.

ZTS510: no rollback holes

A static saga must carry a compensate on every step except possibly the last - the structural signature of a partial rollback.

Proofs in the contract

contract.json records retrySafe, idempotent, faultCovered. The proof receipt carries durableWorkflowProofLevel.

ordinary retry

Retries on failure and hopes the handler was idempotent. The duplicate side effect shows up later, in the logs.

zigttp durable run

Fails closed. Without a retry_safe proof or an Idempotency-Key, replay is refused with a 599 the client can read: DurableRetryUnproven, not a silent second run.

You have already met the missing proof. In the playground above, the fault-covered chip sits off: a plain handler has no durable recovery path for its effects, so the compiler will not claim one. fault_covered is what durable.run() and proven saga compensates earn.

fanout dispatches sequentially, not in parallel a failing compensate is a terminal 500, manual intervention beta: throughput ships with receipt-backed measurement

Positioning

The trade that makes compile-time proof work.

zigttp gives up the full JavaScript and npm surface so the compiler can enumerate handler paths, capabilities, and declared guarantees before deploy.

Capability	Node / Deno / Bun	Serverless platforms	Static type checks	zigttp
Runs TypeScript handlers	✓	✓	partial	✓
Compile-time path and guarantee proofs	-	-	limited	✓
Guarantees enforced by default	-	-	-	✓
Durable workflows with proven-safe replay	-	partial	-	✓
Compiler-guided agent	-	-	-	✓
Small self-contained Zig binary	-	-	-	✓
Proof ledger and witness replay	-	-	-	✓

Runs TypeScript handlers

Node/Deno/Bun ✓Serverless ✓Type checks partialzigttp ✓

Compile-time path and guarantee proofs

Node/Deno/Bun -Serverless -Type checks limitedzigttp ✓

Guarantees enforced by default

Node/Deno/Bun -Serverless -Type checks -zigttp ✓

Durable workflows with proven-safe replay

Node/Deno/Bun -Serverless partialType checks -zigttp ✓

Compiler-guided agent

Node/Deno/Bun -Serverless -Type checks -zigttp ✓

Small Zig binary

Node/Deno/Bun -Serverless -Type checks -zigttp ✓

Proof ledger and witness replay

Node/Deno/Bun -Serverless -Type checks -zigttp ✓

Core idea

Three claims, all concrete.

Provable TypeScript

zigts removes the features that hide control flow: while, try/catch, class, var. That buys the compiler up to 13 properties per handler - every path returns, no secret leaks, safe-to-replay durable runs.

Compiler-in-the-loop agent

zigttp expert writes a patch, runs the proof pass, asks when the prompt is ambiguous, and rewrites until the compiler accepts it.

Small Zig binaries

zigttp deploy emits a local self-contained binary. Current public baseline: 4.8 MB and 7-15 ms typical cold start.

CLI surface

Five commands cover the proof loop.

Init a handler, prove it on save, test it, ask the compiler-guided agent for edits, then deploy a signed local binary.

Getting started CLI reference Contracts and sandboxing Virtual modules Source Deck

Every deploy appends a contract verdict to proofs.jsonl:

safe safe_with_additions blocked needs_review

# create a handler project
zigttp init api && cd api
zigttp dev

# run handler tests
zigttp test

# ask the compiler-guided agent for a patch
zigttp expert "add health check"

# build a signed local binary
zigttp deploy
zigttp proofs show HEAD

Start proving

Install zigttp. Break a proof on purpose.

The quickest demo is one unsupported feature. Add while or try/catch and watch the compiler point to the proof it cannot discharge.

Download v0.1.1-beta Quick start