Atlas / MCP servers / yogthos / Chiasmus

ChiasmusCAUTION

Name: Chiasmus
Author: yogthos

mcp/yogthos/chiasmus

MCP server by yogthos · ai agents · ai assistant · ai tools · Audited 2026-10-06

⚑ Report / re-scan Source ↗

Chiasmus is an MCP server that gives language models access to formal verification

Verdict

CAUTION

Grade

Trust score

89 /100

Exposed tools

65 61r · 4w · 0d

Transport

stdio

License

Apache-2.0

Stars

214

Overview

From the repository's own README, as read at the audited commit. Badges and raw HTML are left out.

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.

Example use cases

"Can our RBAC rules ever conflict?" → Z3 finds the exact role/action/resource triple where allow and deny both fire
"Find compatible package versions" → Z3 solves dependency constraints with incompatibility rules, returns a valid assignment or proves none exists
"Can user input reach the database?" → Prolog traces all paths through the call graph, flags taint flows to sensitive sinks
"Are our frontend and backend validations consistent?" → Z3 finds concrete inputs that pass one but fail the other (e.g. age=15 passes frontend min=13 but fails backend min=18)
"Does our workflow have dead-end or unreachable states?" → Prolog checks reachability from the initial state, identifies orphaned and terminal nodes
"What's the dead code in this module?" → tree-sitter parses source files, Prolog finds functions unreachable from any entry point
"What breaks if I change this function?" → call graph impact analysis shows all transitive callers
"Do a full code review of these files" → chiasmus_review returns a phased recipe of graph analyses + verification templates, and you execute it step-by-step

Setup

npm install -g chiasmus

Claude Code

claude mcp add chiasmus -- npx -y chiasmus

Or add to ~/.claude/settings.json:

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

Crush

Add to crush.json:

{
"mcp": {
"chiasmus": {
"type": "stdio",
"command": "npx",
"args": ["-y

Read from source at commit 4479e3f8fc7aOBSERVED · 2026-10-06

Connect

Built from this server's own package name, version and transport as found in its source — not copied from anyone's documentation, so it cannot drift against a page we do not control. Replace the environment placeholders with a token scoped to the least it needs.

claude-code

claude mcp add chiasmus --env ANTHROPIC_API_KEY=${ANTHROPIC_API_KEY} --env AZURE_OPENAI_API_KEY=${AZURE_OPENAI_API_KEY} --env DEEPSEEK_API_KEY=${DEEPSEEK_API_KEY} --env OPENAI_API_KEY=${OPENAI_API_KEY} -- npx -y [email protected]

claude-desktop

{
  "mcpServers": {
    "chiasmus": {
      "command": "npx",
      "args": [
        "-y",
        "[email protected]"
      ],
      "env": {
        "ANTHROPIC_API_KEY": "${ANTHROPIC_API_KEY}",
        "AZURE_OPENAI_API_KEY": "${AZURE_OPENAI_API_KEY}",
        "DEEPSEEK_API_KEY": "${DEEPSEEK_API_KEY}",
        "OPENAI_API_KEY": "${OPENAI_API_KEY}"
      }
    }
  }
}

Exposed tools (65)

61 read · 4 write · 0 destructive.

Tool	Risk	Description
`access_rules`	read	OR of conditions that grant access
`action_type`	read	Type name for actions
`allow_rules`	read	OR of all allow conditions — each is (and (= r X) (= a Y) (= res Z))
`call_facts`	read	Prolog facts of the form calls(Function, Operation) — which function calls which operation
`chiasmus_formalize`	read	Find best template for problem → return skeleton + slot-filling instructions + tips. Guided workflow: 1. chiasmus_formalize → get template + slots + tips 2. Fill slots using your context 3. chiasmus_verify → verified result
`chiasmus_learn`	write	Extract reusable template from verified solution → add to skill library. Generalizes concrete spec into parameterized template. Stored as candidate → promoted after 3+ successful reuses. Needs API key. Flow: chiasmus_verify → chiasmus_learn → template appears in chiasmus_skills.
`chiasmus_lint`	read	Fast structural validation of formal spec without running solver. Auto-fixes: markdown fences, (check-sat)/(get-model), (set-logic). Checks: balanced parens, unfilled {{SLOT:}} markers, missing periods (Prolog). Returns cleaned spec + fixes applied + remaining errors.
`chiasmus_map`	read	Pre-built codebase map — read before bulk file reads. Returns a compact outline derived from the tree-sitter call graph: per-file headlines with exports, signatures, token estimates, leading doc. Lets you answer
`chiasmus_review`	write	Phased code-review recipe — which tools to run, in what order, what to flag. Pure plan, no side effects. Execute phases sequentially; each action carries
`chiasmus_skills`	read	Search/list formalization templates. Returns skeletons, slots, normalization recipes, usage metadata. Find template before chiasmus_verify or chiasmus_formalize. query:
`chiasmus_solve`	read	End-to-end: select template → fill slots → lint → verify → correction loop. Needs ANTHROPIC_API_KEY \| DEEPSEEK_API_KEY \| OPENAI_API_KEY. Without key → falls back to chiasmus_formalize. Returns: solver result + template used + correction history. NOTE: \
`computation`	read	Expression computing the result from inputs
`condition`	read	Test condition
`config_a_expr`	read	Boolean expression for config A
`config_b_expr`	read	Boolean expression for config B
`declarations`	read	Variable declarations
`deny_rules`	read	OR of all deny conditions — each is (and (= r X) (= a Y) (= res Z))
`dependencies`	read	Dependency edges
`dependency_rules`	read	Conditional version requirements. Use (=>) for
`domain_constraints`	read	Boolean expression constraining valid input ranges (single expression)
`edges`	read	Direct edges as edge(from, to) facts
`extra_slot`	read	Extra
`facts`	read	Ground facts about the domain
`field_declarations`	read	Declare variables for each input field
`flow_facts`	read	Prolog facts of the form flows(From, To) — data flow from one function/variable to another
`function_body`	read	SMT-LIB assertions defining the input→output relationship (the function
`incompatibility_rules`	read	Pairs of versions that cannot coexist
`input`	read	test input
`input_declarations`	read	Declare input variables covering the input space
`label`	read	The label/property name to propagate (used as both predicate name and prefix)
`permissions`	read	What each role can do
`postcondition`	read	Boolean expression the result should satisfy (will be negated to find violations)
`precondition`	read	Boolean expression constraining valid inputs (wrapped as single expression)
`principal_type`	read	Type name for principals
`range_a_constraints`	read	First port range bounds
`range_b_constraints`	read	Second port range bounds
`range_constraints`	read	Constrain each package to its available versions using (or (= pkg v1) (= pkg v2) ...)
`range_declarations`	read	Port range variables
`required_pairs`	read	Prolog facts of the form required_pair(OperationA, OperationB) — B must appear whenever A appears
`resource_type`	read	Type name for resources
`result_declarations`	read	Declare output/result variables
`result_type`	read	Type of the result variable
`role_assignments`	read	Which users have which roles
`role_hierarchy`	read	Role inheritance relationships
`rule_a`	read	First rule expression
`rule_b`	read	Second rule expression
`rule_set_a_conditions`	write	Conjunction of conditions for rule set A (e.g. frontend validation)
`rule_set_b_conditions`	write	Conjunction of conditions for rule set B (e.g. backend validation)
`rules`	read	Prolog rules that derive conclusions from facts
`sanitizers`	read	Prolog facts of the form sanitize(Node) — functions that clean/escape tainted data
`seed_labels`	read	Prolog facts of the form label(Function) — functions with known classification
`sinks`	read	Prolog facts of the form sink(Node) — security-sensitive operations that must not receive tainted data
`source_state`	read	The source state to check
`state_declarations`	read	SMT-LIB declare-datatypes for all states in the machine
`state_type`	read	Type name for the state enumeration
`subject`	read	the subject atom
`taint_sources`	read	Prolog facts of the form taint_source(Node, TaintType) — origins of untrusted data
`target_principal`	read	The principal to check
`target_resource`	read	The resource to check
`target_state`	read	The target state to check reachability for
`transitions`	read	OR of valid transition pairs — each is (and (= from S1) (= to S2))
`type_declarations`	read	SMT-LIB declare-datatypes for principals, actions, resources
`version_declarations`	read	Declare an Int variable for each package version
`violation_condition`	read	The condition that would indicate a bug (result out of bounds, negative, overflow, etc.)
`x`	read	test

Trust audit

CAUTIONgrade B · trust 89/100 Install with care. The audit found things worth knowing before you trust its output.

Layer	What it checks	Result
L0	Provenance & inventory	WARN
L1	Static analysis of the code	PASS
L2	Instruction surface (what it tells the agent)	PASS
L3	Class-specific surface	PASS
L4	Behavioural (sandbox)	SKIPPED

What the source does

Filesystem: declared (1 observation(s))
Network: declared (4 observation(s))
Shell: none-observed
Dependencies: not all pinned
Secrets in source: none-found

Findings (8)

MEDIUMInventory / provenance · inv.binary · CWE-1104

grammars/tree-sitter-commonlisp.wasm

tree-sitter-commonlisp.wasm

Why it matters. a compiled or binary member cannot be reviewed from source

Fix. ship source, or explain the binary in the README

MEDIUMInventory / provenance · inv.binary · CWE-1104

grammars/tree-sitter-scheme.wasm

tree-sitter-scheme.wasm

Why it matters. a compiled or binary member cannot be reviewed from source

Fix. ship source, or explain the binary in the README