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"]
    }
  }
}

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: [{}] }

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. 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. 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.

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.

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: [