Curate-Ipsum

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

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

# PyPI
pip install curate-ipsum

# or with uv
uv 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