# Formal Verification & Topological Deficit — Full Reference
# Betti number computation, topological deficit analysis, fold verification, DAG structural analysis, and pipeline invariant checking.

## Server
- Name: verification-mcp
- Version: 1.0.0
- MCP Protocol: 2024-11-05
- Endpoint: https://verification.forkjoin.ai/mcp
- Paper: "Being Irreversible" by Taylor William Buley
- LEDGER sections: Foundation: Fork/Race/Fold Axioms, Covering Space & Topological Deficit
- Paper result: Result 1: Computational Topology

## Tools

### measure_betti
Compute the first Betti number (beta_1) of a directed acyclic graph. beta_1 = edges - nodes + connected_components. A beta_1 of 0 means the graph is a forest (tree per component). Positive beta_1 indicates independent cycles that represent topological redundancy or wasted structure. Derived from "Being Irreversible" Section 6.

Input schema:
```json
{
  "type": "object",
  "properties": {
    "nodes": {
      "type": "array",
      "items": {
        "type": "string"
      },
      "description": "List of node identifiers in the DAG (e.g., [\"a\", \"b\", \"c\", \"d\"])"
    },
    "edges": {
      "type": "array",
      "items": {
        "type": "array",
        "items": {
          "type": "string"
        },
        "minItems": 2,
        "maxItems": 2
      },
      "description": "List of directed edges as [source, target] pairs (e.g., [[\"a\",\"b\"], [\"a\",\"c\"], [\"b\",\"d\"], [\"c\",\"d\"]])"
    }
  },
  "required": [
    "nodes",
    "edges"
  ]
}
```

### topological_deficit
Compute the topological deficit between a system's actual first Betti number and the problem's natural (minimal) Betti number. Delta_beta = beta_1_star - beta_1. A zero deficit means the topology is efficient. A positive deficit means structural waste. Returns the estimated Landauer heat cost: Delta_beta * kT * ln(2). Derived from "Being Irreversible" Result 1.

Input schema:
```json
{
  "type": "object",
  "properties": {
    "beta_1": {
      "type": "number",
      "description": "The system's current first Betti number (actual topology)"
    },
    "beta_1_star": {
      "type": "number",
      "description": "The problem's natural (minimal) first Betti number (ideal topology)"
    },
    "temperature_kelvin": {
      "type": "number",
      "description": "Temperature in Kelvin for Landauer cost calculation (default: 300 K, room temperature)"
    }
  },
  "required": [
    "beta_1",
    "beta_1_star"
  ]
}
```

### verify_fold
Verify a fold operation against the paper's axioms. A fold merges N inputs into one output, erasing N-1 distinguishable paths. Checks conservation (nothing created or destroyed), irreversibility (information is erased and cannot be recovered), and computes the number of vented paths. Derived from "Being Irreversible" Section 6.

Input schema:
```json
{
  "type": "object",
  "properties": {
    "inputs": {
      "type": "array",
      "items": {
        "type": "string"
      },
      "description": "Labels for the input paths being folded (e.g., [\"result_a\", \"result_b\", \"result_c\"])"
    },
    "output": {
      "type": "string",
      "description": "Label for the single output produced by the fold (e.g., \"merged_result\")"
    },
    "preserves_value": {
      "type": "boolean",
      "description": "Whether the fold preserves the aggregate value of its inputs (e.g., sum, consensus). Default: true."
    }
  },
  "required": [
    "inputs",
    "output"
  ]
}
```

### dag_analysis
Analyze a directed acyclic graph for fork/race/fold/vent structure as defined in "Being Irreversible". Identifies fork points (out-degree > 1, where computation splits), fold points (in-degree > 1, where paths merge irreversibly), sources, sinks, and classifies the overall topology (linear, diamond, fan-out, fan-in, complex).

Input schema:
```json
{
  "type": "object",
  "properties": {
    "nodes": {
      "type": "array",
      "items": {
        "type": "string"
      },
      "description": "List of node identifiers in the DAG"
    },
    "edges": {
      "type": "array",
      "items": {
        "type": "array",
        "items": {
          "type": "string"
        },
        "minItems": 2,
        "maxItems": 2
      },
      "description": "List of directed edges as [source, target] pairs"
    }
  },
  "required": [
    "nodes",
    "edges"
  ]
}
```

### pipeline_invariants
Check a pipeline description against the invariants from "Being Irreversible": (1) beta_1 >= 0 (topological non-negativity), (2) vents <= folds (you cannot vent more information than you fold), (3) eventual termination (all paths reach a sink). Returns pass/fail for each invariant with explanations.

Input schema:
```json
{
  "type": "object",
  "properties": {
    "nodes": {
      "type": "array",
      "items": {
        "type": "string"
      },
      "description": "List of node identifiers in the pipeline DAG"
    },
    "edges": {
      "type": "array",
      "items": {
        "type": "array",
        "items": {
          "type": "string"
        },
        "minItems": 2,
        "maxItems": 2
      },
      "description": "List of directed edges as [source, target] pairs"
    },
    "declared_vents": {
      "type": "number",
      "description": "Number of declared vent operations in the pipeline (paths explicitly discarded)"
    }
  },
  "required": [
    "nodes",
    "edges"
  ]
}
```


## Discovery Endpoints
- /llms.txt — This file
- /llms-full.txt — Full reference (you are here)
- /skills — Skill definitions
- /agents.json — Agent manifest
- /.well-known/mcp.json — MCP discovery
- /.well-known/agent-card.json — Agent card
- /.well-known/openapi.json — OpenAPI spec
- /.well-known/security.txt — Security contact

## Integration
Connect via any MCP-compatible client (Claude, ChatGPT, Cursor, etc.)
POST https://verification.forkjoin.ai/mcp with JSON-RPC 2.0 body.

## Parent
Part of the ForkJoin MCP server family at https://forkjoin.ai
Superserver: https://mcp.forkjoin.ai