gdp-ts: making the authorization check a value the compiler can see

mdjsonmcpcopy↗ai

2026-10-06 · 18 min · explainer · agents · security · harness · open-source

Most authorization bugs are not wrong policy. They are a correct check that never reached the line that needed it: the handler checks project A and writes to project B, or a refactor drops an await. Code review is supposed to catch these, and at the rate agents now write code, review is the part that does not scale.

gdp-ts is Guillermo Rauch's answer, announced on X on 2026-10-05 as "a library, linter and AI skill for safer API design". Under its contract, "sensitive functions require 'proofs' that the caller performed an authorization check", and the type checker verifies them. The pattern is old. It is Matt Noonan's Ghosts of Departed Proofs from Haskell Symposium 2018, applied to authorization by Ollie Charles in 2019. Rauch's argument is about why it is practical now:

Agents are writing more code than we can review, and they thrive in tight loops with hard constraints that would frustrate us.

I read the whole repository, re-derived the mechanism, and type-checked every combination of mistakes a caller can make in front of the README's own sensitive function. The type checker catches all the honest mistakes. The two forgeries that get past it are what the linter is for.

expand

The bug is a boolean

The README opens with this handler:

async function handler(req, res) {
  await assertProjectAdmin(req.user.id, req.params.projectId); // throws 403
  await setPasswordProtection(req.params.projectId, req.body.password); // nothing connects this to the line above
  res.sendStatus(204);
}

The comment on the second line is the whole problem. assertProjectAdmin learns something true about one user and one project, then throws the knowledge away. What reaches setPasswordProtection is a project id and a password, and its signature, (projectId: ProjectId, password: string), accepts any caller that has those, checked or not. Robert Harper called this boolean blindness: a test yields one bit, and the bit does not say what it was about.

The fix is to make the check return something that does say what it was about, and to make the sensitive function demand it.

Ghosts, in Haskell

Noonan's paper starts from a smaller problem. A mergeBy over two lists is only correct if both were sorted by the same comparator. Documenting that, checking it at runtime, or returning Maybe all push work onto a caller who already knows the answer. GDP lets the caller tell the library.

Step one is a name. A value of type a gets a phantom type parameter name, which exists only to the compiler:

expand

The forall name. inside the argument is the trick. name takes a continuation that must work for every possible name, so inside it the name is a fresh, opaque type that matches nothing else. Two calls give two incompatible names, even for the same value.

Step two is a predicate attached to a name, and a module that is the only place able to create it:

expand

That is the full pattern: name a value, let one trusted module mint facts about names, and make the consumer demand the fact. The paper's phrase for why the proofs are "ghosts" is that "no artifacts related to the proof should ever be discernible from the compiler's output".

Ollie Charles's Who Authorized These Ghosts!? made the jump to access control at CircuitHub: name the project and the user, and make price demand a CanViewProject proof about exactly those two names. gdp-ts is that post, ported to TypeScript and to Vercel's Password Protection feature.

Three moves in TypeScript

Name values

// app.ts (from the gdp-ts README)
app.delete(
  "/projects/:id/password-protection",
  authenticated((viewer, req, res) =>
    name(viewer.id, ProjectId(req.params.id), async (user, project) => {
      const admin = await userIsProjectAdmin(user, project);
      if (!admin) throw new HttpError(403, "Only Owners and Members can change this");
      await disablePasswordProtection(project, admin);
      res.sendStatus(204);
    }),
  ),
);

TypeScript has no forall inside an argument type, but it has generic callbacks, which do the same job. The library's signature for the two-value case:

// src/index.ts
export function name<A, B, R>(
  a: A,
  b: B,
  k: <N, M>(a: Named<N, A>, b: Named<M, B>) => R,
): R;

Inside k, N and M are type parameters the callback must be generic over. Nothing outside can produce a Named<N, …>, and the two are distinct from each other. At runtime name wraps each value in a frozen { value } and calls k.

Prove facts about names

A proof lives in a small module under proofs/. The module creates a prover and keeps it private:

// proofs/user-is-project-admin.ts (trusted: the only place that can mint this proof)
const UserIsProjectAdmin = defineProof("UserIsProjectAdmin"); // not exported
export interface UserIsProjectAdmin<U, P> extends Proof<"UserIsProjectAdmin", [U, P]> {}
 
export async function userIsProjectAdmin<U, P>(
  user: Named<U, UserId>,
  project: Named<P, ProjectId>,
): Promise<UserIsProjectAdmin<U, P> | null> {
  const role = await db.roleInProjectTeam(user.value, project.value);
  return role === "owner" || role === "member" ? UserIsProjectAdmin.prove(user, project) : null;
}

prove(user, project) infers the proof's About tuple from its arguments, so the proof is visibly about these names. A failed check returns null, and the caller decides whether that is a 401, a 403 or a fall-through.

Demand proofs

// data/projects.ts (sensitive: demands exact proofs)
export function disablePasswordProtection<U, P>(
  project: Named<P, ProjectId>,
  _proof: UserIsProjectAdmin<U, P>,
): Promise<void> {
  return db.writePasswordProtection(project.value, null);
}

The P in the project and the P in the proof are the same type parameter. A proof minted for a different name() call, or for a different value in the same call, carries a different name and does not unify. When a function needs several facts, it takes them as an object. The README's headline case needs both a role and an entitlement:

export function setPasswordProtection<U, P>(
  project: Named<P, ProjectId>,
  actor: Named<U, UserId>, // recorded as updatedBy; the proofs must be about this user
  setting: { deploymentType: DeploymentType; password: string },
  _proofs: { manage: CanManageProtection<U, P>; plan: PlanIncludesPasswordProtection<P> },
): Promise<void>;

CanManageProtection is the admin proof. PlanIncludesPasswordProtection is a proof about the project's billing plan, which has nothing to do with who is asking. Password Protection is not on the Hobby plan, so forgetting that check is a support ticket today and a compile error here. Taking actor as a named argument means a manage proof about some other user cannot be passed in while the audit column records you.

Where TypeScript fights back

Haskell gave Noonan three things for free that TypeScript does not. src/index.ts is mostly comments explaining how it gets each one back.

Phantom parameters are ignored unless used. TypeScript compares types by structure. An interface whose N appears in no property is the same type for every N, so every name would match every other. gdp-ts stores the name in a property that is never assigned:

// src/index.ts
export interface Named<in out N, out A> {
  readonly value: A;
  readonly [NAME]: (n: N) => N;
}

The in out annotation makes N invariant, so a Named<never, A> or Named<unknown, A> cannot stand in for a real name. The comment explains why the function-typed slot is there as well: TypeScript falls back to structural comparison in some places, notably discriminated-union targets, and a plain N slot would let never through there. Proof<Kind, About> uses the same (about: About) => About slot.

Names must not escape. If a callback could return its Named, the name would outlive the request it was checked in. Returning one forces TypeScript to instantiate N as unknown on the way out, and invariance rejects that. I checked it on 5.9.3: name(a, (project) => project) fails with Type 'Named<N, ProjectId>' is not assignable to type 'Named<unknown, ProjectId>' (measured). The skill's limits page says TypeScript 5.4 and 5.5 catch a returned Named too, but let one wrapped in an object leak as an unbound type parameter that still cannot be mixed up with another (reported).

There are no private constructors. In Haskell, not exporting SortedBy's constructor means no client can make one. In TypeScript, {} as UserIsProjectAdmin<U, P> compiles anywhere. The library confines its own cheat to one line, inside defineProof:

// The single type assertion in this library. Everything downstream of
// `prove` is honest, which is what lets you ban `as` in application code.
prove: () => proof as Proof<Kind, any>,

That comment is the design. The honest path never needs an assertion, so any assertion near a proof is either a bug or a forgery, and a linter can flag it.

Will it typecheck?

The sensitive call is setPasswordProtection(project, user, pw, { manage, plan }). A caller makes four choices in front of it: which role check to run (if any), whether to handle a null result, which project's plan to check, and whether to pass the named project or the raw id. I added two forgeries to the role choices. That gives 5 × 2 × 3 × 2 = 60 combinations. I generated a name() callback for each one, used src/index.ts verbatim from commit ebd0af9, re-declared the proofs and the sensitive function the way examples/basic does, and ran tsc 5.9.3 under the benchmark's compiler options.

name(viewer.id, a, b, async (user, project, other) => {
  const manage = await canViewProtection(user, project);
  if (!manage) throw new HttpError(403, "…");
  const plan = await planIncludesPasswordProtection(project);
  if (!plan) throw new HttpError(403, "…");
  await setPasswordProtection(project, user, pw, { manage, plan });
});

Three of the 60 compile (measured):

1. canManageProtection on this project, null handled, the plan checked on this project, the named project passed. The honest path.
2. The same, but with the manage proof forged as {} as CanManageProtection<…>.
3. The same, but with null as any as the manage proof.

Every other combination fails with a specific message (measured, quoted from tsc):

• No role check: Property 'manage' is missing in type '{ plan: PlanIncludesPasswordProtection<M>; }'.
• A view check where a manage check is required: Type 'UserIsProjectAdmin<N, M> | UserHasProjectAccess<N, M>' is not assignable to type 'CanManageProtection<N, M>'. The view policy is a union that includes plain team access. The type error is the difference between "can see the setting" and "can change it".
• null not handled: the | null survives into the argument type and is rejected.
• The plan checked on the other project: Type 'PlanIncludesPasswordProtection<O>' is not assignable to type 'PlanIncludesPasswordProtection<M>'. O and M are the two projects' names. This is the cross-resource bug the skill says is where cross-tenant incidents live.
• The raw id: Argument of type 'ProjectId' is not assignable to parameter of type 'Named<M, ProjectId>'.

One caveat about reading these. tsc reports the first argument of a call that fails, so a raw id hides the proof errors behind it until you fix the id. The repo's own snapshot (examples/basic/test/mistakes.snapshot.txt, on TypeScript 7.0) lists 12 such mistakes with the same error codes. Where the two differ, it is in which letter a type parameter prints as. The full matrix is below.

What the linter adds

The type checker cannot see the difference between a proof that came out of proofs/ and one written by hand with as. The linter does that job. All five rules are syntactic, so they need no type information and run under ESLint, and under Oxlint on TypeScript 7:

Map that onto the two forgeries that compiled. {} as CanManageProtection<…> is an assertion to a type imported from proofs/, so the default preset reports it with Do not assert a proof or Named type. null as any is the gap. The default preset only watches assertions to proof types, and the README says it "cannot see null as any handed straight to a proof parameter". Strict mode bans every as and any outside proofs/ and lib/ids.ts, the branded-id constructors. The repo's shared lint test cases expect null as any to produce nothing in default mode and both strict rules in strict mode. I am reading that from the test file and the rule source. I did not run the linter (reasoned).

So new code wants strict mode; the default mode is for switching on in an existing codebase. Rauch said in the thread that this is why the linter exists at all: he "had to ship a linter to avoid would-be agents cheating the proof system with 𝚊𝚜 𝚊𝚗𝚢 shenanigans". An agent told to make the build green reaches for as any, and the type system accepts it.

cuda-oxide in CUDA Rust asks the same question: its ThreadIndex can only be minted from hardware registers. Rust enforces that private constructor; TypeScript needs a lint rule for it.

The skill

The third piece is skills/gdp-ts/SKILL.md, installed with npx skills add rauchg/gdp-ts. It is plain Markdown and doubles as the manual. Its workflow is ten steps for adding or changing authorization. A few of them carry most of the weight for an agent:

• "If it takes raw ids, change the signature; let the compiler list the call sites to fix." Changing a signature turns a code search into a compiler task, which is the loop agents handle well.
• "Never write as to satisfy a proof or Named type. If you feel the need, the signature is wrong or you are outside proofs/." It names the forgery up front, before the agent finds it alone.
• "Add the new mistake you almost made to mistakes.ts", a file that is type-checked but never run, one line per near-miss under // @ts-expect-error. tsc fails on an unused @ts-expect-error, so if anyone loosens a sensitive signature, the build breaks. That covers the regression one reply on the launch post worried about: an agent fixes a failing caller by weakening the callee.
• "Test the proof function you added. It is the only thing that can be wrong at runtime."

A page called Where to stop reins it in: name values that cross a trust boundary, not page sizes, and "if a signature starts needing four type parameters, you have gone too far." The authors expect the pattern to be over-applied, and agents follow a pattern harder than people do.

This is a harness decision as much as a library decision. Lilian Weng's point that guardrails live outside the loop applies here: the guarantee does not depend on the agent remembering the rule, because the compiler and the linter run whether it remembers or not.

What it costs to type-check

The repository includes a benchmark that generates two synthetic codebases with the same files and module graph, one with boolean checks and one with gdp-ts, at 1,000 to 20,000 files (all figures reported, Apple M5, medians of 5 runs):

The per-call-site cost is what transfers. On TypeScript 7 it is about 280 µs of check time and 181 KB of memory per name() site, flat from 1,000 to 20,000 files. On 5.9 and 6.0 it is about 650 µs and 240 KB. TypeScript 5.9.3 and 6.0.3 ran out of memory on the 20,000-file gdp variant at Node's default 4,288 MB heap. The generated gdp code is about 35% more lines.

The benchmark says itself that nearly every generated line is authorization code, so the 5-6x ratio is an upper bound. For a service with 2,000 authorized call sites on TypeScript 7, that is 2,000 × 280 µs, about 0.56 s of extra check time and around 360 MB (reasoned). On 5.x in a large monorepo, the memory is what I would test first.

What it does not guarantee

The skill's limits page does not oversell. In my words:

• The check itself is still your code. A proof means userIsProjectAdmin returned non-null. If that query joins the wrong table, the type checker will carry the wrong answer through every layer with total confidence. The trusted modules are the trusted computing base, and they are the part that needs tests.
• Proofs go stale. A proof says the fact held when it was checked. Proofs are request-scoped, because the name callback enforces it. Inside one request, though, a role revoked between the check and the write is a race the types cannot see. Use transactions or database constraints where it matters. Where to stop says to keep both: "the constraint stops bad rows, the proof stops bad code paths from being written."
• Forgery is a lint error, not a type error. Turn off the preset, use // eslint-disable, or write the forgery in a file the preset does not cover, and the guarantee is gone. That is weaker than Haskell, where a hidden constructor cannot be reached at all. The repo is direct about it.
• Structural typing still has corners. Write proofs as interface X<U, P> extends Proof<…> {}, not as a type alias. With aliases, inference can confuse one kind's names with another's when a function accepts a union of proofs. The symptom is Named<unknown, _> showing up in a call that should be valid.
• It does not decide policy. It does not replace a policy engine (CASL, Oso, OpenFGA). It makes sure the engine's decision reaches the function that depends on it, about the right values. You can call your engine inside a proof function.
• Proofs do not cross process boundaries. This one is my inference, not the repo's. A proof is a type plus a frozen { kind } object. Once a job goes onto a queue, the worker cannot receive a proof the compiler will trust, so it has to name its values and check again. That is correct behavior, but it is a re-check you will have to design for (reasoned).

The take

The mechanism is not new, and the repository says so on every page. What is new is the claim about who pays for it. GDP stayed niche in Haskell because humans had to write the type parameters, read the errors and review the result. Rauch's bet is that an agent will happily do the first two in a tight compile loop and that the compiler reduces the third. My matrix supports the narrow version of that bet. Every honest mistake I could generate in front of one sensitive call was a compile error with a message that names the wrong value, and the two things that slipped past the compiler are syntactic patterns a linter catches in strict mode.

The broader claim, that strict type systems matter more as agents write more of the code, is the same argument as Leanstral, where a model can do proof search because Lean will not accept a fake proof. gdp-ts is a much weaker checker than Lean, and says so. It covers one class of bug and ships the lint rule for the way around it. I would adopt it in strict mode, put the demand in the data layer, and spend the saved review time on proofs/.