Reference

ctx_proof

Input contract and parameters for ctx_proof.

Status by featureReviewed September 2026

MCP tool · Analysis tools

Call this tool through your MCP client. Its availability depends on your active configuration and profile.

This registry contract is separate from the SDK. For terminal commands, use the CLI reference.

Parameters

Generated from the registered input schema. “Required” reflects the schema; individual actions can impose additional requirements.

actionstringRequired

export

filenamestring

Optional output filename

formatstring

json|summary|both

max_evidenceinteger

Max tool receipts

max_ledger_filesinteger

Max ledger files

project_rootstring

Project root

writeboolean

Write to .lean-ctx/proofs/

Exact JSON schema

Inspect the complete input schema

{
  "properties": {
    "action": {
      "description": "export",
      "type": "string"
    },
    "filename": {
      "description": "Optional output filename",
      "type": "string"
    },
    "format": {
      "description": "json|summary|both",
      "type": "string"
    },
    "max_evidence": {
      "description": "Max tool receipts",
      "type": "integer"
    },
    "max_ledger_files": {
      "description": "Max ledger files",
      "type": "integer"
    },
    "project_root": {
      "description": "Project root",
      "type": "string"
    },
    "write": {
      "description": "Write to .lean-ctx/proofs/",
      "type": "boolean"
    }
  },
  "required": [
    "action"
  ],
  "type": "object"
}

Runtime description

The following is the tool's own agent-facing description, reproduced from the reviewed registry. It can contain implementation terminology; it does not expand the public stability commitment.

Read the agent-facing description

Export machine-readable ContextProofV1 (Verifier, SLO, Pipeline, Provenance).
WORKFLOW: call after completing a task to generate audit trail.
ANTIPATTERN: not for budget analysis — use ctx_radar/ctx_metrics instead.
action=export (only valid); format=json|summary|both; write=true|false;
max_evidence=max tool receipts (default 50). Writes to .lean-ctx/proofs/.

Sources & versions3 references Reviewed 18 Sept 2026

mcp_manifest.rsrust/src/core/mcp_manifest.rsReviewed checkout
registry.rsrust/src/server/registry.rsReviewed checkout
dynamic_tools.rsrust/src/server/dynamic_tools.rsReviewed checkout

Core checkout: 50fbff09c9
Installed runtime: 3.10.2
SDK release: 1.1.0

Separate baselines for source, CLI/configuration and SDK contracts. Review does not certify every platform or integration.

Versions & compatibility