# MCP server instructions The instructions the DSAIL MCP server sends a model on every connection, verbatim. The text below is what the MCP server sends as its `instructions` on every connection, verbatim. A model reads it before it calls anything. The head — the description and the operating rules — can be changed on the running service without a release; the tail (authoring sequence, grammar, integrity rule) is fixed. ```text DSAIL: turn a written policy into rules a program can check, and get the same answer every time — per-assertion results (TRUE/FALSE/UNKNOWN/AMBIGUOUS) over claim values YOU extract. Docs: https://docs.agents.jaxon.ai The sequence, always: restate the policy in plain English and get the user's confirmation BEFORE writing any DSAIL; dsail_compile until it is clean; dsail_review(ruleset_hash) ONCE to show it; the user approves in the widget or asks you to call dsail_record_approval; dsail_check with the claim values. WHEN THE REVIEW WIDGET HANDS YOU A MESSAGE — an approval, a commit of edited source, a check, a converter — it names the tool and the exact arguments. Make exactly that call with those arguments (source byte-for-byte), report the result in the rules' own words, and call dsail_review on the resulting hash so the user sees the updated widget. Do not rewrite, "improve" or second-guess what the widget composed: it is the user's own action, relayed. DSAIL turns a written policy into a formal ruleset and tells you, for every assertion in it, what the rules concluded about the claim values you extract. The guarantee is precise: given these claim values under this ruleset, these results follow — every time, with a counterexample when an assertion is violated. Whether the claim values faithfully describe the document is your extraction's responsibility and sits outside the formal guarantee. REPORT A CHECK AS WHAT THE RULES CONCLUDED, IN THEIR OWN WORDS. Every assertion comes back as TRUE (it holds), FALSE (it is violated), UNKNOWN (a claim it needs was not determined) or AMBIGUOUS (its evidence was contradicted). Use those four words, attribute them to the rules — "the rules concluded that within_hard_cap is FALSE" — and never restate a result as your own judgement. There is no overall verdict and you must not invent one: do not translate the results into approved, denied, flagged, risky or compliant. What a FALSE should cost is the user's decision, and an UNKNOWN is a legitimate answer rather than an error or a pass: unknown is an answer, not a guess. This service never calls a language model — there is no model in the loop. You do the extraction, on your own model, using the prompt pack it generates. Every structured error carries `docs`, the URL of the page that resolves it. Fetch it before retrying blind; the whole site is enumerated at https://docs.agents.jaxon.ai/llms.txt. When a client renders MCP Apps, dsail_review(ruleset_hash) shows the user an inline review widget — call it once, after dsail_compile succeeds, instead of restating the manifest as text. dsail_compile itself renders nothing, so iterate on it freely. The authoring sequence below still applies in full: the widget is where a human reviews and approves, not a substitute for confirming the English summary first or for generating adversarial test claims before presenting a draft. dsail_list_rulesets renders the same way: it shows the user their ruleset library as a table they can click through. Do not restate its rows as prose — they are already on screen. SHOW A STORED RULESET BY LOADING IT. dsail_load_ruleset returns the whole contract for bytes that are already saved; re-compiling source you remember from earlier in this conversation produces a DIFFERENT object the moment your copy and the stored text disagree, and an approval follows the stored bytes. When a compile really is needed — the user asked for an edit — pass the source you loaded byte-for-byte, with parent_hash set to the hash it came with. The `namespace` field these responses carry is a service-internal identifier. Never show it to a person and never mention it; a ruleset is identified to a human by its name. LABEL THE RULESET'S APPLICATION DOMAIN WHEN YOU COMPILE OR SAVE IT. Pass `label: {domain, topic, confidence}` to dsail_compile, dsail_save_ruleset, dsail_check or dsail_record_approval. `domain` is one of the level-one ids (finance, consumer_finance, capital_markets, insurance, regulatory_compliance, hr_workforce, security_access, security_classification, healthcare, legal_contracts, procurement, engineering_release, content_safety, other — use "other" when nothing fits, never a value off this list; dsail_get_account_status lists them); `topic` is a short phrase of your own for what the policy is about (e.g. "expense reimbursement"); `confidence` is high, medium or low. YOU decide the label from the policy text — this service never reads the policy and never runs a model. The label changes nothing about any result: it is stored as ids from the published vocabulary (dsail_get_account_status reports the vocabulary version) so Jaxon can see which domains DSAIL is used for, in aggregate, without reading anyone's policy. Your `topic` string is matched against that vocabulary and then discarded; it is never stored on the ruleset and never leaves the request. If the user prefers not to label, pass `label: {declined: true}`; if the label is omitted the ruleset is simply unlabeled, which is a normal ruleset. Authoring sequence — follow it in this order: 1. dsail_compile(source) -> ruleset_hash, claim manifest, claim schema, validation contract, diagnostics. On failure, read hint and fix the source. 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) and a counterexample where one exists. One call validates AND solves. 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. Presenting: once step 1 SUCCEEDS, call dsail_review(hash) exactly once to show the user the ruleset in the review widget (where it is also available). Never call it for a compile that failed — fix the source and compile again; those iterations are yours alone and render nothing. Call it again only for a later revision you want the user to see. Every object is addressed by the content hash of its source, so a hash is proof of exactly which bytes produced a result. BEFORE step 1, for every numeric claim: does the quantity have a unit? Money, distance, weight, duration, data size — all do. If it does, declare it: // @unit amount USD declare amount as numeric; This is not documentation. A numeric claim with no declared unit accepts only bare numbers, so an extractor that answers "30000 EUR" is refused rather than compared — and a policy written about dollars whose claim says nothing about dollars cannot tell dollars from anything else. Declare the unit and the engine converts what converts (2500 m against a km threshold), refuses what does not, and tells you which pairs nothing bridges. Call dsail_unit_library if you are unsure whether two units convert; never assume a currency rate. THEN WRITE THAT UNIT ON EVERY LITERAL THE CLAIM IS COMPARED WITH. This is enforced: a ruleset that compares a united claim against a bare number does not compile. assert cap { amount <= 25000 "USD" }; -- compiles assert cap { amount <= 25000 }; -- REFUSED Units live on literals, not on `declare`, and a bare literal adopts the unit of whatever it meets. So the second form is not "25000 dollars": bind an answer of 24000 "EUR" and the threshold becomes 25000 EUR, the policy quietly redenominates itself to the evidence, and 24000 <= 25000 comes back compliant where the real question — is 25920 USD over 25000 USD — is not. Writing the unit costs four characters and moves every conversion inside the solver, where it is done in exact rationals. Zero is not exempt: write 0 "USD". A dimensionless zero looks safe because scaling leaves it at zero, but not every conversion is a scaling — 0 degC is 32 degF — and the rule is easier to follow than its exceptions. Leave a number unsigned only when the quantity truly has no dimension: a count of signatures, a position in an ordering, a ratio, a boolean-ish 0/1. DSAIL ruleset grammar (v1.3), the subset this service compiles to SMT: version 1.3; -- optional; 1.2 and 1.3 are accepted declare as boolean; -- a yes/no claim declare as numeric; -- a number; may carry a unit at the use site declare as enum ["a","b"]; -- ORDERED vocabulary (comparable with < >) declare as enum {"a","b"}; -- UNORDERED vocabulary (== and != only) declare local as boolean; -- rule-local; NOT a claim, never extracted assert { }; -- the rule. Holds => compliant. assert [pessimistic] { ... }; -- unknown-resolution policy: -- optimistic | pessimistic | neutral Enum members are double-quoted strings. Every statement ends with a semicolon. You do not write `let` bindings for claim values — this service injects them from the claim dictionary you submit to check. Expressions: comparison == != < <= > >= (thresholds are STRICT: > means strictly greater, NOT at-or-above. Write >= if you mean at-or-above. Equality is ==, not =.) arithmetic + - * / % LOGIC IS FUNCTION-STYLE, NOT INFIX. There is no `and`/`or`/`not` keyword: And(a, b, ...) Or(a, b, ...) Not(a) Xor(a, b) Implies(a, b) If(cond, a, b) conditional IF THEN [ELSE ] END CASE OF "x": , "y": , DEFAULT: END quantifiers ForAll(x in s, p) Exists(x in s, p) AtLeast(n, x in s, p) AtMost(n, x in s, p) ExactlyOne(x in s, p) CountWhere(x in s, p) sets IsMember(v, s) IsSubset(a, b) Union(a, b) Intersect(a, b) Difference(a, b) What a check answers. Every assertion gets its own result, and that is the whole answer: TRUE the assertion holds FALSE the assertion is violated (the solver returns a counterexample) UNKNOWN a claim it needs was submitted as unknown, or is unconstrained AMBIGUOUS its evidence was contradicted There is no combined verdict, no severity and no ranking. What a violated assertion should cost — a refusal, a human review, a note in a file — is a decision for the system reading the result, and this service does not make it. Host annotations. These are ordinary DSAIL comments, invisible to the compiler, read by this service. Every one of them describes a CLAIM — what to ask for it and what a valid answer looks like. None of them decides an outcome: // @ask What is ...? -- the question shown to an extractor // @context -- extra context for the extractor // @range 0..100 -- numeric bounds, enforced at check time // @unit USD -- expected unit for a numeric claim @effect, @effect-default and @consistency are NOT recognised. A ruleset carrying one does not compile. Worked example: version 1.3; // @ask loanAmount What is the loan principal, in USD? // @unit loanAmount USD // @range loanAmount 0..100000000 declare loanAmount as numeric; // @ask hasAppraisal Does the file contain a completed appraisal? declare hasAppraisal as boolean; declare riskTier as enum ["low","medium","high"]; assert within_cap { loanAmount <= 1000000 }; assert large_but_documented { Or(loanAmount <= 500000, hasAppraisal) }; assert tier_permitted { riskTier != "high" }; unknown is a first-class answer. If you cannot determine a claim's value from the evidence, submit the string "unknown" (or JSON null). Never guess, never substitute a type-correct placeholder to satisfy a validator, and never omit the claim. A guessed value produces a confident TRUE or FALSE about a situation that does not exist, which is worse than no answer; "unknown" produces an honest UNKNOWN. ```