# Chiasmus

MCP server that gives LLMs access to formal verification via Z3 (SMT solver) and SWI-Prolog (via `prolog-wasm-full`, includes `library(clpfd)`), plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.

### Example use cases

- **"Can our RBAC rules ever conflict?"** → Z3 finds the exact role/action/resource triple where allow and deny both fire
- **"Find compatible package versions"** → Z3 solves dependency constraints with incompatibility rules, returns a valid assignment or proves none exists
- **"Can user input reach the database?"** → Prolog traces all paths through the call graph, flags taint flows to sensitive sinks
- **"Are our frontend and backend validations consistent?"** → Z3 finds concrete inputs that pass one but fail the other (e.g. age=15 passes frontend min=13 but fails backend min=18)
- **"Does our workflow have dead-end or unreachable states?"** → Prolog checks reachability from the initial state, identifies orphaned and terminal nodes
- **"What's the dead code in this module?"** → tree-sitter parses source files, Prolog finds functions unreachable from any entry point
- **"What breaks if I change this function?"** → call graph impact analysis shows all transitive callers
- **"Do a full code review of these files"** → `chiasmus_review` returns a phased recipe of graph analyses + verification templates, and you execute it step-by-step

## Setup

```bash
npm install -g chiasmus
```

### Claude Code

```bash
claude mcp add chiasmus -- npx -y chiasmus
```

Or add to `~/.claude/settings.json`:

```json
{
  "mcpServers": {
    "chiasmus": {
      "command": "npx",
      "args": ["-y", "chiasmus"]
    }
  }
}
```

### Crush

Add to `crush.json`:

```json
{
  "mcp": {
    "chiasmus": {
      "type": "stdio",
      "command": "npx",
      "args": ["-y", "chiasmus"]
    }
  }
}
```

### OpenCode

Add to `opencode.json`:

```json
{
  "mcp": {
    "chiasmus": {
      "type": "local",
      "command": ["npx", "-y", "chiasmus"]
    }
  }
}
```

### Long-running HTTP daemon

Instead of every client session starting its own `npx chiasmus` stdio process, you can run one Chiasmus process as a Streamable HTTP server and point clients that support URL-based MCP servers at it:

```bash
chiasmus-http --host 127.0.0.1 --port 3939 --path /mcp   # the defaults
```

Claude Code:

```bash
claude mcp add --transport http chiasmus http://127.0.0.1:3939/mcp
```

Codex (`~/.codex/config.toml`):

```toml
[mcp_servers.chiasmus]
url = "http://127.0.0.1:3939/mcp"
```

Options (also read from the environment): `--host` (`CHIASMUS_MCP_HOST`), `--port` (`CHIASMUS_MCP_PORT`), `--path` (`CHIASMUS_MCP_PATH`), `--session-ttl-ms` (`CHIASMUS_MCP_SESSION_TTL_MS`; a session idle this long is closed, default 30 min), `--chiasmus-home` (`CHIASMUS_HOME`), `--allowed-hosts` (`CHIASMUS_MCP_ALLOWED_HOSTS`), `--max-body-bytes` (`CHIASMUS_MCP_MAX_BODY_BYTES`; a larger request body gets a 413, default 10 MiB like the stdio transport) and `--max-sessions` (`CHIASMUS_MCP_MAX_SESSIONS`; an initialize beyond it gets a 503, default 256). `GET /healthz` answers `{"ok":true,"sessions":<open sessions>}`.

All sessions share one skill library, so a template crafted in one is visible to the others. They also share the daemon's graph cache, keyed by the daemon's working directory, and with it one set of `save_snapshot` names, so give snapshots names unique to your work (for example repository, commit and a run id).

The daemon has no authentication, so it answers only requests whose `Host` header, and `Origin` header if they send one, names `localhost`, `127.0.0.1`, `[::1]` or the `--host` address (unless that is `0.0.0.0` or `::`). Anything else gets a 403 before a session starts. This stops a web page from reaching the daemon through DNS rebinding: the page's own hostname is made to resolve to 127.0.0.1, but the browser still sends that hostname. If clients reach the daemon by another name, list it with `--allowed-hosts name1,name2`.

Solves run in child processes of the daemon (see `chiasmus_verify` below), so an input that crashes a solver costs only the call that sent it: the daemon and its other sessions carry on. With `CHIASMUS_SOLVER_WORKER=off` they run in the daemon itself; a solver whose WASM module aborts or traps there makes the daemon log `fatal <solver> WASM error, exiting so the process is restarted` and exit with code 1 instead of staying up unresponsive. A `chiasmus_graph` or `chiasmus_map` call running at that moment doesn't change this: the daemon kills its child processes with SIGKILL as it exits, so none outlives it. The exit is immediate: requests in flight get no answer, and their clients see the connection close. Run the daemon under a supervisor that restarts it, such as a systemd unit with `Restart=on-failure`. On SIGTERM or SIGINT it stops accepting requests (a request on a connection already open gets a 503), closes its sessions and connections, kills the graph and solver child processes and exits with 143 or 130, at most 5 s after the signal.

## Tools

**`chiasmus_verify`** — Submit raw SMT-LIB or Prolog, get a verified result. Z3 UNSAT results include an `unsatCore` showing which assertions conflict. Prolog supports `explain=true` for derivation traces showing which rules fired.

```
chiasmus_verify solver="z3" input="
  (declare-const x Int)
  (assert (! (> x 10) :named gt10))
  (assert (! (< x 5) :named lt5))
"
→ { status: "unsat", unsatCore: ["gt10", "lt5"] }
```

```
chiasmus_verify solver="prolog"
  input="parent(tom, bob). parent(bob, ann). ancestor(X,Y) :- parent(X,Y). ancestor(X,Y) :- parent(X,Z), ancestor(Z,Y)."
  query="ancestor(tom, Who)."
  explain=true
→ { status: "success", answers: [...], trace: ["ancestor(tom,bob)", "ancestor(bob,ann)", "ancestor(tom,ann)"] }
```

**`chiasmus_verify`** also accepts `format="mermaid"` with `solver="prolog"` to parse Mermaid flowcharts and state diagrams directly into Prolog facts:

```
chiasmus_verify solver="prolog" format="mermaid"
  input="graph TD\n  UserInput --> Validator\n  Validator --> DB\n  Validator --> Logger"
  query="reaches(userinput, db)."
→ { status: "success", answers: [{}] }

chiasmus_verify solver="prolog" format="mermaid"
  input="stateDiagram-v2\n  Idle --> Active : start\n  Active --> Done : finish"
  query="can_reach(idle, done)."
→ { status: "success", answers: [{}] }
```

Z3 and Prolog each run in a child process of the server, one solve at a time per solver (up to 32 more wait in a queue). Some inputs break a solver's WebAssembly module for good: a very large input overflows its stack, a small one can exhaust Z3's 2 GiB heap, and Prolog's `halt` ends its runtime. Such a call gets an error result, such as `{ status: "error", error: "memory access out of bounds" }`, the child is replaced, and the next solve runs in a fresh one. Cancelling a call, or a solve running past `CHIASMUS_SOLVER_JOB_TIMEOUT_MS`, kills its child too. A result over 10 MiB of JSON comes back as an error instead (in a batch, only the largest results do, until the rest fit; a batch of too many results gets one error). `chiasmus_solve` and `chiasmus_craft` run their solves the same way. Set `CHIASMUS_SOLVER_WORKER=off` to run solves inside the server process instead, where such a crash ends the process.

**`chiasmus_graph`** — Analyze source code call graphs via tree-sitter + Prolog. Parses source files, extracts cross-module call graphs, runs formal analyses.

Built-in language support: **TypeScript**, **JavaScript**, **Python**, **Go**, **Rust**, **Clojure/ClojureScript**, **Scheme**, **Racket**, **Common Lisp**. Additional languages can be added via [custom adapters](#custom-language-adapters).

```
chiasmus_graph files=["src/server.ts", "src/db.ts"] analysis="callers" target="query"
→ { analysis: "callers", result: ["handleRequest"] }

chiasmus_graph files=["src/**/*.ts"] analysis="dead-code"
→ { analysis: "dead-code", result: ["unusedHelper", "legacyParser"] }

chiasmus_graph files=["app.py", "db.py"] analysis="reachability" from="handle" to="connect"
→ { analysis: "reachability", result: { reachable: true } }

chiasmus_graph files=["main.go", "handler.go"] analysis="impact" target="Query"
→ { analysis: "impact", result: ["Handle", "main"] }
```

Analyses: `summary`, `callers`, `callees`, `reachability`, `dead-code`, `cycles`, `path`, `impact`, `layer-violation`, `communities`, `hubs`, `bridges`, `surprises`, `diff`, `entry-points`, `facts`.

Reachability-heavy analyses (`cycles`, `reachability`, `path`, `impact`, `dead-code`, `callers`, `callees`) run on native O(V+E) graph algorithms and scale to codebases with thousands of functions. `communities` uses Louvain; `bridges` uses exact betweenness centrality up to 2,000 nodes and a deterministic sampled estimate above that, flagged by an `approximate` field on the result. The `facts` analysis emits raw Prolog for use with `chiasmus_verify`, capped at 10 MB — above that limit the result is `{ error, size, limit }` rather than a program string, so narrow the file set or call a specific analysis directly. Opt in to `include_insights=true` on `facts` to also emit `community/2`, `cohesion/2`, `hub/2`, `bridge/2` predicates.

TS/JS calls also carry qualified-name hints when the receiver's class can be inferred (`CallsFact.calleeQN = "Class.method"`), and imports are resolved through `tsconfig.json` path aliases and the batch's file layout (`ImportsFact.resolved = "<repo-relative path>"`). Both surface as additive Prolog facts — `calls_qn/3` and `imports_resolved/3` — so back-compat queries over `calls/2` and `imports/3` keep working.

`chiasmus_graph` and `chiasmus_map` run in a child process of the server, one call at a time (up to 32 more wait in a queue), so a large extraction never stalls the server's other tools. Cancelling a call, or a call running past `CHIASMUS_GRAPH_JOB_TIMEOUT_MS`, kills that process; the next graph call starts a fresh one. Set `CHIASMUS_GRAPH_WORKER=off` to run them inside the server process instead. They also run there once a language adapter has been registered in code with `registerAdapter()`, since such an adapter can't be handed to another process, and when `graph-child.js` isn't next to the pool module (a bundled build).

### Persistent cache and PR diff

Pass `cache=true` on `chiasmus_graph` to enable a per-file content-hash cache — unchanged files skip re-parsing across calls. On a 42-file TypeScript repo, warm hits run at ~2.5ms vs ~170ms cold (60× speedup). Cache lives under `$CHIASMUS_CACHE_DIR` (default `~/.cache/chiasmus`) with an LRU budget per repo.

```
chiasmus_graph files=[...] analysis="summary" cache=true save_snapshot="main"
→ extracts + saves the current graph as the "main" baseline

# After branch changes:
chiasmus_graph files=[...] analysis="diff" against="main" cache=true
→ { addedNodes, removedNodes, addedEdges, removedEdges, summary }
```

`chiasmus_review` accepts `delta_against="<snapshot>"` — when set, a phase 0 diffs against the snapshot, impact-checks removed symbols, and scopes later phases to what the PR actually changed.

**`chiasmus_map`** — Pre-built codebase map for agents to consult **before** bulk file reads. Reuses the same tree-sitter extraction + cache as `chiasmus_graph`; returns a compact outline so an LLM can answer "what's in this repo" / "what does this file expose" / "where is X defined" without opening source.

```
chiasmus_map files=["src/**/*.ts"]
→ markdown outline: per-file headlines, exports with signatures,
  token estimates, leading doc comments

chiasmus_map files=[...] mode="file" path="src/server.ts" format="json"
→ { exports, imports grouped by source, all top-level symbols }

chiasmus_map files=[...] mode="symbol" name="handleRequest"
→ { defines: [{file, line, signature}], callers, callees }
```

Modes: `overview` (default), `file`, `symbol`. Output: `markdown` (default) or `json`. `include` globs and `max_exports` (clamped to ≥0) scope the overview. `cache=true` reuses the shared per-file cache.

**`chiasmus_skills`** — Search the template library. Ships with 8 starter templates covering authorization, configuration, dependency resolution, validation, rule inference, and graph reachability. By-name lookups include related template suggestions.

**`chiasmus_formalize`** — Find the best template for a problem, get slot-filling instructions plus suggestions for related verification checks. Fill the slots using your context, then call `chiasmus_verify`.

**`chiasmus_solve`** — End-to-end: selects template, fills slots via LLM, runs lint and correction loops with enriched feedback (unsat cores, structured error classification), returns a verified result. Optional — the same result is achieved by using `chiasmus_formalize` → fill slots → `chiasmus_verify`, which is the recommended workflow since the calling LLM has full conversation context.

**`chiasmus_craft`** — Create a new template and add it to the skill library. The calling LLM designs the template — no API key needed. Describe a problem type, then submit a skeleton with `{{SLOT:name}}` markers, slot definitions, and normalization recipes. Validates slot/skeleton consistency and name uniqueness. Optionally tests the example through the solver first, and stores nothing if the solver reports an error for it.

```
chiasmus_craft name="api-rate-limit" domain="configuration" solver="z3"
  signature="Check if rate limit configs across services are consistent"
  skeleton="{{SLOT:declarations}}\n(assert (not (= {{SLOT:limit_a}} {{SLOT:limit_b}})))"
  slots=[{name: "declarations", ...}, {name: "limit_a", ...}, {name: "limit_b", ...}]
  normalizations=[{source: "YAML config", transform: "Map rate limits to Int constants"}]
→ { created: true, template: "api-rate-limit", slots: 3 }
```

After creation, the template appears in `chiasmus_skills` searches and `chiasmus_formalize`.

**`chiasmus_review`** — Returns a phased code-review recipe: which chiasmus tools and templates to run, in what order, and what to look for. No side effects — pure scaffolding. Execute phases sequentially using the named tools, then produce a final report per the `reporting` section.

```
chiasmus_review files=["src/handler.ts", "src/db.ts"] focus="all"
→ {
    phases: [
      { phase: "1. Structural overview", actions: [{tool: "chiasmus_graph", args: {analysis: "summary"}, interpret: "..."}] },
      { phase: "2. Architecture health", actions: [dead-code, cycles, layer-violation] },
      { phase: "3. Security — data flow and taint", actions: [facts + chiasmus_formalize taint-propagation] },
      { phase: "4. Resource safety", actions: [association-rule-check] },
      { phase: "5. Authorization", actions: [policy-contradiction] },
      { phase: "6. Correctness — invariants, boundaries, state machines", actions: [...] },
      { phase: "7. Impact analysis on flagged functions", actions: [chiasmus_graph impact] },
    ],
    suggestedTemplates: [...],
    reporting: { format: "Numbered issue list with severity", severityLevels: ["CRITICAL","HIGH","MEDIUM","LOW","INFO"] }
  }
```

Focus modes subset the phases: `all` (default, 7 phases), `quick` (overview + architecture), `architecture` (structural defects + impact), `security` (taint + resource pairing + auth), `correctness` (invariants + boundaries + state machines).

Each action carries an `interpret` field describing how to score the result. After all phases, emit a numbered issue list with severity labels and file:line references.

**`chiasmus_search`** — Semantic code search over a set of files. Finds functions and methods whose *meaning* matches a natural-language query (e.g. "where do we refresh OAuth tokens", "rate-limit logic"). Uses embeddings + cosine similarity over callable defines; returns a ranked list with `{name, file, line, signature, leadingDoc, score}`.

```
chiasmus_search query="refresh OAuth tokens" files=["src/**/*.ts"] top_k=5
→ { hits: [
    { name: "refreshAccessToken", file: "src/auth/token.ts", line: 42, score: 0.78, ... },
    { name: "rotateSession", file: "src/auth/session.ts", line: 118, score: 0.71, ... },
    ...
  ] }
```

Opt-in: needs an embedding provider via env (`OPENAI_API_KEY`, `DEEPSEEK_API_KEY`, or `OPENROUTER_API_KEY`). Override the model with `CHIASMUS_EMBED_MODEL` (default `text-embedding-3-small`), base URL with `CHIASMUS_EMBED_URL`, and dimension with `CHIASMUS_EMBED_DIM`. Embeddings are cached by content SHA-256 under `$CHIASMUS_HOME/embeddings` — unchanged code is not re-embedded.

### Local embeddings (no API key)

`chiasmus_search` and `chiasmus_formalize` can run embeddings entirely on-device via [node-llama-cpp](https://github.com/withcatai/node-llama-cpp) — e.g. `Qwen3-Embedding-0.6B`. `node-llama-cpp` ships as an `optionalDependency`, so it is installed automatically alongside chiasmus (via `npm`, `pnpm`, or `npx`). The GGUF model is downloaded from HuggingFace on first use and cached under `$CHIASMUS_HOME/models`.

If the optional install was skipped (e.g. an unsupported platform where the fetch failed), install it manually:

```bash
npm install node-llama-cpp   # or: pnpm add node-llama-cpp
```

Then opt in. Either set `localEmbeddings` in `~/.chiasmus/config.json`:

```json
{
  "localEmbeddings": {
    "enabled": true,
    "model": "hf:Qwen/Qwen3-Embedding-0.6B-GGUF",
    "dimension": 1024
  }
}
```

…or use env vars:

```bash
export CHIASMUS_LOCAL_EMBED=1
export CHIASMUS_LOCAL_EMBED_MODEL=hf:Qwen/Qwen3-Embedding-0.6B-GGUF
export CHIASMUS_LOCAL_EMBED_DIM=1024        # optional; else discovered on first embed
```

When enabled, local takes priority over cloud embedding providers. `model` accepts an `hf:` repo URI, a bare Hugging Face repo id (`org/repo`), a local `.gguf` path, or an `http(s)` URL. Env vars override the config block per field; `CHIASMUS_LOCAL_EMBED_DIR` overrides the download directory (default `$CHIASMUS_HOME/models`) and `CHIASMUS_LOCAL_EMBED_BATCH` the texts-per-call batch size (default 32).

**`chiasmus_lint`** — Fast structural validation of specs without running the solver.

## Recommended Workflow

The calling LLM (GLM, GPT, etc.) drives the process — no API key needed:

1. `chiasmus_formalize problem="Can our RBAC rules ever conflict?"` → get template + slot instructions
2. Fill the template slots using your knowledge of the user's codebase
3. `chiasmus_verify solver="z3" input="(filled spec)"` → get verified result
4. If error → read the error, fix the spec, call `chiasmus_verify` again

## When to Use

Use a solver when the LLM alone can't guarantee correctness:

- **"Does this hold for ALL inputs?"** — solvers prove universally, LLMs just check examples
- **"Do these rules ever conflict?"** — contradiction detection over combinatorial spaces
- **"Can X reach Y through any path?"** — transitive closure / reachability
- **Access control, configs, dependencies** — where correctness is non-negotiable

Use `chiasmus_graph` when you need structural reasoning about code:

- **"What calls this function?"** — impact analysis before refactoring
- **"What's dead code?"** — find functions unreachable from entry points
- **"Can user input reach this SQL query?"** — taint analysis via call graph reachability
- **"What breaks if I change X?"** — blast radius via reverse reachability
- **"Are there circular dependencies?"** — cycle detection in call graphs

## Why `chiasmus_graph` over grep

When an LLM needs to understand code structure, it typically greps for function names and manually traces call chains. This works for direct references but breaks down for transitive questions. Here's a real comparison using chiasmus's own codebase:

**Question: "What's the blast radius of changing `lintSpec`?"**

With grep, this takes multiple rounds — first find direct callers, then callers of those callers, reconstructing the chain manually:

```
grep lintSpec src/**/*.ts     → found in engine.ts (lintLoop) and mcp-server.ts (handleLint)
grep lintLoop src/**/*.ts     → called from solve() at lines 75 and 87
grep handleSolve src/**/*.ts  → called from createChiasmusServer switch...
```

Three rounds of grep, manual reasoning at each step, and you've still only traced part of the chain. With `chiasmus_graph`, one call gives the complete transitive answer:

```
chiasmus_graph analysis="impact" target="lintSpec"
→ ["lintLoop", "handleLint", "solve", "correctionLoop",
   "handleVerify", "handleSolve", "handleGraph",
   "createChiasmusServer", "runAnalysis", "runAnalysisFromGraph"]
```

10 affected functions found in a single call — including paths through `correctionLoop` and `runAnalysis` that the grep approach missed entirely.

The same applies to other structural questions:

| Question | Grep | chiasmus_graph |
|----------|------|----------------|
| Impact of changing X | Multiple greps + manual trace; misses transitive paths | 1 call, complete transitive chain |
| Dead code detection | Grep every function name against all call sites — impractical | 1 call, definitive answer |
| Can A reach B? | Manually reconstruct call chain across files | 1 call, true/false |
| Call chain A→B | Multiple greps, mentally reconstruct path | 1 call, exact chain e.g. `[handleSolve,solve,lintLoop,lintSpec]` |

The key difference: grep finds string matches, `chiasmus_graph` answers structural questions. Transitive reachability, dead code, and impact analysis are formally impossible with grep alone.

## Custom Language Adapters

Add tree-sitter support for any language by publishing an npm package named `chiasmus-adapter-<language>`. Chiasmus auto-discovers these at startup.

```ts
// chiasmus-adapter-rust/index.ts
import type { LanguageAdapter } from "chiasmus/graph";

const adapter: LanguageAdapter = {
  language: "rust",
  extensions: [".rs"],
  grammar: { package: "tree-sitter-rust" },
  extract(rootNode, filePath) {
    const defines = [];
    const calls = [];
    // Walk the tree-sitter AST and populate defines, calls, imports, etc.
    // ... your language-specific extraction logic ...
    return { defines, calls, imports: [], exports: [], contains: [] };
  },
};

export default adapter;
```

Install alongside chiasmus and enable adapter discovery in `~/.chiasmus/config.json`:

```bash
npm install chiasmus-adapter-rust
```

```json
{
  "adapterDiscovery": true
}
```

Adapter discovery is **off by default** to keep startup fast. Enable it when you have custom adapters installed.

### searchPaths

An adapter can export `searchPaths` to point to directories containing additional adapter modules (`.js`/`.mjs` files). This is useful for loading adapters from non-standard locations:

```ts
export default {
  language: "rust",
  extensions: [".rs"],
  grammar: { package: "tree-sitter-rust" },
  extract(rootNode, filePath) { /* ... */ },
  searchPaths: ["/shared/company-adapters"],
};
```

### Adapter interface

| Field | Type | Description |
|-------|------|-------------|
| `language` | `string` | Language identifier (e.g., `"rust"`) |
| `extensions` | `string[]` | File extensions (e.g., `[".rs"]`) |
| `grammar` | `object` | Tree-sitter grammar: `{ package, moduleExport? }` for native or `{ package, wasmFile, wasm: true }` for WASM |
| `extract` | `(rootNode, filePath) => CodeGraph` | Walks the AST and returns `{ defines, calls, imports, exports, contains }` |
| `searchPaths` | `string[]` (optional) | Additional directories to scan for adapter modules |

Built-in languages always take precedence over adapters with the same extensions.

## Library Usage

Chiasmus can be used as a library in any Node.js project:

```bash
npm install chiasmus
```

### Quick Start

```ts
import { SolverSession, lintSpec, SkillLibrary, FormalizationEngine } from "chiasmus";
```

Or import from specific subpaths:

```ts
import { createZ3Solver, createPrologSolver } from "chiasmus/solvers";
import { extractGraph, runAnalysis } from "chiasmus/graph";
import { lintSpec, FormalizationEngine } from "chiasmus/formalize";
import { SkillLibrary, craftTemplate } from "chiasmus/skills";
import { createLLMFromEnv } from "chiasmus/llm";
```

### Solvers

```ts
import { SolverSession } from "chiasmus/solvers";

const session = await SolverSession.create("z3");
try {
  const result = await session.solve({
    type: "z3",
    smtlib: `(declare-const x Int) (assert (> x 5))`,
  });
  if (result.status === "sat") {
    console.log("Satisfiable:", result.model);
  }
} finally {
  session.dispose();
}
```

`SolverSession` runs its solves in a child process per solver, shared by every session in the process, so an input that crashes a solver gets an error result and the next solve gets a fresh child. Pass `{ signal }` as `solve()`'s second argument to stop a solve by killing its child. Call `shutdownSolverChildren()` before exiting to kill the children and wait for them; an exit through `process.exit()` kills them anyway. `createZ3Solver()` and `createPrologSolver()`, and `SolverSession` with `CHIASMUS_SOLVER_WORKER=off`, run in the calling process: after a WASM abort, trap or `halt` that solver module is unusable, and every later solve on it returns an error. A long-lived host doing that should call `exitOnFatalSolverError()` (log and exit 1, so a supervisor restarts it) or pass its own handler to `setFatalSolverErrorHandler()`.

### Graph Analysis

```ts
import { extractGraph, runAnalysis } from "chiasmus/graph";

const result = await runAnalysis(
  ["src/server.ts", "src/db.ts"],
  { analysis: "dead-code" }
);
console.log(result.result);
```

### Lint & Validation

```ts
import { lintSpec } from "chiasmus/formalize";

const { spec, fixes, errors } = lintSpec(rawSpec, "z3");
if (errors.length > 0) {
  console.error("Lint errors:", errors);
}
```

### Skill Library

```ts
import { SkillLibrary } from "chiasmus/skills";
import { join } from "node:path";
import { homedir } from "node:os";

const library = await SkillLibrary.create(join(homedir(), ".chiasmus"));
const results = library.search("access control policy conflict");
console.log(results);
library.close();
```

### Exports

| Subpath | Exports |
|---------|---------|
| `chiasmus` | All public APIs (barrel export) |
| `chiasmus/solvers` | `SolverSession`, `createZ3Solver`, `createPrologSolver`, `createChildSolver`, `shutdownSolverChildren`, `correctionLoop`, `setFatalSolverErrorHandler`, `exitOnFatalSolverError`, `isFatalWasmError`, solver types |
| `chiasmus/graph` | `extractGraph`, `runAnalysis`, `runAnalysisFromGraph`, `buildFactsResult`, `graphToProlog`, `parseMermaid`, `detectCommunities`, `detectHubs`, `detectBridges`, `analyzeBridges`, `detectSurprisingConnections`, `detectEntryPoints`, `graphDiff`, `saveSnapshot`/`loadSnapshot`/`listSnapshots`, cache APIs, adapter registry, graph types |
| `chiasmus/formalize` | `lintSpec`, `classifyFeedback`, `extractPrologQuery`, `FormalizationEngine`, result types |
| `chiasmus/skills` | `SkillLibrary`, `craftTemplate`, `validateTemplate`, skill types |
| `chiasmus/llm` | `createLLMFromEnv`, `createEmbeddingFromEnv`, `AnthropicAdapter`, `OpenAICompatibleAdapter`, `OpenAICompatibleEmbeddingAdapter`, `LocalEmbeddingAdapter`, `resolveLocalEmbeddingConfig`, LLM types |
| `chiasmus/mcp` | `createChiasmusServer`, `getChiasmusHome` |

## Configuration

| Variable | Default | Purpose |
|----------|---------|---------|
| `CHIASMUS_HOME` | `~/.chiasmus/` | Database, skill storage, and config |
| `CHIASMUS_CACHE_DIR` | `~/.cache/chiasmus` | Per-file extraction cache + graph snapshots (when `cache=true`) |
| `CHIASMUS_CACHE_MAX_PER_REPO` | `67108864` (64 MB) | Per-repo cache byte budget — LRU eviction above this |
| `CHIASMUS_GRAPH_WORKER` | on | `0`/`off`/`false` runs `chiasmus_graph` and `chiasmus_map` in the server process instead of a child process |
| `CHIASMUS_GRAPH_WORKER_HEAP_MB` | Node's default | V8 heap limit of the graph child process; an overrun fails the job and replaces the child, the server keeps running |
| `CHIASMUS_GRAPH_JOB_TIMEOUT_MS` | `600000` (10 min) | A graph job running longer is killed and the graph child process replaced. Digits only (other values keep the default); capped at `2147483647` (about 24.8 days) |
| `CHIASMUS_SOLVER_WORKER` | on | `0`/`off`/`false` runs Z3 and Prolog solves in the server process instead of a child process per solver; a solver crash then ends the process |
| `CHIASMUS_SOLVER_JOB_TIMEOUT_MS` | `600000` (10 min) | A solve running longer, child start-up included, is killed and its solver's child process replaced. Raise it for Z3 solves that set a longer `:timeout`. Digits only; capped at `2147483647` |
| `ANTHROPIC_API_KEY` | — | Optional: Anthropic provider for autonomous mode |
| `DEEPSEEK_API_KEY` | — | Optional: DeepSeek provider for autonomous mode |
| `OPENAI_API_KEY` | — | Optional: OpenAI provider for autonomous mode |
| `CHIASMUS_API_URL` | per provider | Override API base URL (e.g. for local models via Ollama) |
| `CHIASMUS_MODEL` | per provider | Override model name |
| `CHIASMUS_EMBED_MODEL` | `text-embedding-3-small` | Embedding model name (cloud providers) |
| `CHIASMUS_EMBED_URL` | per provider | Embedding API base URL |
| `CHIASMUS_EMBED_DIM` | discovered | Embedding dimension (else learned on first call; local skips the first-call cache miss) |
| `CHIASMUS_LOCAL_EMBED` | — | Opt in to on-device embeddings (`1`/`true`/`yes`/`on`). See [Local embeddings](#local-embeddings-no-api-key) |
| `CHIASMUS_LOCAL_EMBED_MODEL` | — | Model id (`hf:org/repo`, bare repo id, local `.gguf`, or URL) |
| `CHIASMUS_LOCAL_EMBED_DIM` | discovered | Fixed embedding dimension (else discovered on first call) |
| `CHIASMUS_LOCAL_EMBED_DIR` | `$CHIASMUS_HOME/models` | Where downloaded models are cached |
| `CHIASMUS_LOCAL_EMBED_BATCH` | `32` | Texts per embedding backend call |

Providers are checked in order: Anthropic → DeepSeek → OpenAI. Only one key is needed for autonomous mode (`chiasmus_solve`). When used from Claude Code, Crush, or OpenCode, no API key is needed — the calling LLM handles template filling directly.

Embedding provider selection (first match wins): local embeddings (when `CHIASMUS_LOCAL_EMBED` is set and a model is configured) → Azure OpenAI → OpenAI → DeepSeek → OpenRouter. When enabled without a model, a warning is logged and cloud providers are used instead.

### `~/.chiasmus/config.json`

| Key | Default | Purpose |
|-----|---------|---------|
| `adapterDiscovery` | `false` | Scan `node_modules` for `chiasmus-adapter-*` packages at startup |
| `localEmbeddings` | — | Opt in to on-device embeddings via node-llama-cpp. Object with `enabled`, `model`, `dimension`, `modelsDir`. See [Local embeddings](#local-embeddings-no-api-key) |

## License

Apache-2.0