Loading ToolBench
Neurosymbolic verification engine - MCP server for formal reasoning with Z3 and SWI-Prolog (WASM)
Chiasmus defines 12 tools with explicit names, descriptions, and input schemas visible in src/mcp-server.ts. However, significant gaps exist: (1) Output schemas are NOT documented for any tool, descriptions state what tools return (e.g., 'verified result', 'overview maps') but no structured field definitions are provided, forcing LLMs to infer output shape. (2) Parameter descriptions are present but often terse and domain-specific, lacking guidance on constraints, format, or LLM selection logic. (3) Many tools have complex behavior with undocumented interdependencies (chiasmus_verify requires API keys for certain solvers; chiasmus_solve depends on API keys and falls back to chiasmus_formalize without guidance on when this happens). (4) Error handling is not documented, no guidance on what errors to expect, recovery paths, or how to interpret solver results (e.g., 'converged: true does NOT mean property holds'). (5) Several tools operate on domain-specific concepts (Prolog tabling, Z3 SMT-LIB, unsatCore, derivation traces) with technical descriptions that assume deep formal-verification knowledge, reducing accessibility for general LLM agents. Per-tool analysis shows chiasmus_verify and chiasmus_solve have strong schemas but weak output documentation; chiasmus_graph and chiasmus_map have extensive analysis types but parameter descriptions are sparse; chiasmus_lint has good auto-fix documentation but limited error guidance.
Save/load extraction cache snapshots for reproducible analysis. USE: save → snapshot current cached extractions load → restore from snapshot (resets cold cache) list → show available snapshots delete → remove snapshot
Extract call graph from source code. Low-level tool (used by chiasmus_graph internally). Returns: defines (functions/types), calls (dependencies), imports (cross-file). Languages: TypeScript, JavaScript, Python, Go, Rust, Clojure, Scheme, Racket, Common Lisp.
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
Analyze source-code call graphs (tree-sitter + Prolog). Absolute paths only. Languages: TypeScript, JavaScript, Python, Go, Rust, Clojure, Scheme, Racket, Common Lisp. ANALYSES: summary overview counts callers who calls target (needs target) callees what target calls (needs target) reachability can from reach to (needs from, to) path shortest chain from→to (needs from, to) impact transitive callers of target (needs target) dead-code unreachable functions (methods excluded) cycles circular call dependencies layer-violation calls that skip layers (handlers→db bypassing services) communities modular clusters (Louvain algorithm) hubs high-degree functions bridges functions linking clusters surprises unexpected connections facts export as Prolog facts (edges/defines) diff changed callees between two versions (needs before/after) entry-points user-facing functions (roots, exports, mains)
No output schemas documented for any tool. Tool descriptions state what is returned ('verified result', 'overview maps') but provide no structured field definitions. LLMs cannot infer result shapes and cannot plan downstream tool calls without field-level documentation.
chiasmus_solve falls back to chiasmus_formalize silently when API keys are absent ('Without key → falls back to chiasmus_formalize'). This behavior is undocumented in parameter descriptions and will confuse agents planning tool selection, they cannot distinguish when to call solve vs. formalize based on available parameters.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 59 | 2026-07-28+ | v2 |
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.
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.
Generate codebase overview maps (text, mermaid, html). MODES: overview directory tree + symbol counts per file file detailed symbol list + call graph snippet for one file symbol signature + callers + callees for one symbol FORMATS: text clean ASCII mermaid flowchart/graph html interactive (use with Claude Artifacts)
Parse Mermaid diagram (flowchart, stateDiagram, etc.) → Prolog facts. Useful for converting visual specifications into formal logic for verification.
Plan a structured code review. Suggests focus areas (coverage gaps, risky patterns, deprecated APIs) and templates. WORKFLOW: 1. chiasmus_review → review plan + focus suggestions 2. Review code manually or with AI, following the plan 3. chiasmus_verify → formalize findings if needed
Search/list formalization templates. Returns skeletons, slots, normalization recipes, usage metadata. Find template before chiasmus_verify or chiasmus_formalize. query: "access control policies conflict" → search solver: "prolog" → filter by solver name: "policy-contradiction" → exact lookup
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: `converged: true` means the correction loop reached a non-error solver result — it does NOT mean the property holds. Read `result.status` (sat / unsat / unknown) for the actual verdict; an `unsat` ("no counterexample in this model") is not a proof.
Submit formal logic to solver. Returns verified result. SOLVERS: z3 — SMT-LIB format → SAT + model | UNSAT + unsatCore | error prolog — facts/rules + query goal → answers | error FORMAT (optional, prolog only): mermaid — parse Mermaid flowchart/stateDiagram → Prolog facts + reachability rules Z3 RULES: ⚠ UNSAT results include unsatCore — use (assert (! expr :named label)) for readable conflict labels ⚠ No (check-sat)/(get-model) — added automatically ⚠ Use (= flag (or ...)) NOT (=> ... flag) — implication → trivially SAT ⚠ No (define-fun) with args — breaks model extraction. Use (declare-const) + (assert (=)) instead PROLOG RULES: ⚠ All clauses end with period ⚠ No recursive reachability on cyclic graphs without tabling → infinite loop. Add ":- table reach/2." (SWI tabling), or query edges individually and BFS externally. ⚠ Use "queries" param (JSON array) to batch multiple queries against same program in one call
Critical domain-specific guidance buried in tool descriptions without LLM-optimized separation. chiasmus_verify embeds technical rules (Z3 RULES, PROLOG RULES, assertions about unsatCore/tabling) inline, requiring LLMs to parse 300+ character blocks. These rules should be extracted into parameter constraint documentation or separate structured guidance fields.
chiasmus_solve explicitly warns 'converged: true does NOT mean property holds. Read result.status (sat / unsat / unknown)', this critical distinction is buried in description text, not documented as an output field or error case. Agents may misinterpret convergence as proof.
chiasmus_graph analysis parameter accepts 16 enum values (summary, callers, callees, etc.) but several analyses have undocumented parameter dependencies (e.g., 'callers' needs 'target', 'reachability' needs 'from' and 'to'). These dependencies are not enforced in descriptions and will cause silent failures or incorrect results when omitted.
No error handling or recovery guidance documented for any tool. No guidance on retryable errors, user-fixable errors, or fatal errors. Example: chiasmus_verify calling Z3 may return UNSAT, is this a failure requiring retry, or a valid answer? Agents cannot determine next action.
chiasmus_graph and chiasmus_map paths parameters accept 'Absolute file paths or directory roots' but no constraint documentation on size limits, symbolic link traversal, or permission scope. MAX_FILE_SIZE is referenced in code (runAnalysis, MAX_FILE_SIZE) but not exposed in parameter descriptions.
chiasmus_learn and chiasmus_solve require 'ANTHROPIC_API_KEY | DEEPSEEK_API_KEY | OPENAI_API_KEY' but this dependency is buried in tool descriptions, not enforced as a precondition. Agents will not know these tools require external API configuration until invocation fails.
chiasmus_cache_snapshot 'load' action 'resets cold cache', this destructive behavior is not flagged in naming or parameter description. Agents may invoke load expecting a benign restore and lose prior analysis state.
chiasmus_parse_mermaid parameter 'diagram' has no format constraints (flowchart vs stateDiagram syntax). Tool description mentions both but does not validate or guide LLM on Mermaid dialect choice.