Keep the model on your side of the wire

Most designs for checking a language model's work put a second model behind the first: a judge prompt, a rubric, a score. The judge inherits every property of the model it is judging, including the variance, the sensitivity to phrasing, and the explanation written after the fact.

DSAIL takes a different cut. The model stays where it is good, reading the document, and it stays on the caller's side of the wire. What crosses to our server is a small dictionary of typed values. What comes back is one of four words for every assertion in the ruleset. Our service never calls a language model at compile, at check, or on any tier.

This post is about how that flow is wired as an MCP server: the five calls in the authoring sequence, how each one's output becomes the next one's input, and the decisions we made along the way that other people building MCP servers might want to steal. It is written from the code as it runs today at agents.jaxon.ai.

What crosses the wire

On your side of the wire: your model, your credentials, your document. On ours: a compiled ruleset and an SMT solver (Z3) running in exact arithmetic. The claim dictionary is the only thing that crosses. The service has no document ingestion path at all, which simplifies a lot of the security story. There is nothing to leak that we never received, and what we do receive is the set of values the ruleset asked about and nothing else.

One consequence people find surprising: the caller's model also writes the DSAIL source. A user pastes their expense policy into Claude, Claude writes the ruleset, and our compiler compiles it. dsail_compile is a compiler, full stop. The instructions the server publishes say this outright: the caller's model writes DSAIL source from the person's policy, and the service compiles that source into a formal ruleset addressed by a content hash.

The five calls

The server publishes twenty tools. Five of them are the authoring sequence, shipped verbatim in the server instructions, and every model that connects reads it on initialize:

1. dsail_compile(source)         -> ruleset_hash, claim manifest, claim schema,
                                    validation contract, review text, diagnostics.
2. dsail_get_prompt_pack(hash)   -> one extraction prompt per claim, plus the
                                    schema and the exact validation rules.
                                    You run the extraction on the user's own
                                    model; this service never calls an LLM.
3. dsail_check(hash, claims)     -> every rule with each assertion's own result
                                    (TRUE / FALSE / UNKNOWN / AMBIGUOUS).
4. dsail_save_ruleset(name, src) -> a named, immutable revision (parent-linked).
5. dsail_record_approval(hash)   -> binds a human approval to that exact hash.

Here is what a small ruleset looks like. The comments beginning // @ are host annotations: invisible to the compiler, read by the service, and every one of them describes a claim rather than deciding anything.

version 1.3;
// @ask amount What is the total amount of the expense, in USD?
// @unit amount USD
// @range amount 0..1000000
declare amount as numeric;
// @ask has_receipt Is an itemised receipt attached?
declare has_receipt as boolean;
assert within_hard_cap { amount <= 25000 "USD" };
assert receipt_over_75 { Implies(amount > 75 "USD", has_receipt) };

Compile. The model calls dsail_compile(source). Server-side we normalise line endings, parse the annotations, run the DSAIL compiler for structure, and then also run the Z3 translator as a verification pass. The two front ends can disagree, and a ruleset that compiles but cannot be checked is the worst failure to discover at check time. Compile returns ruleset_hash (sha256 of the normalised source), the claim manifest, a real JSON Schema for the claim dictionary, a validation_contract saying exactly what a check will reject, review (a plain-text rendering, more on that below), and diagnostics. Compile also stores the source, so the hash is immediately usable by every later call.

On a failed compile the error carries per-line diagnostics and the full grammar guide as a hint. That is a deliberate second placement: at failure time the tool description may be thousands of tokens back in the model's context.

Prompt pack. dsail_get_prompt_pack(ruleset_hash) returns the extraction contract without the extraction. One prompt per claim:

{
  "claim": "amount",
  "data_type": "numeric",
  "question": "What is the total amount of the expense, in USD?",
  "answer_format": "a number alone expressed in USD between 0 and 1000000, or unknown",
  "unknown_rule": "unknown is a first-class answer. If you cannot determine ...",
  "undetermined_value": "unknown",
  "unit": "USD",
  "range": {"min": 0, "max": 1000000}
}

plus the claim schema, the validation contract, and three assembly notes. The model runs those prompts against the document on its own side and assembles {"amount": "120 USD", "has_receipt": false}.

Two small things in the pack earned their place by failing without them. (1) The integrity rule ("unknown is an answer, not a guess") appears both in the envelope and inside every per-claim prompt, because the per-claim prompt is what ends up in the extraction call, and a rule that lives only in the envelope is a rule the extracting model never sees. (2) Numeric bounds are trimmed to integers where possible, because "between 0 and 1000000" is followed more reliably than "between 0.0 and 1000000.0".

Check. dsail_check(ruleset_hash, claims) validates and solves in one call. Validation reports every failing field at once, as {field, expected, received}, because an extractor that has to resubmit once per bad field burns its context before it gets an answer. Then the claim values are injected into the source as let bindings, immediately before the first assertion, and Z3 evaluates.

{
  "ok": true,
  "ruleset_hash": "9f2c...",
  "unit_library_hash": "41ab...",
  "rules": [
    {"name": "within_hard_cap", "assertions": [
      {"name": "within_hard_cap", "check": "TRUE", "source": "amount <= 25000 \"USD\""}]},
    {"name": "receipt_over_75", "assertions": [
      {"name": "receipt_over_75", "check": "FALSE",
       "source": "Implies(amount > 75 \"USD\", has_receipt)"}]}
  ],
  "claims": {"bound": ["amount", "has_receipt"], "unbound": []}
}

"ok": true means the check ran. It says nothing about whether the expense passed. There is no overall verdict, and that is a designed absence rather than a gap. The first version of the wire format had ALLOW/REVIEW/DENY derived from an @effect annotation. We removed it, for two reasons. (1) A second vocabulary describing the same ruleset is a second opinion about what the ruleset says, and the two drift. (2) Choosing which of two violated assertions "really" describes a file requires knowing what each rule costs the business, which the service does not know. What a FALSE should cost is the reader's decision. The @effect annotation no longer compiles, and a test asserts that a v1 client fails loudly rather than quietly.

Save and approve. dsail_save_ruleset stores a named, immutable revision; saving over a name links the previous hash as parent. dsail_record_approval binds a person's sign-off to one exact hash, never to the name. A later revision is not covered.

Unknown, by construction

The four result words are TRUE (it holds), FALSE (it is violated), UNKNOWN (a claim it needs was not determined), and AMBIGUOUS (its evidence was contradicted). These are the same four words DSAIL returns in customer deployments, so a result means the same thing wherever it was produced.

UNKNOWN is where the design earns its keep. When the extractor submits "unknown" for a claim, that claim gets no let binding at all. The variable is left unconstrained and Z3 resolves the assertion under its declared policy (neutral answers UNKNOWN; an author can write assert x [pessimistic] { ... } or [optimistic]). Unknown is first-class because of how binding works, with no special case in the evaluator.

AMBIGUOUS is declared in the contract but cannot be produced by this service today. Reaching it needs several answers for one claim from a document, and a claim dictionary holds exactly one. It is on the wire now so the day it becomes reachable is not a wire change.

The hash is the join key, and provenance is a pair

Every object is addressed by the content hash of its source. Prompt pack, check, review, save and approval all take the same ruleset_hash, so a hash is proof of exactly which bytes produced a result. Normalisation touches only line endings and a trailing newline, never whitespace or comments, because the annotations live in the comments.

This is also why the instructions tell the model to load a stored ruleset rather than re-compile source it remembers from earlier in the conversation. Re-compiling produces a different object the moment the model's copy and the stored text disagree, and the approval follows the stored bytes.

A result is reproducible from (ruleset_hash, unit_library_hash), not the ruleset hash alone. DSAIL numerics are dimensional. amount <= 25000 "USD" against a claim of 24000 "EUR" resolves only if a converter bridges the two, and a project can add one. Same ruleset bytes, different library, different answer. So the library is hashed too, and the response to adding a converter says plainly that approvals recorded against the previous library no longer describe what the ruleset does.

We do not ship exchange rates, and the instructions carry a paragraph in capitals about it: never invent a conversion factor. A rate fixed by a contract or a density fixed by a spec is a policy decision with legal weight, and a number recalled from training would enter results as though a person had decided it. The converter tool requires an explicit factor and an attribution, and the attribution is deliberately kept out of the hashed library. Who supplied a rate is provenance about the edit; the hash must cover only the arithmetic a result depends on, or the same rate credited to two people would be two different libraries.

The grammar enforces a related rule at compile time: a united claim compared against a bare literal is refused. amount <= 25000 does not mean 25000 dollars. A bare literal adopts the unit of whatever it meets, so bind an answer of 24000 EUR and the threshold quietly becomes 25000 EUR. Zero is not exempt, because 0 degC is 32 degF.

Telling the model how to behave: instructions vs descriptions

This is the part I would most want another MCP author to read.

MCP gives a server two places to talk to the model: the server instructions returned on initialize, and a description on each tool. We keep a hard split between them. Every tool description says what the tool is for, what it takes, what it returns, and what the result means, and nothing about how the model should behave. Every operating rule (the compile, review, check order; how to handle an exhausted allowance; never reciting an internal identifier to a person) lives in the instructions.

Anthropic's connector directory policy forces this split: a tool description that instructs the model, names other tools, or pulls in outside instructions is refused at review. But it is also the right shape. A fact about a tool carries the same knowledge as a command and stays in the description ("an approval binds to the stored bytes, so re-compiled source is a different object"). The command goes upstairs. A unit test, DirectiveFreeDescriptionTests, keeps the descriptions that way.

The instructions themselves are a HEAD and a TAIL. The head describes the service and its operating rules, and an operator can swap it live on the host by writing a file; the server stats the file on every request and reassigns the SDK's instructions attribute before dispatch, which is the attribute the SDK reads when it answers initialize. That is how we A/B test the description without a release. The tail (the authoring sequence, the grammar guide, and the integrity rule) is never in the file and is always appended, so no variant can drop the part a model needs to write a ruleset that compiles.

One constraint shaped the head's first paragraph: ChatGPT weighs the first 512 characters of a server's instructions most heavily, per OpenAI's own documentation. So the confirmation gate ("confirm your restatement of the policy with the user BEFORE writing any DSAIL") and the three tool names of the authoring order sit inside that window, and a test pins them there.

Every string the model reads about the product comes from one file, phrasing.json: the lead sentence, the trigger phrases, and one problem statement per tool. Tool descriptions are composed, not written, so each one opens with its agreed problem statement and cannot open with anything else:

def _opens_with(tool_name, body):
    return "%s\n\n%s" % (phrasing.problem_statement(tool_name), body)

A lint walks the descriptions, the instructions, both READMEs, the client's skill file and every page of the docs site and fails on any near-verbatim paraphrase of an agreed phrase. The loader is standard library only, so the lint runs in a CI step that has no mcp package and no service image, and still reads the exact bytes the server publishes.

Annotations that argue

The MCP tool annotations (readOnlyHint, idempotentHint, destructiveHint, openWorldHint) are easy to fill in as boilerplate. We treated each one as a claim that had to be defended in a comment.

dsail_compile is a write, and idempotent: it stores the revision it compiled, but the store is content-addressed so repeating changes nothing. dsail_check is a write and not idempotent, because it is the one metered call. Every check spends the account's allowance, which on a paid tier is money, and that is not something a client should auto-approve silently or treat as free to repeat. dsail_add_unit_converter is marked destructive even though it deletes nothing: replacing a conversion factor changes what every later check in the project concludes and stales every prior approval. Not additive, so destructive in the spec's sense. openWorldHint is false on all twenty tools, because the service never calls out to anything, models included.

The metadata module applies titles, per-parameter descriptions, annotations and output schemas in one pass over the registered tools and raises if a published tool has no metadata or an undescribed parameter. Nothing reaches a client half-described.

The person signs what they saw

An approval bound to a hash is worth something only if the approver could read what they were signing. So dsail_compile returns review: a plain-text rendering of every question the ruleset asks and every decision it makes, in the engine's own words, including the source expression of each assertion and its unknown policy. It is derived from the manifest on every call and never stored, so it cannot drift from what it describes. The instructions tell the model to show it verbatim before recording an approval.

On clients that render MCP Apps, dsail_review(hash) opens an inline widget instead: source, claim manifest, diff against the parent revision, an exercise panel for trying claim values (with an explicit "unknown"), and the approve control. Getting that widget to behave taught us a few things.

Only three tools carry a UI, and compile is not one of them, because a client opens a frame for every call of a UI-bearing tool, and while compile carried the widget every failed iteration left a dead frame in the conversation. Compile renders nothing; the model iterates on it freely and calls review once when it succeeds.

Chat clients cache both the tool definition (which names the widget's ui:// resource) and the resource itself for the life of the connection, and in production we cannot ask users to reconnect. Hashing the resource URI defeated only the second cache; four deployed fixes stayed invisible. So the resource at the fixed address ui://dsail/review-widget.html now contains no review UI at all, only the vendored app bridge and a loader. The real UI is a separate fragment at a content-hashed URI that the shell fetches over resources/read on the same authenticated channel at open time. A UI change reaches every connected user on their next conversation. A shell change still needs a reconnect, which is why the shell is kept small and dull. ChatGPT forwards the frame's resources/read to the server and never hands the reply back, so for that host the shell also embeds the UI as an escaped JavaScript string literal.

A widget in a chat client also cannot, in general, call tools. So the approve control composes the exact dsail_record_approval arguments and hands them to the conversation as a message, and the model makes the call. The instructions are blunt about this: make exactly that call with those arguments, source byte for byte, and do not rewrite or "improve" what the widget composed, because it is the user's own action, relayed. Hosts that do proxy tools/call from the frame get direct calls; an operator setting can force the relayed path on every host, which is how we proved the widget degrades deliberately rather than by accident.

Getting a new tool list in front of a cached client

Every deploy that adds tools hits the same wall: claude.ai caches the tool definitions for the life of the connection. When we added eight team tools, a brand-new conversation still offered the twelve it had before.

The MCP spec has notifications/tools/list_changed for this, and the SDK has a convenience sender for it. The sender did not work for us, and the reason is worth knowing. Our streamable HTTP door runs stateless_http=True (the stateful default keeps sessions in process memory, so every deploy orphaned every connected client with 400 no session until they removed and re-added the connector). A stateless door never holds open the standalone GET /mcp SSE stream, and an untagged notification routes to exactly that stream. It left the server and arrived nowhere.

The fix is to tag the notification with the current request's related_request_id, so it rides the POST's own response stream. A small middleware sends tools/list_changed, resources/list_changed and resources/updated on the first request of a connection this process has not served before, which after a deploy is each user's first call. It fires on tools/list too, because a client can fetch the list and still show the model the copy it had. And the seen-mark is taken before the send, so a client that re-lists in response hears nothing the second time and the two cannot loop.

We also declare the SEP-2549 cache hints (ttl_ms=0 on tools/list and the resource methods). Measured, they are inert on every protocol version the current clients negotiate. They cost nothing and start working the day the clients move up.

One service layer, two doors, one byte stream

Every operation lives in one transport-agnostic class that takes arguments and returns a dict. The REST door and the MCP door are thin adapters over it. This is the mechanism behind an acceptance criterion we hold ourselves to: a result reached through MCP must be byte-identical to the same result reached through REST. Two door-specific implementations of "check" would drift in the third month. One core plus one canonical JSON serialiser (sort_keys=True, compact separators, ensure_ascii=False) cannot.

Payloads are pure over their inputs: no timestamps, no durations, no request ids. Identical input produces identical bytes on every replica and through both doors. The REST door returns pre-serialised canonical JSON rather than handing models to the framework's encoder, and the published response schemas are literal artifacts attached to each route, reviewable in a diff.

The MCP door funnels every tool through one closure that runs the operation on a worker thread (the engine is synchronous and a solve is CPU-bound, so one model's check must not stall every other session), catches structured errors into a shared envelope, and canonicalises. Per-request caller facts live in a contextvars.ContextVar rather than a thread local, because the thread offload copies the context into the worker and a thread local would be empty exactly where the usage event is written.

There are three transports. Streamable HTTP at /mcp behind OAuth is what claude.ai's connectors use. An in-process SSE door exists for parity tests and local clients. And a stdio server, launched by a local Claude Code, forwards to the REST door over loopback and returns the body verbatim. Same names, same descriptions, same instructions; a model cannot tell which transport it is talking to.

The stdio door forwards for a reason that cost us a day. The Z3 translator forks a solver child, and inside an MCP stdio server that fork never answers. The parent reports Execution timed out, which reads like a slow solver and is nothing of the kind. Plain process, threads, anyio.to_thread inside asyncio.run, the uvicorn REST door: all fine. MCP stdio: times out every time, including with z3 pre-imported and with a bare multiprocessing queue round-trip. Two things fell out. (1) The server warms up at startup by running one real, determinate translation, which imports z3 in the parent so every forked child inherits it. An unbound warmup would answer UNKNOWN, and UNKNOWN is exactly what a broken engine also produces; a health check that cannot fail is not one. (2) Concurrent solves are gated by a semaphore that defaults to one, because each translator child holds its own Z3 runtime.

Small edges with a bug behind each one

Claim values are compiled into DSAIL source as let bindings, which makes validation an injection boundary: a value containing " or \ could close its string and inject an assertion. The unsafe-string check is a short denylist. An earlier allowlist version refused every value in a ruleset's own enum ["n/a","ok"] vocabulary, a validator rejecting what the contract invited.

The numeric parser is stricter than the platform's, and every clause has a bug behind it. [0-9] rather than \d, because Arabic-Indic digits parsed as 5000 and came back TRUE through a value the engine never read. The exponent belongs to the number, because 5e3 once bound as 5 with unit e3. A unit may not begin with a digit, because 500 000 bound 500 with unit 000. The whole string must match, because 12x34 truncated to 12.

Duplicate assertion names are rejected at compile. The structural compiler kept assertions in a list and the translator in a dict keyed by name, so a duplicate made the manifest advertise a rule the solver never evaluated: an advertised rule that no claim dictionary could ever violate, with no diagnostic. Relatedly, if the set of assertions the manifest advertises and the set the engine answered differ in either direction, the whole check fails closed rather than returning a partial account.

Rejections are capped at fifty reported and the rest counted, because a small request naming many bad claims against long vocabularies produced a response thousands of times its own size while staying inside every published budget.

Compile also probes units. Each @unit claim is bound to a sentinel magnitude in its declared unit and translated, and the translator's own missing-converter attribution is read back. Without that probe a rule whose units cannot be bridged compiles clean, advertises itself in the manifest, and then answers UNKNOWN for every claim dictionary forever. It surfaces as a warning rather than a refusal, because refusing would make the service the arbiter of a policy decision it does not own.

Metering the one call that costs something

Only dsail_check is metered. Compiling, reviewing, saving, loading and approving are free and stay free at any limit, so a model can iterate on a ruleset without anyone watching a meter. One Jaxon Verified Unit is one rule checked against up to 1,000 characters of claim payload. Characters are counted over values, never claim names, because charging for a name would price the ruleset's vocabulary and make a rename a price change. Undetermined values are free. Rules per claim are read off the compiled graph rather than a regex over source, and that count is deliberately not published, because a billing input on the wire invites a client to compute its own price from a field we would then have to keep stable forever.

The charge lands after the compile (only the compiler knows rules times text) and before the solve, so a caller refused for an exhausted allowance has paid nothing for the parse that priced them. The ruleset's owner pays, not whoever ran it: a team's policy is the team's cost, and a member cannot move spend onto a personal allowance by switching workspace.

Try it

DSAIL is live at agents.jaxon.ai over MCP and REST. Add it as a connector in Claude or ChatGPT, or pip install dsail and run dsail init for Claude Code or Codex. The whole docs site is enumerated for agents at docs.agents.jaxon.ai/llms.txt, and every structured error the server returns carries the URL of the page that resolves it.

Paste in a policy you already apply by hand. Watch the model write the rules, compile them, and show you the review. Then hand it a document and read what the rules concluded, in their own four words.