Chiasmus

MCP server that gives LLMs access to formal verification via Z3 (SMT solver) and Tau Prolog, 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, 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

... [View full README on GitHub](https://github.com/yogthos/chiasmus#readme)