Developers

DSAIL

DSAIL takes the reasoning away from the language model

Ask a language model whether a document follows a policy and it does everything in one step. It reads the document, interprets the policy, reasons from one to the other, and hands back a verdict. That step is opaque. Run it again and the answer can change, and there is no reasoning anyone can check afterward.

DSAIL splits the job. The policy is compiled once into a ruleset. At check time the model answers only small, narrow questions about the document, one per claim: what the amount is, whether a second person approved, whether a callback happened. It returns a typed value for each one, or unknown. Every rule, every condition, and every combination of rules is then evaluated by an SMT solver over those answers. The model never decides anything.

Two separate flows. Without DSAIL, a language model does extraction, reasoning, and judgment in one opaque step and returns a verdict that can change. With DSAIL, the model only answers narrow questions about the document, and an SMT solver does all of the reasoning over those answers using a ruleset compiled once from the policy. Without DSAIL Document and policy Language model extraction reasoning and judgment all in one opaque step A verdict can change when you ask again no reasoning anyone can check With DSAIL Document Language model extraction only amount? 25000 USD second approver? no callback? unknown SMT solver reasoning and judgment every rule, over those answers same answers, same result Per assertion TRUE FALSE UNKNOWN AMBIGUOUS Ruleset, compiled once from the policy
Without DSAIL, one model call does extraction, reasoning, and judgment together. With DSAIL, the model only extracts, and the solver does all of the reasoning.

Because the solver is deterministic, the same answers under the same ruleset produce the same result every time. Each assertion comes back as one of four results. TRUE means it holds. FALSE means it is violated. UNKNOWN means a claim it depends on was not determined, so the check reports that instead of guessing. AMBIGUOUS means the document supported both answers. There is no combined verdict; what a FALSE should cost is up to the system reading the result.

DSAIL

One ruleset, two ways to run it

DSAIL ships as the enterprise platform, delivered as releases into customer environments including air-gapped ones, and as DSAIL for Agents, a hosted service (how to connect). In either place a ruleset runs as a standard check: a language model answers the claim questions and the solver does the reasoning. On the enterprise platform a ruleset can also be compiled into a GRAIL, which does both halves without calling a language model at all.

One ruleset run two ways. A standard run extracts claim values with a language model and evaluates the rules with an SMT solver. A GRAIL does both halves with compiled parts: distilled encoder heads for extraction and the rule logic as a frozen neural circuit for reasoning. Written policy Ruleset written in the DSAIL language: one question per claim, and the rules over those claims Extraction Reasoning Document Language model one prompt per claim GRAIL encoder heads distilled from that model Claim values one per claim, or unknown SMT solver evaluates the rules GRAIL rule circuit rules as a frozen neural circuit Per assertion TRUE FALSE UNKNOWN AMBIGUOUS GRAIL: both halves compiled into one network that runs as a single forward pass, with no LLM calls
The top row is a standard run. The dashed row is the same ruleset compiled as a GRAIL.
The DSAIL language
The domain-specific language a ruleset is written in: typed claims (with units where they apply), each with the question that extracts it, and assertions over those claims. DSAIL generates rulesets from your policy documents, and people review and edit them before they are used.
GRAILs
Rulesets compiled for speed and cost. Distilled encoder-based classifier heads do the extraction, trained to answer the ruleset's claim questions the way the language model does, and the rule logic is compiled into a frozen neural circuit. A GRAIL evaluates a document in a single forward pass.

Shipyard

Build complete verification applications on DSAIL

Shipyard is an opinionated system for building verification applications. It treats every application as a formal workflow: a sequence of steps taken by people and automated processes, with decisions between them and at most one DSAIL ruleset checked at any step. Shipyard implements those workflows as BPMN, the standard notation for business processes, so they run on an off-the-shelf workflow engine.

You describe the workflow to a coding agent in plain language: who handles each step, which policy governs each decision, and what the possible outcomes are. Shipyard keeps the result as a single YAML definition, has DSAIL generate the rulesets from your policy documents, and wires each ruleset's claims into the workflow's decisions. The BPMN files and everything else downstream are generated from that one definition.

The work climbs a ladder, one rung at a time, and nothing moves up without your confirmation. Each rung has its own command, from /shipyard-init to /shipyard-promote, and a status command tells you which rung the evidence supports.

The Shipyard ladder: inputs, specs, wired, validated, simulated, promoted. A promoted workflow exports as BPMN and DMN files, a runnable stack, or a full application. L0 Inputs policy documents and an app brief L1 Specs workflow skeleton and ruleset specs L2 Wired rulesets published, real claims wired in L3 Validated paths, types, and decisions checked L4 Simulated every outcome hit, live DSAIL runs Promoted frozen and committed exports as BPMN and DMN portable workflow files Runnable stack Spiff engine, OIDC, DSAIL Full application web front end, per-role tasks
The authoring ladder and the three export targets. Going back down a rung is allowed and expected; Shipyard names the change and asks again.

A promoted workflow exports as portable BPMN and DMN files, as a Docker Compose stack that runs it on the Spiff workflow engine with a bundled OIDC identity provider and DSAIL connectors, or as a complete application with a Next.js front end where each person sees the tasks assigned to their role. Re-exporting after a change refreshes the generated parts and leaves your UI customizations alone. The same bundle deploys to an isolated environment per tenant.

Two rules shape what Shipyard lets through. First, an unknown claim is the normal case, since most rules do not apply to most documents, so every decision that routes on a claim needs a fallback branch and validation refuses a workflow that could dead-end on an unknown. Second, a simulation fed mock claims proves shape and routing and nothing more, so promotion requires at least one live DSAIL run for every ruleset the workflow calls.

DSAIL for Agents

The same engine over MCP and REST

DSAIL as a hosted MCP server and REST API, for both chat and code surfaces. Add it as a connector in a chat assistant and check documents against a policy in conversation, or give a coding agent the same tools while it builds. Your model stays on your side of the wire: it reads the document and answers the claim questions, and only those answers cross to the service. The service has no way to receive a document and never calls a language model.

The document and your model stay on your side. Only the claim values cross to agents.jaxon.ai, where a compiled ruleset and an SMT solver produce per-assertion results that go back to your model. Your side chat assistant or coding agent, your document, your model agents.jaxon.ai compiled ruleset and SMT solver, no language model Document Your model reads the document and answers each claim question Compiled ruleset + SMT solver binds the values, solves Per-assertion results TRUE / FALSE / UNKNOWN / AMBIGUOUS {"amount": "25000 USD", "new_payee": true} only the claim values cross
What crosses the wire. The results come back to your model, which can explain them in the conversation or act on them in code.

A small ruleset, as a model would write it from a payments policy. The // @ask lines are the claim questions; the compiler ignores them and the service turns them into extraction prompts for your model.

version 1.3;

// @ask amount What is the amount of the wire transfer, in USD?
// @unit amount USD
declare amount as numeric;

// @ask second_approver Has a second person approved the transfer?
declare second_approver as boolean;

// @ask new_payee Is this the first transfer to this payee?
declare new_payee as boolean;

// @ask callback_done Were the payee's bank details confirmed by a phone callback?
declare callback_done as boolean;

assert under_single_limit { amount <= 250000 "USD" };
assert dual_approval_over_10k { Implies(amount > 10000 "USD", second_approver) };
assert callback_for_new_payee { Implies(new_payee, callback_done) };

Checked against a $25,000 transfer to a new payee, with no second approver and nothing in the document about a callback:

AssertionResult
under_single_limitTRUE
dual_approval_over_10kFALSE
callback_for_new_payeeUNKNOWN (the callback was never determined)
  • MCP server https://agents.jaxon.ai/mcpStreamable HTTP, signed in with OAuth. Add this URL as a connector in a chat assistant, or register it with a coding agent.
  • Connect itStep-by-step setup for claude.ai, ChatGPT, Claude Code, and Codex, or three curl calls against the REST API.
  • DSAIL Python clientA REST client for codebases that call DSAIL. A coding agent can use it to build a standalone application that runs its own DSAIL checks, with no agent involved once it ships. Install with pip install dsail; the source is on GitHub.

DEEM

Check what a model does when it changes

Retraining a model, swapping in a new version, or changing a prompt can change its behavior in ways a single accuracy number hides. A model can hold its headline score while it gets worse on a rare class, or forgets cases it used to handle. DEEM validates model behavior against your own standards and compares versions side by side, so a shift like that shows up before the new model replaces the old one.

The standards are written in AISL, the AI Specification Language, which sits underneath DEEM the way the DSAIL language sits underneath DSAIL. An AISL program declares the models under test and their settings, loads datasets, queries the models, computes metrics such as accuracy, F1, precision, and recall, and groups them into evaluations with pass or fail conditions. It also records the lineage between models, datasets, and metrics, so every result traces back to what produced it.

DEEM runs the current model and a candidate model through the same AISL specification of datasets, metrics, and pass or fail conditions, then compares the results side by side so a behavior shift shows up before the candidate replaces the current model. Current model in production today Candidate model retrained, swapped, re-prompted AISL specification the same datasets and prompts metrics: accuracy, F1, precision, recall pass or fail conditions you set lineage from every result back to the model and data that produced it EXAMPLE RESULT Condition Current Candidate accuracy above threshold Pass Pass F1 on the rare class Pass Fail recall on older cases Pass Fail Accuracy still passes. Two behaviors regressed. Both models run against one specification, so any difference in the results comes from the model.
One specification, two models. The example result is illustrative.

An AISL program from the public specification: one model, ground truth and predictions from a JSON file, and four metrics, with accuracy held to a threshold.

declare gpt4 as model {
    model_name = "chat",
    temperature = 0.7,
    max_tokens = 150
}

declare data_file as file { name = results, type = json }
declare ground_truth as dataset { data_file, key = y_true }
declare predictions as dataset { data_file, key = y_pred, model = gpt4 }

let y_true = flatten(ground_truth);
let y_pred = flatten(predictions);

declare eval as performance {
    metric[accuracy](y_true, y_pred) > 0.9 ? "Pass" : "Fail",
    metric[f1_score](y_true, y_pred),
    metric[precision](y_true, y_pred),
    metric[recall](y_true, y_pred)
}
  • AISL specificationSyntax, data types, declarations, built-in functions, and the grammar reference, published with our government customer's agreement. Source on GitHub.

Docs and APIs

Documentation and API reference

DSAIL has two documentation sites. docs.jaxon.ai covers the enterprise platform, which you install and run in your own environment. docs.agents.jaxon.ai covers DSAIL for Agents, the hosted service, which offers a lighter-weight subset of the platform's functionality.

Enterprise platform

docs.jaxon.ai
  • Platform documentationInstalling, operating, and building on DSAIL: getting started, concepts, tutorials, administration, and reference.
  • Getting startedThe core workflow from documents to rulesets to runs, with screenshots.
  • System requirementsWhat a deployment needs from its host and network.
  • REST APIEvery endpoint of a deployment, corpus routes included, with authentication and schemas. Each deployment also serves its live OpenAPI document at /api/openapi.json.
  • DSAIL language referenceTypes, units, assertions, and the grammar rulesets are written in.
  • Release notesWhat changed in each release, newest first.

DSAIL for Agents

docs.agents.jaxon.ai
  • Hosted service documentationWritten for agents first, and served as Markdown as well as HTML: guides, one page per error code, and comparisons with OPA, Cedar, and guardrail frameworks.
  • From policy text to a compiled rulesetWhat DSAIL source looks like on the hosted service, how the annotations describe claims, and what the compiler refuses.
  • REST APIThe hosted routes under https://agents.jaxon.ai/v1, rendered from the service's OpenAPI document, which a coding agent can read to generate a client in any language.
  • MCP tools referenceEvery tool the MCP server publishes, with the descriptions and arguments a connected model sees.

Reference

Reference documents

Enterprise platform

docs.jaxon.ai

DSAIL for Agents

docs.agents.jaxon.ai
  • Data handlingWhat the hosted service stores, what it never does with it, and what it must never be sent.
  • How a check reports its resultWhy every assertion gets its own result and there is no combined verdict.
  • UNKNOWN is an answerWhat happens when a document does not settle a fact, and why a missing value never reads as a pass or a failure.
  • No model in the loopExtraction on your model, the check on a solver, and what keeping them apart buys you.

Engineering notes

Design records and post-mortems

  • Keep the model on your side of the wire: how the DSAIL MCP server is wiredGreg Harman, September 2026A walk through the five calls a model makes to write and check a ruleset, and the decisions underneath them. Covers why an approval binds to a content hash instead of a name, how we got claude.ai to see new tools from a stateless HTTP server, and why the check is the only call we meter.