chiasmus

yogthos/chiasmus
★ 153 stars TypeScript 🤖 AI/LLM Updated today
Chiasmus is an MCP server that gives language models access to formal verification
View on GitHub →

Quick Install

Copy the config for your editor. Some servers may need additional setup — check the README.

Add to claude_desktop_config.json:

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

README Excerpt

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.

Tools (20)

ANTHROPIC_API_KEYCHIASMUS_API_URLCHIASMUS_CACHE_DIRCHIASMUS_CACHE_MAX_PER_REPOCHIASMUS_HOMECHIASMUS_MODELDEEPSEEK_API_KEYOPENAI_API_KEYadapterDiscoverychiasmuschiasmus_verifydeclarationsextensionsextractgrammarhandleRequestlanguagelimit_alimit_brefreshAccessToken

Topics

ai-agentsai-assistantai-toolsformalmethodsllmmcpmcp-serverprologz3-smt-solver