Chiasmus is an MCP server that gives language models access to formal verification
{
"mcpServers": {
"chiasmus": {
"command": "<see-readme>",
"args": []
}
}
}No install config available. Check the server's README for setup instructions.
Are you the author?
Add this badge to your README to show your security score and help users find safe servers.
Chiasmus is an MCP server that gives language models access to formal verification
Is it safe?
No package registry to scan.
No authentication — any process on your machine can connect.
Apache-2.0. View license →
Is it maintained?
Last commit 0 days ago. 44 stars.
Will it work with my client?
Transport: stdio. Works with Claude Desktop, Cursor, Claude Code, and most MCP clients.
No automated test available for this server. Check the GitHub README for setup instructions.
No known vulnerabilities.
This server is missing a description. Tools and install config are also missing.If you've used it, help the community.
Add informationHave you used this server?
Share your experience — it helps other developers decide.
Sign in to write a review.
A Model Context Protocol (MCP) server and CLI that provides tools for agent use when working on iOS and macOS projects.
Dynamic problem-solving through sequential thought chains
A Model Context Protocol server for searching and analyzing arXiv papers
The Apify MCP server enables your AI agents to extract data from social media, search engines, maps, e-commerce sites, or any other website using thousands of ready-made scrapers, crawlers, and automation tools available on the Apify Store.
MCP Security Weekly
Get CVE alerts and security updates for Chiasmus and similar servers.
Start a conversation
Ask a question, share a tip, or report an issue.
Sign in to join the discussion.
MCP server that gives LLMs access to formal verification via Z3 (SMT solver) and Tau Prolog, 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.
chiasmus_review returns a phased recipe of graph analyses + verification templates, and you execute it step-by-stepnpm install -g chiasmus
claude mcp add chiasmus -- npx -y chiasmus
Or add to ~/.claude/settings.json:
{
"mcpServers": {
"chiasmus": {
"command": "npx",
"args": ["-y", "chiasmus"]
}
}
}
Add to crush.json:
{
"mcp": {
"chiasmus": {
"type": "stdio",
"command": "npx",
"args": ["-y", "chiasmus"]
}
}
}
Add to opencode.json:
{
"mcp": {
"chiasmus": {
"type": "local",
"command": ["npx", "-y", "chiasmus"]
}
}
}
chiasmus_verify — Submit raw SMT-LIB or Prolog, get a verified result. Z3 UNSAT results include an unsatCore showing which assertions conflict. Prolog supports explain=true for derivation traces showing which rules fired.
chiasmus_verify solver="z3" input="
(declare-const x Int)
(assert (! (> x 10) :named gt10))
(assert (! (< x 5) :named lt5))
"
→ { status: "unsat", unsatCore: ["gt10", "lt5"] }
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)"] }
chiasmus_verify also accepts format="mermaid" with solver="prolog" to parse Mermaid flowcharts and state diagrams directly into Prolog facts:
chiasmus_verify solver="prolog" format="mermaid"
input="graph TD\n UserInput --> Validator\n Validator --> DB\n Validator --> Logger"
query="reaches(userinput, db)."
→ { status: "success", answers: [{}] }
chiasmus_verify solver="prolog" format="mermaid"
input="stateDiagram-v2\n Idle --> Active : start\n Active --> Done : finish"
query="can_reach(idle, done)."
→ { status: "success", answers: [{}] }
chiasmus_graph — Analyze source code call graphs via tree-sitter + Prolog. Parses source files, extracts cross-module call graphs, runs formal analyses.
Built-in language support: TypeScript, JavaScript, Python, Go, Clojure/ClojureScript. Additional languages can be added via custom adapters.
chiasmus_graph files=["src/server.ts", "src/db.ts"] analysis="callers" target="query"
→ { analysis: "callers", result: ["handleRequest"] }
chiasmus_graph files=["src/**/*.ts
... [View full README on GitHub](https://github.com/yogthos/chiasmus#readme)