Chiasmus

What it does

Chiasmus provides language models with access to formal verification and neurosymbolic reasoning. By leveraging Z3 (SMT solver) and SWI-Prolog, it allows AI agents to prove correctness, detect contradictions in RBAC rules, analyze call graphs for dead code, and verify system invariants with mathematical certainty.

Tools

• chiasmus_verify: Submit SMT-LIB or Prolog specs to get verified results, including unsat cores and derivation traces.
• chiasmus_graph: Perform deep structural analysis of source code (TypeScript, JS, Python, Go, Clojure) including reachability and impact analysis.
• chiasmus_map: Generate a compact codebase outline for agents to consult before reading files.
• chiasmus_skills: Search a library of verification templates for common problems like authorization and dependency resolution.
• chiasmus_formalize: Match natural language problems to formal verification templates.
• chiasmus_solve: End-to-end pipeline that formalizes, solves, and corrects logic specs.
• chiasmus_review: Generate a phased code-review recipe based on structural and formal analysis.
• chiasmus_search: Semantic code search using embeddings to find logic by meaning.

Installation

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

Supported hosts

• Claude Code
• Claude Desktop
• Crush
• OpenCode