Evoduce API

Evoduce checks changes to a taxonomy (categories, rules and terms) and proves whether each one is consistent with your rules. You send the vocabulary and a proposed term; it either proves the term fits or returns the rules it breaks with a concrete conflict. Under the hood it's the neurosymbolic-evaluator library on the Z3 SMT solver, so a pass is a proof, not a score.

Quickstart

Sign up with an email to get a free API key (10,000 requests a month), and export it as EVODUCE_API_KEY. Then save a vocabulary as vocab.json:

{
  "name": "spatial_relations",
  "axes": {
    "duration": {"values": ["absolute", "temporary"]},
    "type":     {"values": ["contact", "proximity", "containment"]}
  },
  "rules": [
    {"type": "AXIS_COVERAGE"},
    {"type": "SYMMETRIC_IS_SELF_INVERSE"},
    {"type": "REQUIRES_INVERSE"},
    {"type": "NO_DUPLICATE"}
  ],
  "predicates": {
    "touching": {"duration": "temporary", "type": "contact", "symmetric": true}
  }
}

Then verify a proposal:

curl -s https://$EVODUCE_HOST/v1/verify \
  -H "Authorization: Bearer $EVODUCE_KEY" \
  -H "Content-Type: application/json" \
  -d "{\"vocabulary\": $(cat vocab.json),
       \"proposal\": {\"name\": \"resting_on\", \"duration\": \"temporary\", \"type\": \"contact\"}}"

{
  "sat": false,
  "reason": "[REQUIRES_INVERSE] Non-symmetric predicate 'resting_on' has no inverse declared. ...",
  "violated_rules": ["REQUIRES_INVERSE"],
  "counterexample": {
    "proposal": "resting_on",
    "axes": {"duration": "temporary", "type": "contact"},
    "violations": {"REQUIRES_INVERSE": "..."}
  },
  "compliance": 1.0,
  "unmet_soft": []
}

Add "inverse": "supports" (or "symmetric": true) and the same call returns "sat": true.

SDKs

Both clients are thin, typed wrappers over the HTTP API. They read EVODUCE_API_KEY and EVODUCE_BASE_URL from the environment.

Python

pip install evoduce

from evoduce import Client, EvoduceError

with Client() as nse:
    r = nse.verify(vocab, "resting_on", duration="temporary", type="contact")
    r.sat, r.violated_rules, r.counterexample

    grown = nse.accept(vocab, "resting_on", inverse="supports",
                       duration="temporary", type="contact").vocabulary
    nse.optimize(vocab, proposals, content_value={"x": 5}).admitted
    nse.prove(grown).sat, nse.audit(grown).passed

Axis values are keyword arguments. A neurosymbolic_evaluator.Vocabulary object works anywhere a dict does.

TypeScript

npm install evoduce

import { Client, EvoduceError } from "evoduce";

const nse = new Client();                    // or { apiKey, baseUrl }
const r = await nse.verify(vocab, { name: "resting_on", duration: "temporary", type: "contact" });
const { vocabulary: grown } = await nse.accept(vocab, { name: "resting_on", inverse: "supports", duration: "temporary", type: "contact" });

No dependencies; runs on Node 18+, Deno, Bun, edge runtimes and browsers. In both SDKs, a non-2xx response raises EvoduceError with status, detail and a retry-after value.

Authentication & limits

Send your key as a bearer token: Authorization: Bearer sk_…. Requests without a key use the anonymous tier, which is how the playground works.

Request bodies are capped at 256 KB. Each check has a 10 s budget; a call that runs past it returns 504.

Vocabulary format

Every request carries the full vocabulary, so your vocabularies are never stored server-side (what is kept, and where, is listed under where data lives). The format is the one Vocabulary.from_dict reads, and /v1/accept returns the same shape.

A proposal is a flat object: name, optional symmetric, inverse, metadata and aliases, and every other key is an axis value.

Rule types

CUSTOM rules are Python callables and can't be submitted over HTTP. They're available on Enterprise deployments.

Strict vs graded

A rule with no weight is a hard invariant: one violation makes the result UNSAT. A rule with a weight is a soft preference. Strict endpoints ignore soft rules. The graded endpoints let hard rules gate and turn soft rules into a compliance score (satisfied soft weight ÷ total soft weight).

{"type": "METADATA_REQUIRED", "name": "PREFER_REVIEWED", "metadata_key": "reviewed", "weight": 3}

Use cases

A use case is what you sign up to do. It has a type, and the type sets its configuration: how a name two terms share is handled, how sure a model must be before its answer is used, what the service learns, and where each kind of data lives. You pick the type when you sign up and can add more use cases later, each with its own key.

Which use case a call runs under. A key made for a use case carries it on every call. Any of your keys can name another of your use cases with the header X-Evoduce-Use-Case: <name>. A call with neither, or with no key, runs on the standard settings: every default in the tables above, with aliases: settle. Every endpoint works under every type; the type only sets the defaults.

No key needed. Returns each type with its config, what each setting means, its storage list, and store: whether the durable store is on.

Body: {name, type, config?, key?}. name is lowercase letters, digits, - and _. config overrides any setting the type lists. key is "new" (the default: a new key bound to the use case, returned once as api_key), "current" (bind the calling key) or "none". At most 20 use cases per account.

Your use cases, each with its settings in force, your overrides, its storage and the prefixes of the keys bound to it. GET /v1/usecases/{name} returns one.

Body: {config: {setting: value}}. Changes take effect within 15 seconds. A null value restores the type's default.

Shared names

A name sends a term to exactly one predicate, by exact match. So when two predicates list the same alias, something has to decide which one it means. The aliases setting of the call's use case says what:

A vocabulary that says so itself is left alone under every setting: one that declares ALIAS_UNAMBIGUOUS in its rules gets the strict check, and one that carries default_rules gets what it asked for. An entry in the vocabulary's own aliases map always wins over a remembered choice.

# response to /v1/audit, /v1/prove, /v1/verify, /v1/accept, /v1/optimize, /v1/evolve under "settle"
"aliases_settled": {
  "next to": {"term": "near", "candidates": ["touching", "near"], "by": "order"}
}

by is order (declared last), you (you named the owner), or kept (a proposal asked for a name that already had an owner; not_taken_by lists the proposals). Under candidates, an evolve result for such a term carries "alias": {"candidates": [...], "picked_by": "tier0" | "claude"}, or comes back needs_review when no tier is sure.

What has been remembered for a use case, per vocabulary name: settled (name, owner, how it was chosen, when) and picks (how often each candidate was picked). Add ?vocabulary= for one vocabulary.

Body: {vocabulary, alias, term}. Names the owner yourself. It is used from the next call on, whenever that predicate is among the ones claiming the name.

/v1/prove covers the structure of the whole vocabulary: axes and inverses. Per-predicate rules such as ALIAS_UNAMBIGUOUS and METADATA_REQUIRED are checked by /v1/audit. Under strict, a vocabulary with an open shared name passes prove and fails audit.

Where data lives

Each type of use case keeps different things, in different places. There are three stores. The durable store is Redis with its append-only log on and no expiry on these keys; it holds what the service has learned for you and must survive a restart. The cache is the same Redis with an expiry on every entry; losing it costs time, never an answer. The database is Postgres.

Callers without a key have nothing remembered. If the durable store is unreachable, calls still succeed: a shared name is settled by order for that call and nothing is recorded. GET /healthz and GET /v1/usecases/types report the store's state under store; durable is true only when the log is on and the server will not evict keys that have no expiry.

Endpoints

Strict check of one proposal. Body: {vocabulary, proposal}. Returns a VerificationResult:

Same body and result as /verify. Hard rules gate the result, and weighted rules fill in compliance and unmet_soft.

Verifies the proposal and, if SAT, adds it. Returns {result: VerificationResult, vocabulary: object | null}. Persist the returned vocabulary yourself; nothing is stored on our side.

MaxSMT batch admission. Body: {vocabulary, proposals: Proposal[], content_value?: {name: int}}. Admits the maximum-weight consistent subset of competing proposals.

{
  "admitted": ["x"],
  "rejected": ["x"],
  "extensions": [
    {"name": "x", "admitted": true,  "compliance": 1.0, "hard_violations": [], "unmet_soft": []},
    {"name": "x", "admitted": false, "compliance": 0.0, "hard_violations": [], "unmet_soft": ["PREFER_REVIEWED"]}
  ],
  "objective": 8
}

A consistency proof over the whole vocabulary. Body: {vocabulary}. Returns a VerificationResult.

Re-verifies every predicate. Returns {predicates, passed, failures: [{predicate, ...VerificationResult}]}.

Lists the rule types a submitted vocabulary may declare.

Decision gateway

Send typed decisions to POST /v1/systemone. Its request and response follow the Jev-compatible shape, whether Jev or the configured open model answers. Evoduce answers each question from the cheapest source that can settle it:

Facts come from state when it's a JSON object (or a JSON string), or from a separate facts field when state is prose. score questions always go to the model. A plain-text state with no facts goes to the model.

Headers: Authorization: Bearer evd_… (your Evoduce key; optional, see below), X-Upstream-Key (your Jev key; optional when the server has a configured provider), and X-Evoduce-Upstream: auto (default: your Jev key, else the server's model), jev, open (the server's open model), or none (rules only). The body follows Jev's API reference: {state, questions, model?}; state and instructions may be strings or objects, and a structured state keeps its object or array form when forwarded. Evoduce also accepts optional facts for prose state. Counts as one request.

Inline rules. A question may carry rules in the decision-rule format; they are used instead of your policy for that question and stripped before anything goes to a model. Without a key the gateway still works at the anonymous rate, with inline rules and the server's model, but has no policies and learns nothing. Drop-in: Jev's own SDK accepts a TYPESAFE_BASE_URL; point it here with your Evoduce key as TYPESAFE_API_KEY and your code is unchanged. See the examples.

{
  "model": "jev-1.13.0",
  "answers": {
    "route":  {"type": "choice", "choice": "billing", "confidence": 1.0, "probabilities": {"billing": 1.0, "sales": 0.0}},
    "urgent": {"type": "noul", "noul": 0.93}
  },
  "usage": {"input_tokens": 100, "output_tokens": 1},
  "evoduce": {
    "sources": {"route": "rules", "urgent": "model"},
    "details": {"route": {"rules": ["refunds"]}},
    "upstream_calls": 1,
    "learned_pending": {"urgent": 2}
  }
}

If two of your rules demand different answers for the same facts, neither is used: the question goes to the model and details names the conflicting rules. If no provider is configured and no upstream key is available for a question rules can't settle, you get 503 naming it.

Use an NS vocabulary in a typed Choice

Add an Evoduce vocabulary to a choice question. Its predicate names become the exact criteria option keys. Evoduce makes a short option description from each predicate's axis values, then removes vocabulary before calling the configured provider. You can provide your own criteria descriptions if their keys match the predicate names exactly.

{
  "state": {"ticket": {"category": "refund", "amount": 40}},
  "model": "jev-latest",
  "questions": {
    "route": {
      "type": "choice",
      "instructions": "Which department should handle this ticket?",
      "vocabulary": {
        "name": "ticket_departments",
        "axes": {"department": {"values": ["billing", "support"]}},
        "rules": [{"type": "AXIS_COVERAGE"}],
        "predicates": {
          "billing": {"department": "billing", "symmetric": true},
          "support": {"department": "support", "symmetric": true}
        }
      }
    }
  }
}

The forwarded question uses Jev-compatible Choice syntax: {type: "choice", instructions, criteria: {billing: "department: billing", support: "department: support"}}. Jev is one provider; the configured open model adapter accepts the same question shape. A Choice has at most 255 options. Keep the same question id for learned decision rules; confident model choices become observations for that policy, and a rule can later settle the question without a model call.

The vocabulary defines which answers are allowed and its structural rules govern additions through /v1/verify and /v1/accept. A model choice is a judgment, not a proof that it is the correct label. The decision rules are checked separately against the facts in state.

Decision rules

A policy is the set of rules behind one question id. Each rule says: when these facts hold, the answer is this.

{"name": "big deals",
 "when": [{"var": "category", "op": "==", "val": "quote"},
          {"var": "amount",   "op": ">=", "val": 10000}],
 "then": "sales"}

op is one of ==, !=, <, <=, >, >= or in (with a list). Nested facts use dotted names (customer.vip). For a yes/no question, then is true or false. A rule whose condition depends on a fact the request didn't include still applies when the solver can show the answer is forced regardless.

Learning

Every confident model answer over structured facts is an observation. A pattern that holds in at least min_support observations (default 5) and fails in none becomes a learned rule: one fact, a numeric threshold, or two facts together. A later model answer that contradicts a learned rule withdraws it. Each policy's learning mode is:

A learned rule is a generalisation of what the model did, so it can be wrong where the model would have decided differently. Your own rules are never changed by learning; if a learned rule contradicts one of yours on some facts, that's a conflict and the model decides.

Every question id this account has rules or observations for, with counts.

{question_id, rules, learned, learning, min_support}. Learned rules carry learned.support.

Body: any of {rules, learning, min_support}; unspecified fields keep their value. Rules are checked for shape and type consistency.

Body: {indexes?: [0, 2]}. Moves the given learned rules (all, if omitted) into the policy's own rules.

Evolve

The endpoints above check a change you already have. /v1/evolve finds the changes: give it text or a list of candidate terms, and it works out which are already covered, which are new, and where each new one belongs. Nothing is added until it has been proven consistent with your rules.

It uses up to two model tiers, cheapest first:

Tier 0 is any typed-decision model: Jev from TypeSafe AI, or an open model served through an OpenAI-compatible endpoint (Ollama, vLLM and similar). With an open model, each question is posed as a lettered list and the option probabilities are read from the model's own next-token distribution, so they are what the model assigned rather than a number it wrote down; a server that can't return those falls back to a self-reported estimate and the answer says so. GET /v1/evolve/tiers reports which tiers a server has and which tier-0 provider. With only tier 0, send terms; reading text needs Claude.

Body: {vocabulary, text | terms, auto_accept?: true, max_repair_attempts?: 3, min_confidence?: 0.7}. Send exactly one of text (up to 20,000 characters) or terms (up to 25). Requires an API key and counts as 10 requests; limited to 10 calls a minute per key.

{
  "results": [
    {"term": "touching", "action": "mapped", "canonical": "touching", "trace": []},
    {"term": "near", "action": "accepted", "canonical": null,
     "repair": {"axes": {"duration": "temporary", "type": "proximity"}, "symmetric": true, "inverse": null},
     "verification": {"sat": true, "reason": "...", "violated_rules": []},
     "trace": [{"step": "adjudicate", "tier": "tier0", "confidence": 0.93},
               {"step": "repair", "tier": "claude", "escalated_because": "axis type: confidence 0.41 is below 0.7"}]}
  ],
  "accepted": ["near"],
  "vocabulary": { ... },
  "tiers": {"tier0": true, "claude": true},
  "usage": {"tier0": {"calls": 2, "escalations": ["repair: ..."]}, "claude": {"llm_calls": 1, "input_tokens": 812, "output_tokens": 96}}
}

action is one of mapped (an existing term or a synonym of one), accepted, rejected (no proposal passed the proof check), noise, out_of_scope, needs_review (tier 0 was unsure and there is no tier above it) or declined. vocabulary is the updated vocabulary when anything changed, otherwise null. trace shows which tier settled each step and why it escalated. For long inputs, submit {"op": "evolve", ...} to /v1/jobs.

Background jobs

Synchronous calls get a 10 s solver budget, which is plenty for verify and audit at any size. A full prove grows quickly with vocabulary size: about 0.5 s at 100 terms and over 10 s at 1,000. For large vocabularies, run prove, audit or optimize as a job. Jobs run on dedicated solver workers with a 60 s budget, and nothing is held open while they run.

Body: {op: "prove" | "audit" | "optimize", vocabulary, proposals?, content_value?}. Input is validated before it's queued, so a bad vocabulary still gets an immediate 422. Returns 202 with a job and a Location header, or 200 with the finished job if the result is already cached. Each submission counts as one request against your quota.

Returns {id, op, status, created_at, started_at?, finished_at?, result?, error?, cache_hit?}. status is queued, running, succeeded or failed. On failure, error.code is one of:

Polling doesn't count against your quota but is limited to 120 per minute per IP. Job IDs are unguessable and act as the credential for reading the job. Jobs expire after 24 hours.

# Python
result = nse.prove_in_background(vocab)            # submit + wait
job = nse.submit_job("optimize", vocab, proposals=[...]); nse.wait_job(job)

// TypeScript
const result = await nse.proveInBackground(vocab);
const job = await nse.submitJob("audit", vocab); await nse.waitJob(job);

Caching

prove, audit and optimize results are cached for 7 days, keyed on a hash of the input and the exact evaluator build. Top-level keys that start with _ (such as _comment) are ignored for the key. Synchronous responses carry X-Evoduce-Cache: hit | miss. A new evaluator release can never return a stale proof, and timeouts are never cached.

Account endpoints

These back the dashboard. They take a developer key as the bearer token and don't count toward your quota.

Body: {email, use_cases?}, where use_cases is a list of {type, name?, config?}: one entry per thing you are building (see use cases). Each becomes its own subproject with its own key, settings and data; two of the same type need different names. Creates the account and returns {email, plan, id, api_key, prefix, name, use_cases?}, where each use case carries its own api_key and the first one's is the account's first key. If any entry is invalid, no account is created. A single use_case object is also accepted. api_key appears only in this response; we store a SHA-256 hash of it. Limited to 5 signups per hour per IP.

Returns {email, plan, month: {used, quota}, daily: [{day, count}], keys: [{id, prefix, name, created_at, revoked_at, active}]}, with daily counts covering the last 30 days.

Body: {name}. Creates another key (at most 5 active) and returns it once.

Revokes a key. You can't revoke your only active key. Revocation reaches every server within a minute.

Errors

An UNSAT verdict is not an error: it's a 200 with "sat": false.