Holds by construction
Rejected drafts cannot reach the write path. The analyzer is total over zts.
zttp agent-compiler
AI-written TypeScript, proved before it lands.
zttp restricts TypeScript to a language its compiler can judge completely, so red drafts never reach disk and supported failures get a compiler-authored repair.
$
curl -fsSL
https://raw.githubusercontent.com/srdjan/zttp/main/install.sh |
sh
zttp expertone write path
$ zttp expert "add auth to the webhook"
[agent] draft 1: simulating before write
[veto] draft adds a violation
error[E0003]: try/catch is not supported in zts
--> handler.ts:12:5
[compiler] canonicalize and re-simulate: still red
[compiler] typed repair: try/catch -> Result
[compiler] applied with no model call
edit recorded: compiler-authored
PROVEN 3/3 declared | 6/7 propertiesLive zts analyzer
Break a proof in your browser.
Edit the handler or inject a failure. The WebAssembly analyzer returns the failed property, file, and line. Your source stays in the page.
Real analyzer
Local source
Typed verdict
PROVEN
3/3 specs | 6/7 props
pre-rendered proof preview
- +deterministic
- +read-only
- +state-isolated
- +injection-safe
- +retry-safe
- +idempotent
- -fault-covered
declared Spec<>
deterministic
no_secret_leakage
injection_safe
fault-covered requires a proven recovery path.
Press a perturbation, then read the certificate here.
What a third party sees when they verify your deploy:
HTTP/1.1 200 OK Zttp-Proofs: deterministic, read_only, injection_safe Zttp-Attest: eyJhbGciOiJFZERTQS...
$ zttp verify https://your-service.dev Verified key 9f2c..a1 3 proven chips Policy pinned by runtime_policy_sha256
The signature is checked against the public key at
/.well-known/zttp-attest. Since v0.18.0 the
envelope also pins the egress, env, cache, and SQL allowlist the
sandbox enforces.
One write path
The compiler gates every agent edit.
The agent drafts. The compiler proves the draft before writing it. Green code lands. Supported failures are repaired and proved again.
-
01
Draft
The agent proposes a handler.
-
02
Prove
The compiler checks it before disk.
-
03
Repair
Supported failures receive a typed compiler edit.
-
04
Write
Only a green result lands.
The session ledger records whether the model or compiler authored each
edit. zttp expert needs an Anthropic or OpenAI key.
Why zts restricts TypeScript
zts removes constructs that make whole-program proof open-ended. Each restriction buys a specific proof and narrows the agent's search space.
Read the restriction mapCompare zttp with bolt-on checkers
Agent plus checker: code lands before a post-hoc verdict over an unrestricted language.
Compiler plus agent: diagnostics feed an open-ended model retry loop.
zttp: the restricted language and compiler share the only write path.
Current evidence
See what holds today.
zttp separates construction guarantees from incomplete and unmeasured claims. The ledger is versioned with the repository.
Thin today
Compiler-authored repairs and replayable witnesses exist, with limited aggregate agent evidence.
Unmeasured
Reachability across the provable set and time to first green have no current aggregate.
Attested runtime
Ship the proof with the handler.
zttp deploy builds one signed binary.
zttp verify <url> checks the signature and
pinned runtime policy.
- Self-contained binary
- Signed receipt
- Public verification
Open the full claim ledger
The roadmap names each claim, its evidence grade, and the file that owns the measurement.
Recount the claimsRuntime and workflow details
First proof
Prove your first handler.
Install zttp, scaffold an API, then add an unsupported construct. The compiler points to the failed property and source line.
$
curl -fsSL
https://raw.githubusercontent.com/srdjan/zttp/main/install.sh |
sh
zttp init api --template api
cd api
zttp dev
zttp expert needs an Anthropic or OpenAI key. The
compiler, CLI, and browser playground do not.