Chiasmus

Setup

npm install -g chiasmus

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

Library Usage

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

npm install chiasmus

Quick Start

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

Or import from specific subpaths:

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

Configuration

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

`~/.chiasmus/config.json`

Adapter interface

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

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