Chiasmus

https://github.com/yogthos/chiasmus
Admin
A neurosymbolic verification engine and MCP server that combines Z3 SMT solver and SWI-Prolog for...
Tokens:13,095
Snippets:151
Trust Score:9.6
License:Apache-2.0
Update:4 months ago
Show doc for...
Tokens:
Raw
### Install Rust Adapter and Enable Discovery

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Instructions to install a custom language adapter package and enable adapter discovery in the Chiasmus configuration.

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

--------------------------------

### Install Chiasmus CLI

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Installs the Chiasmus command-line interface globally using npm.

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

--------------------------------

### Install Chiasmus Package

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Install the Chiasmus library using npm. This is the first step to using Chiasmus in your Node.js project.

```bash
npm install chiasmus
```

--------------------------------

### Example Call Chain for Specific Path

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Illustrates a specific call chain, e.g., from handleSolve to solve to lintLoop, as might be returned by chiasmus_graph.

```text
[handleSolve,solve,lintLoop,lintSpec]
```

--------------------------------

### Solver Session Example (Z3)

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Demonstrates creating and using a SolverSession with the Z3 solver to solve an SMT-LIB query. Ensure to dispose of the session when done.

```typescript
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();
}
```

--------------------------------

### Custom Rust Language Adapter Example

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

An example of a custom language adapter for Rust, defining language, extensions, grammar, and the extract function for AST traversal.

```typescript
// 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;

```

--------------------------------

### Quick Start: Import Core Components

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Import essential components like SolverSession, lintSpec, SkillLibrary, and FormalizationEngine from the main 'chiasmus' package.

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

--------------------------------

### CI Pipeline Steps for Chiasmus

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Steps executed in the CI pipeline for Chiasmus, including dependency installation, type checking, and running tests.

```bash
pnpm install --frozen-lockfile
pnpm typecheck
pnpm test:run
```

--------------------------------

### Formalization Template Example (YAML)

Source: https://github.com/yogthos/chiasmus/blob/main/architecture.md

A YAML-defined template for a 'policy-contradiction-check' skill, specifying the domain, solver, signature, skeleton SMT-LIB code, and normalization rules.

```yaml
name: policy-contradiction-check
domain: authorization
solver: z3
signature: "Check if a set of allow/deny rules can ever conflict"
skeleton: |
  (declare-datatypes ((Principal 0) (Resource 0) (Action 0)) ...)
  (declare-fun allow (Principal Resource Action) Bool)
  (declare-fun deny (Principal Resource Action) Bool)
  {{SLOT: rule_assertions}}
  (assert (exists ((p Principal) (r Resource) (a Action))
    (and (allow p r a) (deny p r a))))
  (check-sat)
normalizations:
  - source: "AWS IAM JSON"
    transform: "map Statement[].{Effect, Principal, Action, Resource} to triples"
  - source: "Django permissions"
    transform: "extract user as principal, permission as action, app as resource"
  - source: "Kubernetes RBAC"
    transform: "expand rules[].{verbs, resources} into action/resource pairs"
  - source: "natural language"
    transform: "extract entities, classify as principal/resource/action"
metadata:
  reuse_count: 0
  success_rate: 0.0
  last_used: null
  promoted: false
```

--------------------------------

### Skill Library Usage Example

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Create and use a SkillLibrary to search for skills. It requires a path to the Chiasmus home directory for storage. Remember to close the library when finished.

```typescript
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();
```

--------------------------------

### Verify Prolog with Explanations

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_verify with Prolog solver and explain=true to get derivation traces. Supports custom Prolog input and queries.

```shell
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)"] }
```

--------------------------------

### Custom Adapter with Additional Search Paths

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

An example of a custom language adapter that exports 'searchPaths' to load additional adapter modules from non-standard locations.

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

```

--------------------------------

### Vitest Test Structure Example

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Illustrates a typical test structure using Vitest, including describe blocks, individual tests, and setup/teardown logic for solver instances.

```typescript
import { describe, it, expect, afterEach } from "vitest";

describe("Z3Solver", () => {
  let solver: Solver;
  afterEach(() => { solver?.dispose(); });

  it("returns sat with a model", async () => {
    solver = await createZ3Solver();
    const result = await solver.solve({ type: "z3", smtlib: `...` });
    expect(result.status).toBe("sat");
    if (result.status === "sat") {  // TypeScript narrowing
      expect(result.model).toHaveProperty("x");
    }
  });
});
```

--------------------------------

### ESM Import Style Example

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Demonstrates the required import style using .js extensions for ESM modules and 'import type' for type-only imports.

```typescript
import { SolverSession } from "./solvers/session.js";
import type { SolverResult } from "./solvers/types.js";
```

--------------------------------

### Formalize a Problem with Chiasmus

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_formalize to get a template and slot instructions for a given problem. This is the first step in the recommended workflow.

```bash
chiasmus_formalize problem="Can our RBAC rules ever conflict?"
```

--------------------------------

### Verify a Specification with Chiasmus

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_verify with a specified solver and the filled template to get a verified result. This is the third step in the recommended workflow.

```bash
chiasmus_verify solver="z3" input="(filled spec)"
```

--------------------------------

### Example Call Chain from Chiasmus Graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

This output shows a complete transitive call chain for a given analysis target, demonstrating the comprehensive nature of chiasmus_graph analysis.

```text
["lintLoop", "handleLint", "solve", "correctionLoop",
   "handleVerify", "handleSolve", "handleGraph",
   "createChiasmusServer", "runAnalysis", "runAnalysisFromGraph"]
```

--------------------------------

### Graph Analysis Example

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Perform graph analysis, such as dead-code detection, on specified source files. The result object contains the analysis outcome.

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

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

--------------------------------

### Lint Specification Example

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Lint a raw specification string using the 'lintSpec' function. It returns the processed spec, any suggested fixes, and detected errors.

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

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

--------------------------------

### Build and Test Commands for Chiasmus

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Common commands for building, type-checking, and testing the Chiasmus project using pnpm and Vitest.

```bash
pnpm build          # Compile TypeScript (tsc) → dist/
pnpm typecheck      # Type-check only (tsc --noEmit)
pnpm test           # Run tests in watch mode (vitest)
pnpm test:run       # Run tests once (vitest run)
pnpm test:coverage  # Run tests with V8 coverage report
pnpm mcp            # Run MCP server locally via tsx
```

--------------------------------

### Chiasmus Home Directory Configuration

Source: https://github.com/yogthos/chiasmus/blob/main/architecture.md

Sets the CHIASMUS_HOME environment variable to define the database and skills directory. Defaults to ~/.chiasmus/ if not specified.

```bash
CHIASMUS_HOME=~/.chiasmus/   # default
```

--------------------------------

### Parse Mermaid State Diagrams with Prolog

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_verify with Prolog solver and format="mermaid" to parse Mermaid state diagrams into Prolog facts.

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

--------------------------------

### Chiasmus Configuration for Adapter Discovery

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

JSON configuration to enable adapter discovery in Chiasmus. This is off by default for faster startup.

```json
{
  "adapterDiscovery": true
}

```

--------------------------------

### Skill Library Lifecycle Stages

Source: https://github.com/yogthos/chiasmus/blob/main/architecture.md

Illustrates the lifecycle of a skill within the Chiasmus system, from initial creation to promotion and potential pruning based on usage.

```text
Solved problem
  → LLM abstracts concrete values into typed parameters
  → Generates signature + normalization schemas
  → Stored as candidate skill (promoted=false, reuse_count=0)
  → After N successful reuses → promoted=true
  → Unused for M sessions → demoted or pruned
  → Before adding: check embedding similarity against existing (merge if >0.9)
```

--------------------------------

### Configure Claude MCP Server

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Adds Chiasmus as an MCP server to Claude using the command line.

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

--------------------------------

### Verify SMT-LIB with Z3

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_verify with Z3 solver to check SMT-LIB inputs. Z3 UNSAT results include an unsatCore.

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

--------------------------------

### Create a New Template with chiasmus_craft

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_craft to create and add new templates to the skill library. Define the template's name, domain, solver, signature, skeleton, slots, and normalizations. It validates consistency and uniqueness, and can optionally test the template.

```bash
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 }
```

--------------------------------

### Parse Mermaid Flowcharts with Prolog

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_verify with Prolog solver and format="mermaid" to parse Mermaid flowcharts into Prolog facts.

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

--------------------------------

### Configure OpenCode MCP Server

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Adds Chiasmus as an MCP server to OpenCode by modifying the opencode.json file.

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

--------------------------------

### Configure Claude MCP Server in settings.json

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Adds Chiasmus as an MCP server to Claude by modifying the settings.json file.

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

--------------------------------

### Configure Crush MCP Server

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Adds Chiasmus as an MCP server to Crush by modifying the crush.json file.

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

--------------------------------

### Generate Phased Code Review Recipe with chiasmus_review

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

chiasmus_review generates a phased code-review recipe, specifying tools, templates, and actions for each phase. It supports various focus modes to subset the review phases and provides detailed reporting instructions.

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

--------------------------------

### Enable Caching for chiasmus_graph Summary Analysis

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph with cache=true to enable a per-file content-hash cache for faster analysis across calls. Saves the current graph as a baseline.

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

--------------------------------

### Analyze Python Reachability with chiasmus_graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph to analyze function reachability between 'from' and 'to' points in Python files.

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

--------------------------------

### Chiasmus Project Directory Structure

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Overview of the Chiasmus project's file and directory organization, showing the location of various modules and their responsibilities.

```tree
src/
├── mcp-server.ts          # Entry point — MCP server, all tool handlers, CLI bootstrap
├── config.ts              # Loads ~/.chiasmus/config.json
├── solvers/
│   ├── types.ts           # SolverType, SolverResult (discriminated union), Solver, SolverInput
│   ├── session.ts         # SolverSession — factory for Z3/Prolog solver instances
│   ├── z3-solver.ts       # Z3 WASM wrapper (z3-solver npm), auto-strips check-sat/get-model
│   ├── prolog-solver.ts   # SWI-Prolog (prolog-wasm-full) wrapper, derivation tracing via assertz
│   └── correction-loop.ts # Bounded repair loop (delegates to repl-sandbox)
├── formalize/
│   ├── engine.ts          # FormalizationEngine — template selection, LLM slot-filling, solve pipeline
│   ├── validate.ts        # lintSpec — structural validation, auto-fixes for SMT-LIB/Prolog
│   └── feedback.ts        # classifyFeedback — converts SolverResult to human-readable feedback
├── skills/
│   ├── types.ts           # SkillTemplate, SlotDef, Normalization, SkillMetadata
│   ├── library.ts         # SkillLibrary — SQLite-backed template storage, BM25 search
│   ├── starters.ts        # 8 built-in starter templates (5 Z3, 3 Prolog)
│   ├── bm25.ts            # BM25 keyword search for template retrieval
│   ├── craft.ts           # craftTemplate — user-created template validation + storage
│   ├── learner.ts         # SkillLearner — LLM-driven template extraction from solutions
│   └── relationships.ts   # Template relationship/suggestion graph
├── graph/
│   ├── types.ts           # CodeGraph, LanguageAdapter, FileNode, Hyperedge, DefinesFact, CallsFact.calleeQN, ImportsFact.resolved, FileTypeInfo
│   ├── parser.ts          # tree-sitter lang registry + sync/async parse for TS/JS/Py/Go/Rust/Clojure
│   ├── extractor.ts       # AST walking + per-language call graph extraction + TS/JS collectTypeInfo
│   ├── facts.ts           # graphToProlog — CodeGraph → Prolog facts (incl. calls_qn/3, imports_resolved/3)
│   ├── analyses.ts        # runAnalysis — dispatches all graph analyses
│   ├── native-analyses.ts # O(V+E) cycles/reachability/impact/dead-code/callers/callees
│   ├── graph-util.ts      # Shared helpers: buildUndirectedGraph, forEachUndirectedEdge, undirectedDegree
│   ├── community.ts       # Louvain community detection + cohesion score
│   ├── insights.ts        # detectHubs, detectBridges, detectSurprisingConnections
│   ├── diff.ts            # graphDiff — set diff on nodes + (src,tgt) edge keys
│   ├── entry-points.ts    # Heuristic entry-point detection (zero-in-degree exports)
│   ├── cache.ts           # SHA256 per-file cache + LRU eviction + named snapshots (proper-lockfile)
│   ├── mermaid.ts         # parseMermaid — Mermaid flowcharts/state diagrams → Prolog facts
│   ├── type-env.ts        # TS/JS three-tier type inference + class field/method extraction
│   ├── resolve-calls.ts   # Project-wide QN resolution: inheritance-aware field/method registry
│   ├── tsconfig-aliases.ts # Parses tsconfig.json paths/baseUrl with JSONC + extends chain
│   ├── suffix-index.ts    # Suffix index over batch files for relative import resolution
│   └── adapter-registry.ts # Auto-discovery of chiasmus-adapter-* npm packages
├── search/
│   ├── engine.ts          # buildSearchCorpus + runSearch — cosine-sim code search
│   ├── vector-store.ts    # In-process linear-scan store; serializable
│   ├── embedding-cache.ts # SHA-256-keyed persistent cache, atomic writes
│   └── index.ts           # Module exports
├── llm/
│   ├── types.ts           # LLMAdapter + EmbeddingAdapter interfaces, LLMMessage
│   ├── anthropic.ts       # Anthropic/DeepSeek/OpenAI provider factories (createLLMFromEnv, createEmbeddingFromEnv)
│   ├── openai-compatible.ts # OpenAI-compatible chat + embedding adapters
│   └── mock.ts            # Mock LLM + MockEmbeddingAdapter for testing
tests/                      # Unit tests (mirrors src/ structure)
benchmark/                  # Benchmark problems (5 problems × traditional + chiasmus implementations)

```

--------------------------------

### SolverInput Discriminated Union Type

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Specifies the input format for different solver types, either SMT-LIB for Z3 or a program and query for Prolog. The 'explain' option is specific to Prolog queries.

```typescript
type SolverInput =
  | { type: "z3"; smtlib: string }
  | { type: "prolog"; program: string; query: string; explain?: boolean }

```

--------------------------------

### Chiasmus Architecture Overview

Source: https://github.com/yogthos/chiasmus/blob/main/architecture.md

Visual representation of the four-phase process in the Chiasmus verification engine: Normalize, Formalize, Verify, and Extract.

```text
User prompt
  │
  ▼
┌─────────────────────────────────┐
│  Phase 1: NORMALIZE             │
│  LLM classifies problem type,   │
│  maps domain-specific inputs to │
│  common intermediate format     │
└──────────────┬──────────────────┘
               │
               ▼
┌─────────────────────────────────┐
│  Phase 2: FORMALIZE             │
│  Embed problem signature,       │
│  retrieve matching template,    │
│  LLM fills slots in skeleton    │
│  (or generates from scratch     │
│   using closest as few-shot)    │
└──────────────┬──────────────────┘
               │
               ▼
┌─────────────────────────────────┐
│  Phase 3: VERIFY                │
│  Submit to solver (Z3 / Tau     │
│  Prolog), catch errors, feed    │
│  back to LLM for correction     │
│  (max 5 rounds), return result  │
└──────────────┬──────────────────┘
               │
               ▼
┌─────────────────────────────────┐
│  Phase 4: EXTRACT (optional)    │
│  Generalize solved problem into │
│  candidate skill template for   │
│  future reuse                   │
└─────────────────────────────────┘
```

--------------------------------

### Analyze Go Impact with chiasmus_graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph to analyze the impact of a target function in Go files. Specify files, 'impact' analysis, and the target.

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

--------------------------------

### LLM and Embedding Adapter Interfaces

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Defines the interfaces for Language Model (LLM) and Embedding adapters, specifying the methods they must implement for text completion and embedding generation.

```typescript
interface LLMAdapter {
  complete(system: string, messages: LLMMessage[]): Promise<string>;
}

interface EmbeddingAdapter {
  embed(texts: string[]): Promise<number[][]>;
  dimension(): number;
}
```

--------------------------------

### Generate Codebase Map with chiasmus_map

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

chiasmus_map creates a compact outline of a codebase for agents. It can generate a markdown outline with exports and signatures, or a JSON object detailing exports, imports, and symbols for a specific file or symbol.

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

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

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

--------------------------------

### Analyze Code Changes with chiasmus_graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph to analyze code changes, comparing a branch against a base like 'main'. It provides details on added/removed nodes and edges, and a summary of changes. Caching is enabled by default.

```bash
chiasmus_graph files=[...] analysis="diff" against="main" cache=true
→ { addedNodes, removedNodes, addedEdges, removedEdges, summary }
```

--------------------------------

### Import Specific Modules

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Import specific functionalities from Chiasmus subpaths for more granular control and potentially smaller bundle sizes.

```typescript
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";
```

--------------------------------

### Analyze TypeScript Callers with chiasmus_graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph to analyze call graphs in TypeScript files. Specify files and the 'callers' analysis target.

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

--------------------------------

### Analyze TypeScript Dead Code with chiasmus_graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph to identify dead code in TypeScript files using glob patterns. Specify files and the 'dead-code' analysis.

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

--------------------------------

### Error Correction Loop for LLM-Generated Specs

Source: https://github.com/yogthos/chiasmus/blob/main/architecture.md

Describes the iterative process of correcting errors in LLM-generated formal specifications by feeding solver feedback back to the LLM.

```text
LLM generates formal spec
  → Solver attempts compilation/execution
  → On error: extract stack trace / error message
  → Feed error back into LLM prompt with original spec
  → LLM patches and resubmits
  → Repeat (max 5 rounds)
  → On convergence: return verified result
  → On failure to converge: return best attempt + diagnostics
```

--------------------------------

### Analyze Code Impact with Chiasmus Graph

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use chiasmus_graph with the 'impact' analysis to find all functions affected by a change to a target function. This provides a complete transitive chain of influence.

```bash
chiasmus_graph analysis="impact" target="lintSpec"
```

--------------------------------

### Perform Semantic Code Search

Source: https://github.com/yogthos/chiasmus/blob/main/README.md

Use `chiasmus_search` to find functions and methods semantically matching a natural language query. Requires an embedding provider to be configured via environment variables.

```bash
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, ... },
    ...
  ] }
```

--------------------------------

### SolverResult Discriminated Union Type

Source: https://github.com/yogthos/chiasmus/blob/main/AGENTS.md

Defines the possible outcomes from a solver operation, including status, model, core, answers, or errors. Always check the 'status' field first to determine the result type.

```typescript
type SolverResult =
  | { status: "sat"; model: Record<string, string> }        // Z3 found satisfying assignment
  | { status: "unsat"; unsatCore?: string[] }                // Z3 proved unsatisfiable
  | { status: "unknown" }                                    // Z3 couldn't determine
  | { status: "success"; answers: PrologAnswer[]; trace?: string[] }  // Prolog query succeeded
  | { status: "error"; error: string }                       // Solver/parse error

```
Tokens:
Raw