{
  "markdown": "<!-- mcp-name: io.github.egoughnour/curate-ipsum -->\n\n# Curate-Ipsum\n\n**A graph-spectral MCP server for verified code synthesis through belief revision**\n\n[![PyPI](https://img.shields.io/pypi/v/curate-ipsum?style=flat-square&logo=pypi&logoColor=white)](https://pypi.org/project/curate-ipsum/)\n[![MCP Registry](https://img.shields.io/badge/MCP-Registry-blue?style=flat-square&logo=anthropic&logoColor=white)](https://registry.mcp.so/servers/io.github.egoughnour/curate-ipsum)\n[![Claude Desktop](https://img.shields.io/badge/Claude-Desktop-orange?style=flat-square&logo=anthropic&logoColor=white)](https://github.com/egoughnour/curate-ipsum/releases/latest/download/curate-ipsum.mcpb)\n[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg?style=flat-square)](https://opensource.org/licenses/MIT)\n[![Python](https://img.shields.io/pypi/pyversions/curate-ipsum?style=flat-square&logo=python&logoColor=white)](https://pypi.org/project/curate-ipsum/)\n\n[![Top Language](https://img.shields.io/github/languages/top/egoughnour/curate-ipsum?style=flat-square&color=3379ef)](https://github.com/egoughnour/curate-ipsum)\n[![Code Size](https://img.shields.io/github/languages/code-size/egoughnour/curate-ipsum?style=flat-square&color=3379ef)](https://github.com/egoughnour/curate-ipsum)\n[![Last Commit](https://img.shields.io/github/last-commit/egoughnour/curate-ipsum?style=flat-square&color=2579ef&logo=github)](https://github.com/egoughnour/curate-ipsum/commits/main)\n[![Repo Size](https://img.shields.io/github/repo-size/egoughnour/curate-ipsum?style=flat-square&color=3379ef)](https://github.com/egoughnour/curate-ipsum)\n\nCurate-Ipsum bridges the gap between LLM-generated code (fast, plausible, unverified) and formally verified patches (slow, correct, trustworthy). It treats mutation testing as one component of a larger system for maintaining robust, self-healing codebase metadata that supports reachability analysis, symbolic execution, and automated test generation.\n\n## Install\n\n```bash\n# PyPI\npip install curate-ipsum\n\n# or with uv\nuv pip install curate-ipsum\n\n# Docker (includes baked-in embedding model)\ndocker pull ghcr.io/egoughnour/curate-ipsum:latest\n```\n\n### Claude Desktop / MCP Client\n\nAdd to your `claude_desktop_config.json`:\n\n```json\n{\n  \"mcpServers\": {\n    \"curate-ipsum\": {\n      \"command\": \"uvx\",\n      \"args\": [\"curate-ipsum\"]\n    }\n  }\n}\n```\n\nOr with Docker (embedding model pre-loaded, no Python needed):\n\n```json\n{\n  \"mcpServers\": {\n    \"curate-ipsum\": {\n      \"command\": \"docker\",\n      \"args\": [\"run\", \"-i\", \"--rm\", \"ghcr.io/egoughnour/curate-ipsum:latest\"]\n    }\n  }\n}\n```\n\n## MCP Tools\n\nCurate-Ipsum exposes 30 tools over the MCP stdio transport, organised into six groups:\n\n**Testing** — `run_unit_tests`, `run_integration_tests`, `run_mutation_tests`, `get_run_history`, `get_region_metrics`, `detect_frameworks`, `parse_region`, `check_region_relationship`, `create_region`\n\n**Belief Revision** — `add_assertion`, `contract_assertion`, `revise_theory`, `get_entrenchment`, `list_assertions`, `get_theory_snapshot`, `store_evidence`, `get_provenance`, `why_believe`, `belief_stability`\n\n**Rollback & Failure** — `rollback_to`, `undo_last_operations`, `analyze_failure`, `list_world_history`\n\n**Graph-Spectral** — `extract_call_graph`, `compute_partitioning`, `query_reachability`, `get_hierarchy`, `find_function_partition`, `incremental_update`, `persistent_graph_stats`, `graph_query`\n\n**Verification** — `verify_property` (Z3/angr), `verify_with_orchestrator` (CEGAR budget escalation), `list_verification_backends`\n\n**Synthesis & RAG** — `synthesize_patch` (CEGIS + genetic + LLM), `synthesis_status`, `cancel_synthesis`, `list_synthesis_runs`, `rag_index_nodes`, `rag_search`, `rag_stats`\n\n## Current Status\n\n**Last Updated**: 2026-02-08\n\n| Component | Status |\n|-----------|--------|\n| Multi-framework parsing (5 frameworks) | Complete |\n| Graph Infrastructure (Spectral/Kameda) | Complete |\n| Belief Revision Engine (AGM/Provenance) | Complete |\n| Synthesis Loop (CEGIS/Genetic) | Complete |\n| Verification Backends (Z3/angr) | Complete |\n| Graph Persistence (SQLite/Kuzu) | Complete |\n| RAG / Semantic Search (Chroma) | Complete |\n\n## The Problem\n\nLLMs produce code that is:\n- ✅ Syntactically valid (usually)\n- ✅ Statistically plausible\n- ❌ Semantically correct (sometimes)\n- ❌ Type-safe (by accident)\n- ❌ Formally verified (never)\n\nCurrent approaches either trust LLM output blindly or reject it entirely. Neither is optimal.\n\n## The Solution\n\nUse LLMs for **cheap candidate generation**, then invest computational resources to achieve **formal guarantees**:\n\n```\nLLM Candidates (k samples)\n        ↓\n   Seed Population\n        ↓\n┌───────────────────────────┐\n│  CEGIS + CEGAR + Genetic  │  ← Verification loop\n│  + Belief Revision        │\n└───────────────────────────┘\n        ↓\n  Strongly Typed Patch\n  (with proof certificate)\n```\n\n## Key Differentiators from State of the Art\n\n### vs. Traditional Mutation Testing (Stryker, mutmut, cosmic-ray)\n\n| Traditional | Curate-Ipsum |\n|-------------|--------------|\n| Single tool, single language | Multi-framework orchestration |\n| Flat file-level analysis | Hierarchical graph-spectral decomposition |\n| Mutation score as output | Mutation testing as *input* to synthesis |\n| No formal verification | CEGIS/CEGAR verification loop |\n| Manual test writing | Automated patch generation |\n\n### vs. LLM Code Generation (Copilot, Claude, GPT)\n\n| LLM-only | Curate-Ipsum |\n|----------|--------------|\n| Trust model output | Verify model output |\n| Single sample or best-of-k | Population-based refinement |\n| No formal guarantees | Proof certificates |\n| Stateless generation | Belief revision with provenance |\n| Plausible code | Provably correct code |\n\n### vs. Program Synthesis (Sketch, Rosette, SyGuS)\n\n| Traditional Synthesis | Curate-Ipsum |\n|----------------------|--------------|\n| Hand-written sketches | LLM-generated candidates |\n| Cold-start search | Warm-start from LLM population |\n| No learning across runs | Totalizing theory accumulates knowledge |\n| Single specification | Multi-framework implicit regions |\n\n### vs. Symbolic Execution (KLEE, S2E)\n\n| Symbolic Execution | Curate-Ipsum |\n|-------------------|--------------|\n| Path exploration only | Integrated with synthesis |\n| Boolean constraint solving | Mathematical reformulation (SymPy) |\n| Single-tool analysis | Graph DB + SMT + mutation orchestration |\n| No code generation | Generates verified patches |\n\n### Novel Contributions\n\n1. **Graph-Spectral Code Decomposition**\n   - Fiedler vector partitioning for optimal reachability\n   - Hierarchical SCC condensation\n   - Planar subgraph identification → O(1) Kameda queries\n   - Kuratowski subgraphs as atomic non-planar units\n\n2. **Belief Revision for Synthesis**\n   - AGM-compliant theory revision\n   - Entrenchment ordering for minimal contraction\n   - Provenance DAG for failure mode analysis\n   - Rollback sharpens validity (failures refine the universal model)\n\n3. **Implicit Region Detection**\n   - Spectral anomalies reveal undertested code\n   - Cross-framework mutation resistance identifies critical regions\n   - Historical mutability guides partition optimization\n\n4. **Mathematical Constraint Reformulation**\n   - Boolean-intractable → differential/root-finding\n   - SymPy path condition encoding\n   - Hybrid SMT + numerical solving\n\n## Architecture\n\n```mermaid\nflowchart TB\n    subgraph MCP[\"MCP Interface\"]\n        direction TB\n\n        subgraph Sources[\"Analysis Sources\"]\n            direction LR\n            MUT[\"🧬 Mutation<br/>Orchestrator<br/><small>Stryker<br/>mutmut<br/>cosmic-ray</small>\"]\n            SYM[\"🔬 Symbolic<br/>Execution<br/><small>KLEE · Z3<br/>SymPy</small>\"]\n            GRAPH[\"📊 Graph<br/>Analysis<br/><small>Joern<br/>Neo4j<br/>Fiedler</small>\"]\n        end\n\n        MUT --> BRE\n        SYM --> BRE\n        GRAPH --> BRE\n\n        BRE[\"🧠 Belief Revision Engine<br/><small>AGM Theory · Entrenchment · Provenance DAG</small>\"]\n\n        BRE --> SYNTH\n\n        SYNTH[\"⚙️ Synthesis Loop<br/><small>CEGIS · CEGAR · Genetic Algorithm</small>\"]\n\n        SYNTH --> |\"counterexample\"| BRE\n\n        SYNTH --> OUTPUT\n\n        OUTPUT[\"✅ Strongly Typed Patch<br/><small>Proof Certificate ·Type Signature<br/>Pre/Post Conditions</small>\"]\n    end\n\n    LLM[\"🤖 LLM Candidates<br/><small>top-k samples</small>\"] --> SYNTH\n\n    style MCP fill:#1a1a2e,stroke:#16213e,color:#eee\n    style Sources fill:#16213e,stroke:#0f3460,color:#eee\n    style MUT fill:#0f3460,stroke:#e94560,color:#eee\n    style SYM fill:#0f3460,stroke:#e94560,color:#eee\n    style GRAPH fill:#0f3460,stroke:#e94560,color:#eee\n    style BRE fill:#533483,stroke:#e94560,color:#eee\n    style SYNTH fill:#e94560,stroke:#ff6b6b,color:#fff\n    style OUTPUT fill:#06d6a0,stroke:#118ab2,color:#000\n    style LLM fill:#ffd166,stroke:#ef476f,color:#000\n```\n\n## Roadmap\n\n### Phase 1: Foundation ✅\n- [x] MCP server infrastructure\n- [x] Stryker report parsing\n- [x] Run history and PID metrics\n- [x] Flexible region model (hierarchical: file → class → function → lines)\n- [x] mutmut parser integration\n- [x] Framework auto-detection\n- [x] Unified parser interface\n\n### Phase 2: Graph Infrastructure ✅\n- [x] Graph models (CodeGraph, Node, Edge)\n- [x] Call graph extraction (AST-based)\n- [x] ASR extractor (import/class analysis)\n- [x] Dependency graph extraction (module-level imports)\n- [x] Laplacian construction from call/dependency graphs\n- [x] Fiedler vector computation (scipy.sparse.linalg)\n- [x] Recursive Fiedler partitioning with virtual sink/source\n- [x] SCC detection and hierarchical condensation\n- [x] Planar subgraph identification (Boyer-Myrvold)\n- [x] Kameda preprocessing for O(1) reachability\n- [x] MCP tools (extract, partition, reachability, hierarchy, find)\n\n### Phase 3: Multi-Framework Orchestration ✅\n- [x] Unified mutation framework interface\n- [x] cosmic-ray parser\n- [x] poodle parser\n- [x] universalmutator parser\n\n### Phase 4: Belief Revision Engine ✅\n- [x] py-brs library integration (AGM core)\n- [x] Evidence adapter (mutation results → beliefs)\n- [x] Theory manager for curate-ipsum\n- [x] AGM contraction (py-brs v2.0.0 released)\n- [x] Entrenchment calculation (py-brs v2.0.0)\n- [x] Provenance DAG storage and queries\n- [x] Failure mode analyzer\n- [x] Rollback mechanism\n\n### Phase 5: Synthesis Loop ✅\n- [x] CEGIS implementation with LLM seeding\n- [x] Genetic algorithm with AST-aware crossover\n- [x] Entropy monitoring and diversity injection\n- [x] Counterexample-directed mutation\n- [x] CEGAR budget escalation (10s → 30s → 120s)\n\n### Phase 6: Verification Backends ✅\n- [x] Z3 integration for SMT solving (default backend)\n- [x] angr Docker symbolic execution (expensive tier)\n- [x] CEGAR orchestrator with budget escalation\n- [x] Verification harness builder (C source generation)\n- [x] Mock backend for testing\n- [ ] Alternative solvers (CVC5, Boolector)\n- [ ] SymPy path condition encoding\n\n### Phase 7: Graph Persistence ✅\n- [x] Abstract GraphStore ABC\n- [x] SQLite graph store (primary)\n- [x] Kuzu graph store (optional)\n- [x] Synthesis result persistence\n- [x] Kameda & Fiedler persistence\n- [x] Incremental update engine\n\n### Phase 8: RAG / Semantic Search ✅\n- [x] ChromaDB vector store integration\n- [x] sentence-transformers embedding provider (all-MiniLM-L6-v2)\n- [x] Graph-expanded RAG pipeline (vector top-k → neighbor expansion → rerank)\n- [x] Decay scoring for temporal relevance\n- [x] CEGIS integration for context-aware synthesis\n\n### Phase 9: Production Hardening ✅\n- [x] CI/CD (GitHub Actions — lint, test matrix, integration, lockfile)\n- [x] Release pipeline (tag push → PyPI + GHCR + MCP registry)\n- [x] uv lockfile (149 packages)\n- [x] pre-commit hooks (ruff format + lint + lock check)\n- [x] MCP bundle packaging (server.json, smithery.yaml, manifest.json)\n- [ ] HTML/SARIF reporting\n- [ ] IDE extensions (VSCode)\n- [ ] Regression detection and alerting\n\n## Future Work\n\n### Advanced Orchestration (Deferred)\n- [ ] Implicit region detection (spectral anomalies)\n- [ ] Non-contradictory framework assignment\n- [ ] Cross-framework survival analysis\n\n### Semantic Search & RAG\n- [x] Code Graph RAG for semantic search\n- [x] Semantic search index (ChromaDB)\n- [x] RAG retrieval pipeline with graph expansion\n- [ ] Text-to-Cypher queries\n\n## Quick Start\n\n```bash\n# Clone and install (dev)\ngit clone https://github.com/egoughnour/curate-ipsum.git\ncd curate-ipsum\nuv sync --extra dev --extra verify --extra rag --extra graph --extra synthesis\n\n# Run the MCP server\nuv run curate-ipsum\n\n# Or run tests\nmake test                     # fast suite (no Docker/model needed)\nmake test-all                 # including integration tests\n```\n\n## Configuration\n\nAll configuration is via environment variables (see `.env.example`):\n\n```bash\nCURATE_IPSUM_GRAPH_BACKEND=sqlite   # or kuzu\nMUTATION_TOOL_DATA_DIR=.mutation_tool_data\nMUTATION_TOOL_LOG_LEVEL=INFO\nCHROMA_HOST=                         # empty = in-process, or localhost:8000\nEMBEDDING_MODEL=all-MiniLM-L6-v2\n```\n\nFor the full service stack (ChromaDB + angr runner):\n\n```bash\nmake docker-up-verify         # starts Chroma + angr via Docker Compose\n```\n\n## Documentation\n\n### Planning & Design\n- [Phase 2 Plan](./PHASE2_PLAN.md) - **Active**: Graph-spectral infrastructure (9 steps)\n- [Progress](./PROGRESS.md) - Current status, what's done, what's next\n- [Decisions](./DECISIONS.md) - Architectural decisions with reasoning (D-001 through D-008)\n- [M1 Multi-Framework Plan](./m1_multi_framework_plan.md) - Region model & parser design (done)\n- [BRS Integration Plan](./brs_integration_plan.md) - Belief revision integration\n- [BRS v2 Refactoring Plan](./brs_v2_refactoring_plan.md) - Modular architecture\n- [ROADMAP](./ROADMAP.md) - Full milestone tracker\n\n### Architecture\n- [Architectural Vision](./architectural_vision.md) - Graph-spectral framework\n- [Synthesis Framework](./synthesis_framework.md) - CEGIS/CEGAR/genetic approach\n- [Belief Revision](./belief_revision_framework.md) - AGM theory and provenance\n\n### Reference\n- [Summary](./summary.md) - Functionality catalog\n- [Potential Directions](./potential_directions.md) - Enhancement roadmap\n- [Synergies](./synergies.md) - Tool ecosystem integration\n- [CONTEXT](./CONTEXT.md) - Session context for AI assistants\n- [DOCS_INDEX](./DOCS_INDEX.md) - Documentation quick reference\n\n## Key References\n\n- Alchourrón, Gärdenfors, Makinson (1985). *On the Logic of Theory Change*\n- Fiedler (1973). *Algebraic Connectivity of Graphs*\n- Kameda (1975). *On the Vector Representation of Reachability in Planar Directed Graphs*\n- Solar-Lezama (2008). *Program Synthesis by Sketching* (CEGIS)\n- Clarke et al. (2000). *Counterexample-Guided Abstraction Refinement* (CEGAR)\n\n## License\n\nMIT License - see [LICENSE](./LICENSE)\n\n---\n\n",
  "bytes": 14774,
  "sha": "86b278b7f65c0a1cf45d2ea8992d97595d6df3cba5f0610840b3870fd7e1d345",
  "repo_slug": "egoughnour/curate-ipsum",
  "fonte": "repo",
  "truncated": false,
  "api": "https://agentalog.com/api/listings/mcp_io_github_egoughnour_curate_ipsum_9dfe36d1/readme"
}