chiasmus: Instructions file for Codex

AGENTS.md — Chiasmus

Project Overview

Chiasmus is an MCP (Model Context Protocol) server that gives LLMs access to formal verification via Z3 (SMT solver) and SWI-Prolog (via prolog-wasm-full, including library(clpfd)). It also provides tree-sitter-based source code call graph analysis. The server 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.

• Language: TypeScript (strict mode, ESM)
• Runtime: Node.js ≥20
• License: Apache-2.0
• Package: npm package chiasmus, exposes a CLI binary

Commands

pnpm build          # Compile TypeScript (tsc) → dist/
pnpm typecheck      # Type-check only (tsc --noEmit)
pnpm test           # Run tests in watch mode (vitest)
pnpm test:run       # Run tests once (vitest run)
pnpm test:coverage  # Run tests with V8 coverage report
pnpm mcp            # Run MCP server locally via tsx

CI Pipeline

CI runs on push/PR to main (.github/workflows/test.yml):

1. pnpm install --frozen-lockfile
2. pnpm typecheck
3. pnpm test:run

Tested on Node 22 and 24. Minimum is Node 22 (better-sqlite3 13 requires it; Node 20 went EOL 2026-04-30).

Code Organization

src/
├── mcp-server.ts          # Entry point — MCP server, all tool handlers, CLI bootstrap
├── config.ts              # Loads ~/.chiasmus/config.json
├── solvers/
│   ├── types.ts           # SolverType, SolverResult (discriminated union), Solver, SolverInput
│   ├── session.ts         # SolverSession — factory for Z3/Prolog solver instances
│   ├── z3-solver.ts       # Z3 WASM wrapper (z3-solver npm), auto-strips check-sat/get-model
│   ├── prolog-solver.ts   # SWI-Prolog (prolog-wasm-full) wrapper, derivation tracing via assertz
│   └── correction-loop.ts # Bounded repair loop (delegates to repl-sandbox)
├── formalize/
│   ├── engine.ts          # FormalizationEngine — template selection, LLM slot-filling, solve pipeline
│   ├── validate.ts        # lintSpec — structural validation, auto-fixes for SMT-LIB/Prolog
│   └── feedback.ts        # classifyFeedback — converts SolverResult to human-readable feedback
├── skills/
│   ├── types.ts           # SkillTemplate, SlotDef, Normalization, SkillMetadata
│   ├── library.ts         # SkillLibrary — SQLite-backed template storage, BM25 search
│   ├── starters.ts        # 8 built-in starter templates (5 Z3, 3 Prolog)
│   ├── bm25.ts            # BM25 keyword search for template retrieval
│   ├── craft.ts           # craftTemplate — user-created template validation + storage
│   ├── learner.ts         # SkillLearner — LLM-driven template extraction from solutions
│   └── relationships.ts   # Template relationship/suggestion graph
├── graph/
│   ├── types.ts           # CodeGraph, LanguageAdapter, FileNode, Hyperedge, DefinesFact, CallsFact.calleeQN, ImportsFact.resolved, FileTypeInfo
│   ├── parser.ts          # tree-sitter lang registry + sync/async parse for TS/JS/Py/Go/Rust/Clojure/Scheme/Racket/CL
│   ├── extractor.ts       # AST walking + per-language call graph extraction + TS/JS collectTypeInfo
│   ├── extract-sexp.ts    # Scheme/Racket + Common Lisp extraction (scope-aware s-expression walkers)
│   ├── facts.ts           # graphToProlog — CodeGraph → Prolog facts (incl. calls_qn/3, imports_resolved/3)
│   ├── analyses.ts        # runAnalysis — dispatches all graph analyses
│   ├── native-analyses.ts # O(V+E) cycles/reachability/impact/dead-code/callers/callees
│   ├── graph-util.ts      # Shared helpers: buildUndirectedGraph, forEachUndirectedEdge, undirectedDegree
│   ├── community.ts       # Louvain community detection + cohesion score
│   ├── insights.ts        # detectHubs, detectBridges, detectSurprisingConnections
│   ├── diff.ts            # graphDiff — set diff on nodes + (src,tgt) edge keys
│   ├── entry-points.ts    # Heuristic entry-point detection (zero-in-degree exports)
│   ├── cache.ts           # SHA256 per-file cache + LRU eviction + named snapshots (proper-lockfile)
│   ├── mermaid.ts         # parseMermaid — Mermaid flowcharts/state diagrams → Prolog facts
│   ├── type-env.ts        # TS/JS three-tier type inference + class field/method extraction
│   ├── resolve-calls.ts   # Project-wide QN resolution: inheritance-aware field/method registry
│   ├── tsconfig-aliases.ts # Parses tsconfig.json paths/baseUrl with JSONC + extends chain
│   ├── suffix-index.ts    # Suffix index over batch files for relative import resolution
│   └── adapter-registry.ts # Auto-discovery of chiasmus-adapter-* npm packages
├── search/
│   ├── engine.ts          # buildSearchCorpus + runSearch — cosine-sim code search
│   ├── vector-store.ts    # In-process linear-scan store; serializable
│   ├── embedding-cache.ts # SHA-256-keyed persistent cache, atomic writes
│   └── index.ts           # Module exports
├── llm/
│   ├── types.ts           # LLMAdapter + EmbeddingAdapter interfaces, LLMMessage
│   ├── anthropic.ts       # Anthropic/DeepSeek/OpenAI provider factories (createLLMFromEnv, createEmbeddingFromEnv)
│   ├── openai-compatible.ts # OpenAI-compatible chat + embedding adapters
│   └── mock.ts            # Mock LLM + MockEmbeddingAdapter for testing
tests/                      # Unit tests (mirrors src/ structure)
benchmark/                  # Benchmark problems (5 problems × traditional + chiasmus implementations)