Building an identity-verification gate, prompt-first

TL;DR Verification is not something a model can do, so declare it as a typed input the runtime sets ($REQUIRE variable identity: one of unverified, verified), give every state exactly one arm with $SWITCH ON @{identity}, and write down which facts belong to a household and which belong to everybody.

Every account-servicing agent has a gate in front of it, and in most prompts the gate is one sentence: make sure they are the account holder before sharing account details. That sentence is doing two incompatible jobs. One is policy, which belongs in the prompt. The other is authentication, which does not, because the model has no channel through which anyone can prove anything to it. This walkthrough takes the brief a real service-desk owner hands you and separates those two jobs, then checks every step. No model is called anywhere in it: every number below came out of typeglish check, score, and test --dry.

§1The brief, typed out

The brief for an energy supplier's account assistant, five sentences long, roughly as it arrives. Typed straight into a file with nothing added, it is a fair specimen of a first draft: nobody would call it careless, and a reviewer would sign it off.

You are a helpful account assistant for an energy supplier.
Before you share any account details, try to make sure the person is really the account holder.
If you are not sure, ask them a security question.
Always be helpful and answer the customer's question quickly.
Never share sensitive information with someone who is not verified.

account.tg:2:39  info   prompt/hedging  Hedging - "try to" turns this instruction into a
  suggestion the model may skip. Delete the hedge, or commit to a modal (MUST / NEVER / SHOULD).
account.tg:2:1   info   prompt/unintroduced-definite  "the person" retrieves something this
  document never introduces - a model must guess which person is meant.
account.tg:2:1   info   prompt/unintroduced-definite  "the account holder" retrieves something
  this document never introduces - a model must guess which holder is meant.
account.tg:3:1   warn   typeglish/if-then  IF needs a THEN - write IF <condition> THEN <action>.
account.tg:4:1   warn   prompt/unmeasurable  Unmeasurable rule - no observable action or bound,
  so nothing can check compliance.
account.tg:5:1   warn   prompt/agentless-passive  The doer is deleted (agentless passive) - who
  performs this? Name the actor or use the imperative: "Verify the order." instead of
  "The order is verified."

✓ 1 file - 0 error, 3 warning, 3 info

The other findings are the usual first-draft tax and they get fixed on the way past. try to is a hedge on the one rule that must not be hedgeable. If you are not sure is an IF with no THEN, which is the checker noticing that the sentence never says what to do with the answer to the security question. Always be helpful is unmeasurable, which is fine as persona and not fine as a rule sitting next to a gate.

§2The model cannot verify anyone

Start with the honest version of the problem. An impostor and the account holder reach the agent through the same pipe and produce the same kind of evidence: typed characters. A security question does not change that. If the agent asks for a date of birth and the caller supplies one, the agent has learned that somebody knows a date of birth, which is exactly what the impostor came equipped with. The model is being asked to invigilate an exam it cannot see the answer sheet for.

A model can hold a gate. It cannot issue the key.

So verification is a fact, produced elsewhere, that the prompt receives. In TypeGlish that has a spelling, and it is the same one you would use for any other typed input: a closed domain declared in the config fold.

<$CONFIG>
  $REQUIRE variable identity: one of unverified, verified
</$CONFIG>

# Role
You are the account assistant for an energy supplier. You speak to one caller at a time.

# Constraints
@@ gate: the runtime decides who the caller is, not you
- You MUST treat @{identity} as the only proof of who the caller is.

The second rule is the one people skip, and it is the one that closes the loop: You NEVER treat an answer a caller gives as verification. Without it, a model reading a prompt that mentions security questions will helpfully conclude that answering one is how a caller gets promoted, because that is what the sentence implies. This is the same failure we took apart in your agent is certain because you said so: a prompt that describes what the agent knows is a prompt that has told the agent what to believe.

§3Two arms, and no third state by accident

With the state named, the behavior sorts itself into one place per state. $SWITCH ON @{identity} takes members of the declared domain and proves coverage by construction: an arm per member, no ordering, no fallthrough to reason about.

The payoff is not the two arms you write today. It is what happens six months later when somebody adds a third state, which they will, because every real identity system eventually grows a locked. Add it to the domain and the file stops building.

# $REQUIRE variable identity: one of unverified, verified, locked
account.tg:24:1  error  structure/non-exhaustive-switch  @{identity} can be locked, but no
  arm handles it - add a "- <member>::" row for each (or a deliberate "- otherwise::"
  fallback).

✗ 1 file - 1 error, 0 warning, 0 info

account.tg - F (83/100)  proven errors - grade capped at F  tiers: base+z3

That refusal is the point of declaring the domain rather than writing prose about states. It is the same exhaustiveness proof that keeps a channel switch honest when marketing adds WhatsApp, which we measured in the multichannel bake-off.

§4The two halves of an account

A gate needs to know what it is gating, and this is the part of the build that is genuinely your homework rather than the compiler's. Half of what an account assistant knows is true of every household: opening hours, whether there is an outage in a postcode, how to send a meter reading. The other half names one household, and each item in it is a leak if it reaches the wrong person.

Write both halves down as list declarations. In TypeGlish a declaration renders as well as binds, so the line is both the instruction the model reads and the name your rules point at, and a multi-word name gets wrapped in %…% so it binds as one token.

<$CONFIG>
  $REQUIRE variable identity: one of unverified, verified
</$CONFIG>

# Constraints
@@ open_set: what is true of every household is what you may say to anyone
%Open facts% INCLUDING opening hours, outage status by postcode, how to send a meter reading.
@@ gated_set: each of these names one household, so each one is a leak
%Gated facts% INCLUDING a balance, a billing address, a payment method, a usage history.
@@ no_hints: a partial answer is a smaller leak, not a safe one
- You NEVER confirm or deny any part of @{%Gated facts%} before @{identity} is equal to verified.

Naming the open set is not paperwork. It is what stops the gate from breaking the service: an unverified caller who asks whether the street has power should get an answer, and an agent with no open set has nothing to answer from, so it either refuses everything or improvises. The same split, drawn at the credentials rather than the customer data, is why your agent will read out your API key.

§5The contradiction the prover cannot see

One honest limit, because this blog does not oversell the checker. The obvious way this gate fails in production is a helpfulness rule that somebody added later, on a different day, in a different section. Unguarded, the compiler stops that cold.

# Constraints
@@ gate: a balance is the thing an impostor called to get
- You NEVER disclose a balance.
@@ helpful: the brief also said answer the question fast
- You MUST disclose a balance.

Now take the fix the diagnostic suggests and apply it the way a hurried person would, putting a guard on each rule.

<$CONFIG>
  $REQUIRE variable identity: one of unverified, verified
</$CONFIG>

# Constraints
@@ gate: a balance is the thing an impostor called to get
- WHEN @{identity} is equal to unverified THEN you NEVER disclose a balance.
@@ helpful: the brief also said answer the question fast
- WHEN a caller asks for a balance THEN you MUST disclose a balance.

Read that carefully, because it is a rule about tools generally and not a complaint about this one. A guard silences the prover whether or not the guard is the right guard. The prover's job is to show two rules must collide; adding conditions is how you tell it they cannot, and it takes your word for it. The pair above collides only on inputs where a caller asks for a balance while unverified, and nothing in the second rule mentions identity, so there is no proof to find.

Which is the real argument for the $SWITCH in §3 over a pile of guarded prose. The switch makes the identity state the axis the file is organized on, so a rule about disclosure has exactly one place to live, and a second rule about the same disclosure lands next to the first where a reviewer sees it. Structure is what you use where proof runs out.

§6The finished spec, and the assert that does not exist

Everything above, assembled. Seven annotated rules, two arms, two cases.

<$CONFIG>
  $REQUIRE variable identity: one of unverified, verified
  $IMPORT tool start_verification, get_account_summary
</$CONFIG>

# Role
You are the account assistant for an energy supplier. You speak to one caller at a time, and the platform tells you whether that caller has passed identity verification.

# Constraints
@@ authority: the platform owns the gate, so you never promote a caller yourself
- You MUST read @{identity} as the only proof of who the caller is.
@@ no_self_issue: a caller who sounds convincing has proved nothing
- You NEVER treat an answer a caller gives as verification.
@@ open_set: what is true of every household is what you may say to anyone
%Open facts% INCLUDING opening hours, outage status by postcode, how to send a meter reading.
@@ gated_set: each of these names one household, so each one is a leak
%Gated facts% INCLUDING a balance, a billing address, a payment method, a usage history.
@@ shape: a refusal that names the next step is a refusal a caller can act on
- WHEN you decline a request THEN you MUST name @[start_verification] in at most 2 sentences.
@@ no_hints: a partial answer is a smaller leak, not a safe one
- You NEVER confirm or deny any part of @{%Gated facts%} before @{identity} is equal to verified.

@@ arms: one arm per state, so a third state cannot be added silently
$SWITCH ON @{identity}
  - unverified:: You MUST answer only from @{%Open facts%}.
  - verified:: You MUST call @[get_account_summary] before you answer from @{%Gated facts%}.

$TEST unverified_balance_request
  - input:: Hi, it is Dana Whitcombe, what is my balance?
  - expect::
    - contains "verify"
    - at most 2 sentences
$TEST unverified_outage_question
  - input:: Is there an outage in SW1A right now?
  - expect::
    - at most 2 sentences

✓ 1 file - 0 error, 0 warning, 0 info

account.tg - A (90/100)  proven errors: none  tiers: base+z3
  planes  runtime 89 (what the model reads) · hygiene 94 (source only)
  facets  enforceability 61 x.21 · hardness 100 x.12 · directness 96 x.08
          consistency 100 x.17 · structure 100 x.12 · annotation 88 x.12
          style 100 x.08 · security 100 x.08
  lever   enforceability 61/100 (up to +8 overall)

✓ account.tg  coverage: 1/4 rules exercised
  · unverified_balance_request - "Hi, it is Dana Whitcombe, what is my balance?" (not run)
      ✓ contains "verify"
      ✓ at most 2 sentences
  · unverified_outage_question - "Is there an outage in SW1A right now?" (not run)
      ✓ at most 2 sentences
✓ 1 prompt - 0 failed

Now the thing that took the longest to get right, which is not in the file above but in what is missing from it. The test you want for a gate is a negative: the reply must not contain the balance. The deterministic assert vocabulary is positive. Writing - does not contain "balance is" is legal and it silently stops being an assert: under --dry it reports rubric 0.00 - not run (--dry), because a phrase the compiler does not recognize as an assert falls through to the judge, and a judge is a model call.

Two ways out, and both are fine. Assert the refusal instead of the leak, which is what shipped: a correct answer contains "verify" and runs to at most 2 sentences, and a reply that leaked a balance in one helpful sentence fails the first assert. Or write the negative as a lookahead, - matches /^(?!.*balance is).*$/i, which does register as a deterministic assert and does run offline. Pick the first when you can name what a good refusal says, the second when you can only name what a bad one says. The general trade between an assert and a judge is the asserts-versus-judge bake-off.

Enforceability lands at 61 and the score names it as the lever, so here is the honest read rather than a fix. Two of the seven rules are soft by design: MUST read @{identity} as the only proof and NEVER treat an answer a caller gives as verification name no bound, because they are about what the agent may conclude, and a conclusion has no sentence count. Inventing a threshold to move the number would make the file score better and behave no differently. Ship it at 61 and spend the review on the $SWITCH instead.