Curate-Ipsum

Curate-Ipsum

A graph-spectral MCP server for verified code synthesis through belief revision

[PyPI] [MCP Registry] [Claude Desktop] [License: MIT] [Python]

[Top Language] [Code Size] [Last Commit] [Repo Size]

Curate-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.

Install

# PyPIpip install curate-ipsum
# or with uvuv pip install curate-ipsum
# Docker (includes baked-in embedding model)docker pull ghcr.io/egoughnour/curate-ipsum:latest

Claude Desktop / MCP Client

Add to your claude_desktop_config.json:

{  "mcpServers": {    "curate-ipsum": {      "command": "uvx",      "args": ["curate-ipsum"]    }  }}

Or with Docker (embedding model pre-loaded, no Python needed):

{  "mcpServers": {    "curate-ipsum": {      "command": "docker",      "args": ["run", "-i", "--rm", "ghcr.io/egoughnour/curate-ipsum:latest"]    }  }}

MCP Tools

Curate-Ipsum exposes 30 tools over the MCP stdio transport, organised into six groups:

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

Belief Revision — add_assertion, contract_assertion, revise_theory, get_entrenchment, list_assertions, get_theory_snapshot, store_evidence, get_provenance, why_believe, belief_stability

Rollback & Failure — rollback_to, undo_last_operations, analyze_failure, list_world_history

Graph-Spectral — extract_call_graph, compute_partitioning, query_reachability, get_hierarchy, find_function_partition, incremental_update, persistent_graph_stats, graph_query

Verification — verify_property (Z3/angr), verify_with_orchestrator (CEGAR budget escalation), list_verification_backends

Synthesis & RAG — synthesize_patch (CEGIS + genetic + LLM), synthesis_status, cancel_synthesis, list_synthesis_runs, rag_index_nodes, rag_search, rag_stats

Current Status

Last Updated: 2026-02-08

The Problem

LLMs produce code that is:

• ✅ Syntactically valid (usually)
• ✅ Statistically plausible
• ❌ Semantically correct (sometimes)
• ❌ Type-safe (by accident)
• ❌ Formally verified (never)

Current approaches either trust LLM output blindly or reject it entirely. Neither is optimal.

The Solution

Use LLMs for cheap candidate generation, then invest computational resources to achieve formal guarantees:

LLM Candidates (k samples)        ↓   Seed Population        ↓┌───────────────────────────┐│  CEGIS + CEGAR + Genetic  │  ← Verification loop│  + Belief Revision        │└───────────────────────────┘        ↓  Strongly Typed Patch  (with proof certificate)

Key Differentiators from State of the Art

vs. Traditional Mutation Testing (Stryker, mutmut, cosmic-ray)

vs. LLM Code Generation (Copilot, Claude, GPT)

vs. Program Synthesis (Sketch, Rosette, SyGuS)

vs. Symbolic Execution (KLEE, S2E)

Novel Contributions

1. Graph-Spectral Code Decomposition

   • Fiedler vector partitioning for optimal reachability
   • Hierarchical SCC condensation
   • Planar subgraph identification → O(1) Kameda queries
   • Kuratowski subgraphs as atomic non-planar units

2. Belief Revision for Synthesis

   • AGM-compliant theory revision
   • Entrenchment ordering for minimal contraction
   • Provenance DAG for failure mode analysis
   • Rollback sharpens validity (failures refine the universal model)

3. Implicit Region Detection

   • Spectral anomalies reveal undertested code
   • Cross-framework mutation resistance identifies critical regions
   • Historical mutability guides partition optimization

4. Mathematical Constraint Reformulation

   • Boolean-intractable → differential/root-finding
   • SymPy path condition encoding
   • Hybrid SMT + numerical solving

Architecture

flowchart TB    subgraph MCP["MCP Interface"]        direction TB
        subgraph Sources["Analysis Sources"]            direction LR            MUT["🧬 Mutation<br/>Orchestrator<br/><small>Stryker<br/>mutmut<br/>cosmic-ray</small>"]            SYM["🔬 Symbolic<br/>Execution<br/><small>KLEE · Z3<br/>SymPy</small>"]            GRAPH["📊 Graph<br/>Analysis<br/><small>Joern<br/>Neo4j<br/>Fiedler</small>"]        end
        MUT --> BRE        SYM --> BRE        GRAPH --> BRE
        BRE["🧠 Belief Revision Engine<br/><small>AGM Theory · Entrenchment · Provenance DAG</small>"]
        BRE --> SYNTH
        SYNTH["⚙️ Synthesis Loop<br/><small>CEGIS · CEGAR · Genetic Algorithm</small>"]
        SYNTH --> |"counterexample"| BRE
        SYNTH --> OUTPUT
        OUTPUT["✅ Strongly Typed Patch<br/><small>Proof Certificate ·Type Signature<br/>Pre/Post Conditions</small>"]    end
    LLM["🤖 LLM Candidates<br/><small>top-k samples</small>"] --> SYNTH
    style MCP fill:#1a1a2e,stroke:#16213e,color:#eee    style Sources fill:#16213e,stroke:#0f3460,color:#eee    style MUT fill:#0f3460,stroke:#e94560,color:#eee    style SYM fill:#0f3460,stroke:#e94560,color:#eee    style GRAPH fill:#0f3460,stroke:#e94560,color:#eee    style BRE fill:#533483,stroke:#e94560,color:#eee    style SYNTH fill:#e94560,stroke:#ff6b6b,color:#fff    style OUTPUT fill:#06d6a0,stroke:#118ab2,color:#000    style LLM fill:#ffd166,stroke:#ef476f,color:#000

Roadmap

Phase 1: Foundation ✅

• MCP server infrastructure
• Stryker report parsing
• Run history and PID metrics
• Flexible region model (hierarchical: file → class → function → lines)
• mutmut parser integration
• Framework auto-detection
• Unified parser interface

Phase 2: Graph Infrastructure ✅

• Graph models (CodeGraph, Node, Edge)
• Call graph extraction (AST-based)
• ASR extractor (import/class analysis)
• Dependency graph extraction (module-level imports)
• Laplacian construction from call/dependency graphs
• Fiedler vector computation (scipy.sparse.linalg)
• Recursive Fiedler partitioning with virtual sink/source
• SCC detection and hierarchical condensation
• Planar subgraph identification (Boyer-Myrvold)
• Kameda preprocessing for O(1) reachability
• MCP tools (extract, partition, reachability, hierarchy, find)

Phase 3: Multi-Framework Orchestration ✅

• Unified mutation framework interface
• cosmic-ray parser
• poodle parser
• universalmutator parser

Phase 4: Belief Revision Engine ✅

• py-brs library integration (AGM core)
• Evidence adapter (mutation results → beliefs)
• Theory manager for curate-ipsum
• AGM contraction (py-brs v2.0.0 released)
• Entrenchment calculation (py-brs v2.0.0)
• Provenance DAG storage and queries
• Failure mode analyzer
• Rollback mechanism

Phase 5: Synthesis Loop ✅

• CEGIS implementation with LLM seeding
• Genetic algorithm with AST-aware crossover
• Entropy monitoring and diversity injection
• Counterexample-directed mutation
• CEGAR budget escalation (10s → 30s → 120s)

Phase 6: Verification Backends ✅

• Z3 integration for SMT solving (default backend)
• angr Docker symbolic execution (expensive tier)
• CEGAR orchestrator with budget escalation
• Verification harness builder (C source generation)
• Mock backend for testing
• Alternative solvers (CVC5, Boolector)
• SymPy path condition encoding

Phase 7: Graph Persistence ✅

• Abstract GraphStore ABC
• SQLite graph store (primary)
• Kuzu graph store (optional)
• Synthesis result persistence
• Kameda & Fiedler persistence
• Incremental update engine

Phase 8: RAG / Semantic Search ✅

• ChromaDB vector store integration
• sentence-transformers embedding provider (all-MiniLM-L6-v2)
• Graph-expanded RAG pipeline (vector top-k → neighbor expansion → rerank)
• Decay scoring for temporal relevance
• CEGIS integration for context-aware synthesis

Phase 9: Production Hardening ✅

• CI/CD (GitHub Actions — lint, test matrix, integration, lockfile)
• Release pipeline (tag push → PyPI + GHCR + MCP registry)
• uv lockfile (149 packages)
• pre-commit hooks (ruff format + lint + lock check)
• MCP bundle packaging (server.json, smithery.yaml, manifest.json)
• HTML/SARIF reporting
• IDE extensions (VSCode)
• Regression detection and alerting

Future Work

Advanced Orchestration (Deferred)

• Implicit region detection (spectral anomalies)
• Non-contradictory framework assignment
• Cross-framework survival analysis

Semantic Search & RAG

• Code Graph RAG for semantic search
• Semantic search index (ChromaDB)
• RAG retrieval pipeline with graph expansion
• Text-to-Cypher queries

Quick Start

# Clone and install (dev)git clone https://github.com/egoughnour/curate-ipsum.gitcd curate-ipsumuv sync --extra dev --extra verify --extra rag --extra graph --extra synthesis
# Run the MCP serveruv run curate-ipsum
# Or run testsmake test                     # fast suite (no Docker/model needed)make test-all                 # including integration tests

Configuration

All configuration is via environment variables (see .env.example):

CURATE_IPSUM_GRAPH_BACKEND=sqlite   # or kuzuMUTATION_TOOL_DATA_DIR=.mutation_tool_dataMUTATION_TOOL_LOG_LEVEL=INFOCHROMA_HOST=                         # empty = in-process, or localhost:8000EMBEDDING_MODEL=all-MiniLM-L6-v2

For the full service stack (ChromaDB + angr runner):

make docker-up-verify         # starts Chroma + angr via Docker Compose

Documentation

Planning & Design

• Phase 2 Plan - Active: Graph-spectral infrastructure (9 steps)
• Progress - Current status, what's done, what's next
• Decisions - Architectural decisions with reasoning (D-001 through D-008)
• M1 Multi-Framework Plan - Region model & parser design (done)
• BRS Integration Plan - Belief revision integration
• BRS v2 Refactoring Plan - Modular architecture
• ROADMAP - Full milestone tracker

Architecture

• Architectural Vision - Graph-spectral framework
• Synthesis Framework - CEGIS/CEGAR/genetic approach
• Belief Revision - AGM theory and provenance

Reference

• Summary - Functionality catalog
• Potential Directions - Enhancement roadmap
• Synergies - Tool ecosystem integration
• CONTEXT - Session context for AI assistants
• DOCS_INDEX - Documentation quick reference

Key References

• Alchourrón, Gärdenfors, Makinson (1985). On the Logic of Theory Change
• Fiedler (1973). Algebraic Connectivity of Graphs
• Kameda (1975). On the Vector Representation of Reachability in Planar Directed Graphs
• Solar-Lezama (2008). Program Synthesis by Sketching (CEGIS)
• Clarke et al. (2000). Counterexample-Guided Abstraction Refinement (CEGAR)

License

MIT License - see LICENSE