vvuq-mcp 2.0.1

Verification, Validation & Uncertainty Quantification MCP for marketplace contracts

VVUQ-MCP: Verification, Validation & Uncertainty Quantification

MCP Server for automated marketplace contract verification

Overview

VVUQ-MCP is a FastMCP server that acts as an automated judge for marketplace contracts. It verifies formal proofs (starting with Lean4), validates contract fulfillment, and executes cryptographic payments.

Features

• Tiered Dependency Management - Dynamic workspace provisioning with deterministic caching
• Server-Side Context Injection - Secure injection of versioned assumption contexts (e.g. Physics:v1.0.0)
• Lean4 Proof Verification - Compile and verify proofs against contract claims
• Cryptographic Payments - Secure payment settlement with audit trail
• Neo4j Integration - Contract storage and query
• MCP Protocol - Standard interface for AI agents

Quick Start

# Setup
python -m venv .venv
source .venv/bin/activate
pip install vvuq-mcp
# Or for development: pip install -e ".[dev]"

# Run MCP server
# Automatically manages its own workspaces directory
python -m vvuq_mcp.server

# Run tests
pytest tests/ -v

Architecture

See VVUQ_MCP_ARCHITECTURE.md (in mcp-marketplace repo) for complete architecture documentation.

Core components:

• server.py - FastMCP server with 4 core tools
• workspaces/ - Tiered Dependency Manager (Refactored v2.0)
  • path_generator.py - Deterministic SHA256 path generation
  • provisioner.py - Dynamic lakefile generation and mathlib downloading
• verifiers/lean4.py - Lean4 compilation and verification with context injection
• payments/ledger.py - Simple cryptographic ledger
• storage/neo4j_client.py - Async Neo4j integration

MCP Tools

verify_lean4_proof

Verify a Lean4 proof against a contract claim.

Input:

{
  "contract_id": "lean4-uuid-123",
  "claim_id": 1,
  "proof_code": "theorem my_theorem : ... := by ...",
  "dependencies": ["Mathlib.Data.Nat.Basic"],
  "mathlib_version": "v4.15.0",           # Optional: Pin specific version
  "assumption_contexts": ["Physics:v1.0.0"] # Optional: Inject specific context
}

Output:

{
  "verdict": "ACCEPTED",  # or REJECTED/ERROR
  "matches_claim": true,
  "payment_executed": {...},
  "verification_time_ms": 4823
}

submit_contract_proof

Submit a proof file for verification (convenience wrapper).

get_contract_requirements

Retrieve contract requirements for a specific contract.

query_verification_history

Query past verification attempts and outcomes.

Development

TDD Workflow

# 1. Write test FIRST (RED)
pytest tests/unit/test_lean4_verifier.py::test_new_feature -v

# 2. Implement (GREEN)
# Edit src/vvuq_mcp/verifiers/lean4.py

# 3. Verify
pytest tests/unit/test_lean4_verifier.py::test_new_feature -v

# 4. Refactor

Running Tests

# All tests
pytest tests/ -v

# Unit tests only (fast)
pytest tests/unit/ -v

# Integration tests (require Neo4j)
pytest tests/integration/ -v

# E2E Tests (Real filesystem/network)
pytest tests/e2e/ -v --slow

# With coverage
pytest tests/ -v --cov=vvuq_mcp --cov-report=term-missing

Configuration

Create .env file:

NEO4J_URI=bolt://localhost:7687
NEO4J_USER=neo4j
NEO4J_PASSWORD=your_password

# Optional customizations
# WORKSPACES_DIR=./workspaces (default: ~/.vvuq/workspaces)
# MAX_CONCURRENT_PROVISIONS=3
# MAX_TOTAL_WORKSPACES=50

PAYMENT_SECRET_KEY=<generate with: python -c "import secrets; print(secrets.token_hex(32))">
PAYMENT_LEDGER_MODE=simple

Security (Hardened v2.0)

• Command Injection Prevention - Strict regex validation (^[a-f0-9]{40}$ or ^v\d+...) for version inputs.
• Path Traversal Prevention - pathlib sandboxing and regex validation for context injection.
• Sandboxed Execution - Lean4 compilation in isolated, hashed directories.
• Resource Limits - Semaphore-based concurrency limits (MAX_CONCURRENT_PROVISIONS).
• Integrity Checks - Lockfiles (.vvuq_contexts) verify workspace consistency.

Status

Phase: Production (v2.0.0) Progress: 100% (Tiered Dependency Management & Security Hardening Complete) Next: Continuous Maintenance

License

MIT

Contact

Dirk Englund - [e-mail]