Chiasmus Neurosymbolic Verification Engine

Chiasmus is an MCP (Model Context Protocol) server that provides LLMs with formal verification and source code analysis capabilities. It uses a template-based pipeline to translate natural language into formal logic, which is then verified using Z3 (an SMT solver) and SWI-Prolog (via prolog-wasm-full, including library(clpfd)).

Key capabilities include:

• Formal Verification: Using Z3 to solve constraints (e.g., RBAC rule conflicts, dependency version compatibility, or validation consistency).
• Logic & Reachability: Using Prolog to trace call graphs for taint analysis (e.g., user input reaching a database) or state machine reachability (e.g., identifying dead-end states).
• Source Code Analysis: Using tree-sitter to parse files and identify dead code or perform impact analysis (transitive callers) when functions change.
• Automated Review: The chiasmus_review tool provides a phased recipe of graph analyses and verification templates for step-by-step execution.

The grammars/ directory contains prebuilt WASM grammars for specific languages. These are used instead of standard npm packages because:

1. Compatibility: Some grammars (like Scheme) have node type names (e.g., syntax) that cause ReferenceError: Cannot access 'SyntaxNode' before initialization when using tree-sitter's native Node bindings.
2. Installation Efficiency: Vendoring these as WASM prevents npm install from triggering heavy node-gyp builds for languages like Common Lisp.

Supported Grammars:

Note on Racket: Racket (.rkt) reuses the Scheme grammar. The #lang lines are parsed as an ERROR node, which tree-sitter recovers from, allowing the rest of the file to be extracted normally.

Chiasmus is a neurosymbolic verification engine that uses LLMs as semantic translators to map natural language problems into formal logic for mathematical solvers. The process follows a four-phase pipeline:

1. NORMALIZE: The LLM classifies the problem type and maps domain-specific inputs (e.g., AWS IAM JSON, Kubernetes RBAC) into a common intermediate format.
2. FORMALIZE: The system retrieves a matching template (Skill) based on the problem signature. The LLM then fills the slots in the template's skeleton.
3. VERIFY: The formalized logic is submitted to a solver (Z3 or Prolog). If errors occur, the system enters an Error Correction Loop, feeding error messages back to the LLM for up to 5 rounds of automated patching.
4. EXTRACT (Optional): Successfully solved problems can be generalized into new candidate skill templates for future reuse.

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                   │
└─────────────────────────────────┘

Chiasmus is best used when a problem requires proving properties about all possible inputs (e.g., finding if any input can trigger a specific conflict) rather than just checking specific cases.

When to use Chiasmus

• Constraint Problems: Use Chiasmus when you need mathematical guarantees and concrete counterexamples (e.g., Dependency Resolution, Validation Gaps).
• Proving Properties: Use Chiasmus to answer questions like "Can any request trigger both allow and deny?" or "Is there any input that passes frontend but fails backend?".
• Complex Constraints: Use Chiasmus when constraints are arbitrary in shape and would be difficult to implement manually in TypeScript.

When to use Traditional (TypeScript) approaches

• Simple Graph/Set Problems: For well-defined problems like BFS (Breadth-First Search) or set intersections, writing a few lines of TypeScript is often faster and more direct.
• Direct Algorithms: If the problem can be directly encoded as a standard algorithm, a traditional approach is simpler and avoids the SMT-LIB/Prolog formulation overhead.

Chiasmus provides two primary modes of reasoning: Solvers for formal correctness and Graph Analysis for structural code reasoning.

Use Solvers when you need formal guarantees:

• Universal correctness: Proving a property holds for ALL inputs (unlike LLMs which only check examples).
• Contradiction detection: Checking if rules conflict within combinatorial spaces.
• Reachability: Determining if state X can reach state Y.
• Critical systems: Access control, configurations, and dependency management where correctness is non-negotiable.

Use chiasmus_graph for structural code reasoning:

• Impact analysis: Finding what calls a specific function (blast radius).
• Dead code detection: Identifying functions unreachable from entry points.
• Taint analysis: Checking if user input can reach sensitive sinks (e.g., SQL queries) via call graph reachability.
• Dependency analysis: Detecting circular dependencies or reverse reachability.

A Skill is a parameterized formal specification used to solve recurring problems. It consists of a name, a domain, a solver type, a signature, a skeleton (the formal logic with placeholders), and normalization schemas.

Example Template Structure (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

Key Concepts:

• Slots: Placeholders like {{SLOT: rule_assertions}} that the LLM fills during the Formalize phase.
• Normalization Layer: Maps domain-specific formats (like AWS IAM or K8s RBAC) into the template's expected input format.
• Lifecycle: Skills start as learned candidates. After $N$ successful reuses, they are promoted: true. Unused skills are eventually pruned.

You can add tree-sitter support for any language by publishing an npm package named chiasmus-adapter-<language>. Chiasmus auto-discovers these at startup if adapterDiscovery is enabled in ~/.chiasmus/config.json.

Adapter Interface

An adapter must implement the LanguageAdapter interface:

Implementation Example

// 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.
    return { defines, calls, imports: [], exports: [], contains: [] };
  },
};

export default adapter;

Enabling Discovery

1. Install your adapter: npm install chiasmus-adapter-rust
2. Enable discovery in ~/.chiasmus/config.json:

{
  "adapterDiscovery": true
}