The usual way to check a language model's work is to put a second model behind it, with a judge prompt, a rubric, and a score. Whatever is wrong with the first model is wrong with the judge too: it varies from run to run, it shifts with phrasing, and it explains itself after the fact.

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

This post walks through how that works when DSAIL is running as an MCP server behind Claude, ChatGPT, or Claude Code. It describes the code as it runs today at agents.jaxon.ai. If you build MCP servers yourself, the engineering note on our Developers hub covers the same ground in more depth.

What crosses the wire

Your document, your model, and your credentials never leave your side. Ours holds a compiled ruleset and Z3, an SMT solver working in exact arithmetic, and all it ever sees is the claim dictionary.

The service has no document ingestion path at all. That sounds like a limitation until you work through the security review, where it turns into the whole story: there is nothing to leak that we never received. What does cross is the set of values the ruleset asked about, and only those. If your expense policy asks about an amount and whether a receipt is attached, that is what our server sees. It never sees the receipt.

One consequence people find surprising is that your model also writes the DSAIL source. You paste an expense policy into Claude, Claude drafts the ruleset, and our compiler compiles it. The server's own instructions say so outright: the caller's model writes DSAIL from the person's policy, and the service compiles that source into a formal ruleset addressed by a content hash.

Five calls

The server publishes twenty tools. Five of them form the authoring sequence, and every model that connects reads it before it does anything else.

Here is a ruleset small enough to follow. Lines beginning // @ are annotations: the compiler ignores them, the service reads them, and each one 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) and gets back a ruleset_hash (the sha256 of the source), a manifest of the claims the ruleset needs, a JSON Schema for the claim dictionary, a plain-text review of what the ruleset asks and decides, and diagnostics. The source is stored, so the hash is usable by every later call.

Prompt pack. dsail_get_prompt_pack(ruleset_hash) returns one extraction prompt per claim: the question, the answer format, the unit and range, and the rule that "unknown" is a first-class answer rather than a guess. The model runs those prompts against the document on your side and assembles the dictionary: {"amount": "120 USD", "has_receipt": false}.

Check. dsail_check(ruleset_hash, claims) validates the dictionary, binds the values into the ruleset, and hands it to Z3. Back comes every assertion with its own result:

{
  "ok": true,
  "rules": [
    {"name": "within_hard_cap", "assertions": [
      {"name": "within_hard_cap", "check": "TRUE"}]},
    {"name": "receipt_over_75", "assertions": [
      {"name": "receipt_over_75", "check": "FALSE"}]}
  ]
}

"ok": true means the check ran. It says nothing about whether the expense passed, and that is deliberate (more below).

Save and approve. dsail_save_ruleset stores a named, immutable revision, and saving over a name links the previous hash as its parent. dsail_record_approval ties a person's sign-off to a single hash rather than to the name. Revise the ruleset and the approval stays with the old hash.

Four words, and no verdict

Every assertion comes back TRUE when it holds, FALSE when it is violated, UNKNOWN when a claim it depends on could not be determined, or AMBIGUOUS when its evidence contradicts itself. Customer deployments of DSAIL use exactly these four, so a result reads the same whether it came from the hosted service or from an installation inside your own walls.

There is no overall ALLOW or DENY, and there used to be. The first version of the wire format derived one from an annotation. We removed it for two reasons. (1) Two vocabularies for one ruleset amount to two opinions about what it says, and over time they disagree. (2) Deciding which of two violated assertions "really" describes a file requires knowing what each rule costs the business, and the service does not know that. The reader decides what a FALSE should cost.

UNKNOWN is where this design pays for itself. When the extractor answers "unknown" for a claim, that claim is left unbound and the solver resolves the assertion under the policy its author declared: a neutral assertion answers UNKNOWN, and an author can mark one [pessimistic] or [optimistic]. A model that could not find the receipt does not get to guess, and the service does not guess for it.

Sign what you read

Binding an approval to a hash means little unless the approver could read the thing behind the hash. So compile returns review: a plain-text rendering of every question the ruleset asks and every decision it makes, including the source of each assertion and its unknown policy. It is derived from the compiled ruleset on every call and never stored, so it cannot drift from what it describes. Before it records an approval, the model is instructed to show that review word for word. On clients that render MCP Apps, dsail_review opens the same content as an inline widget, with a diff against the parent revision and a panel for trying claim values.

A result is reproducible from the pair (ruleset_hash, unit_library_hash), not the ruleset hash alone, because DSAIL numbers carry units. amount <= 25000 "USD" against a claim of 24000 "EUR" resolves only when a converter connects the two currencies, and each project can add its own. Same ruleset, different library, different answer. When you add a converter, the response says plainly that approvals recorded against the previous library no longer describe what the ruleset does.

Never invent a rate

We do not ship exchange rates, and the instructions carry a paragraph in capitals about it. A rate fixed by a contract or a density fixed by a spec is a policy decision with legal weight. A number recalled from a model's training would enter results as though a person had decided it. So the converter tool requires an explicit factor and an attribution of who supplied it.

The grammar enforces a related rule at compile time. A claim with a unit cannot be compared against a bare number, because 25000 does not mean 25000 dollars. A bare literal adopts the unit of whatever it meets, so an answer of 24000 EUR would quietly turn the threshold into 25000 EUR. Zero gets no exception either: 0 degC and 32 degF are the same temperature.

What it costs

Only dsail_check is metered. Compiling, reviewing, saving, loading and approving are free at every tier, so a model can iterate on a ruleset without anyone watching a meter. One Jaxon Verified Unit (JVU) is one rule checked against up to 1,000 characters of claim values. The free tier includes 1,000 JVUs. Past that, JVUs cost $1 per 1,000, a tenth of a cent each.

Claim names are not counted, because charging for a name would price your vocabulary and make a rename a price change, and undetermined values are free. The charge lands before the solve, so a caller refused for an exhausted allowance has paid nothing. The ruleset's owner pays, not whoever ran it: a team's policy is the team's cost.

Running it yourself

You can run the service by connecting your agent to https://agents.jaxon.ai/mcp. It speaks both MCP and REST. In Claude or ChatGPT you add it as a connector. For Claude Code or Codex, pip install dsail followed by dsail init sets it up. The docs live at docs.agents.jaxon.ai, and every structured error the server returns carries the URL of the page that resolves it.

A good first test is a policy your team already applies by hand. The model writes the rules, compiles them, and shows you the review. Give it a document after that, and every assertion answers in one of the four words.

The engineering note on the Developers hub has the rest: how the tool instructions are written, how a new tool list reaches a client that cached the old one, and the small edges that each had a bug behind them.