Skip to content
appsgit

Chiasmus

Chiasmus is an MCP server that gives LLMs access to formal verification via Z3 (SMT solver) and SWI-Prolog (via prolog-wasm-full, includes library(clpfd)), plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results… It has 214 GitHub stars, is released under the Apache-2.0 license and runs locally with npx -y chiasmus.

github.com/yogthos/chiasmus (opens in a new tab)

View on GitHub (opens in a new tab)

Install Chiasmus

Generated from the server's published package. Replace your-value with your own values.

Claude Desktop

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

Settings > Developer > Edit Config. macOS: ~/Library/Application Support/Claude/, Windows: %APPDATA%\Claude\. Restart Claude Desktop afterwards.

Claude Code

claude mcp add --transport stdio chiasmus -- npx -y chiasmus

Cursor

.cursor/mcp.json
{
  "mcpServers": {
    "chiasmus": {
      "type": "stdio",
      "command": "npx",
      "args": [
        "-y",
        "chiasmus"
      ]
    }
  }
}

Project file; use ~/.cursor/mcp.json to enable it in every project.

VS Code

.vscode/mcp.json
{
  "servers": {
    "chiasmus": {
      "type": "stdio",
      "command": "npx",
      "args": [
        "-y",
        "chiasmus"
      ]
    }
  }
}

Config formats checked against the official docs on Oct 7, 2026: modelcontextprotocol.io (opens in a new tab), code.claude.com (opens in a new tab), cursor.com (opens in a new tab), code.visualstudio.com (opens in a new tab).

About Chiasmus

MCP server that gives LLMs access to formal verification via Z3 (SMT solver) and SWI-Prolog (via prolog-wasm-full, includes library(clpfd)), 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.

  • formalmethods
  • llm
  • mcp
  • prolog
  • z3-smt-solver
  • ai-agents
  • ai-assistant
  • ai-tools
  • mcp-server

Similar MCP servers

More developer tools MCP servers

All Developer tools

FAQ

Chiasmus FAQ

Still curious? Email info@appsgit.com.

What is Chiasmus?

Chiasmus is an MCP server that gives LLMs access to formal verification via Z3 (SMT solver) and SWI-Prolog (via prolog-wasm-full, includes library(clpfd)), plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results… It has 214 GitHub stars, is released under the Apache-2.0 license and runs locally with npx -y chiasmus. The source code is at github.com/yogthos/chiasmus.

How do I install the Chiasmus MCP server?

Add the command npx -y chiasmus to your MCP client: put it in claude_desktop_config.json for Claude Desktop, run claude mcp add for Claude Code, or add it to .cursor/mcp.json (Cursor) or .vscode/mcp.json (VS Code). The snippets on this page are ready to paste.

Is Chiasmus free?

The server is open source under the Apache-2.0 license, so running it is free. It does not declare any required API key.

Is Chiasmus actively maintained?

The most recent commit was on Sep 4, 2026. appsgit only lists MCP servers with a commit in the last six months and re-checks every server daily.