Curate-Ipsum

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

1. 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)

1. Implicit Region Detection

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

1. 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 Orchestrator Stryker mutmut cosmic-ray "] SYM["🔬 Symbolic Execution KLEE · Z3 SymPy "] GRAPH["📊 Graph Analysis Joern Neo4j Fiedler "] end

MUT --> BRE SYM --> BRE GRAPH --> BRE

BRE["🧠 Belief Revision Engine AGM Theory · Entrenchment · Provenance DAG "]

BRE --> SYNTH

SYNTH["⚙️ Synthesis Loop CEGIS · CEGAR · Genetic Algorithm "]

SYNTH --> |"counterexample"| BRE

SYNTH --> OUTPUT

OUTPUT["✅ Strongly Typed Patch Proof Certificate ·Type Signature Pre/Post Conditions "] end

LLM["🤖 LLM Candidates top-k samples "] --> 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 (spe