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

npm install -g chiasmus

Claude Code

claude mcp add chiasmus -- npx -y chiasmus

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

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

Crush

Add to crush.json:

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

OpenCode

Add to opencode.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:

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

Claude Code:

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

Codex (~/.codex/config.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.

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