Integrations · MCP

MCP server: verify reasoning from inside any agent

prova-mcp exposes the Prova reasoning verifier as a Model Context Protocol server. Drop it into Claude Code, Cursor, Windsurf, Zed, or ChatGPT desktop and the host model can verify its own draft reasoning before producing an answer. For VALID verdicts, it can kernel-check the emitted Lean 4 proof on the local machine without depending on Prova's servers.

What you get

  • Self-verification loop. Agents catch their own circular arguments, contradictions, and unsupported leaps before users ever see them.
  • Local trust anchor. kernel_check_proof runs the local lean binary on the emitted proof. The kernel accepts or rejects every step. Prova is not in that loop.
  • Certificate URLs in every answer. One line of system prompt makes the model attach Verified: <url> to anything it reasons about.

1. Install

terminalbash
# Install the server
pip install prova-mcp

# Wire it into Claude Code
claude mcp add prova prova-mcp -e PROVA_API_KEY=prv_...

Optional but recommended. Install Lean 4 so kernel_check_proof actually runs:

elan installerbash
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

2. Wire it into any MCP client

Most clients (Cursor, Windsurf, Zed, ChatGPT desktop, Claude desktop) read MCP servers from a JSON config. Drop in:

mcp configjson
{
  "mcpServers": {
    "prova": {
      "command": "prova-mcp",
      "env": {
        "PROVA_API_KEY": "prv_..."
      }
    }
  }
}

For Claude Code, the one-liner above takes care of it.

3. Tools the agent gains

verify_reasoning(reasoning, retain?, source_url?, domain?, metadata?)

Verify a multi-step argument. Returns verdict, confidence, certificate URL, and (if INVALID) the failing step.

get_certificate(certificate_id)

Fetch a previously issued certificate by ID, e.g. PRV-2026-A7X4.

download_lean_proof(certificate_id)

Download the self-contained Lean 4 proof for a VALID certificate.

kernel_check_proof(lean_source)

Run the local lean binary on a proof. Exit code 0 means accepted. Prova is not in this loop.

verify_and_kernel_check(reasoning, ...)

One shot: verify the reasoning, then kernel-check the emitted proof locally. The complete trust loop in one tool call.

Each certificate is also exposed as a resource at prova://certificate/{id} for clients that consume MCP resources directly.

4. Make verification the default reflex

Append this to the host model's system prompt. One paragraph turns Prova into a built-in habit:

system prompt addendumtext
You have access to the prova MCP server. For any answer that depends on
a multi-step reasoning chain, you MUST:

  1. Draft your reasoning as a numbered list.
  2. Call prova.verify_and_kernel_check on the draft.
  3. If the verdict is INVALID, read the failure field, repair the broken
     step, and re-verify. Do not show the user the broken draft.
  4. If the verdict is VALID and the kernel accepted the proof, append
     "Verified: <certificate_url>" to your answer.

5. Configuration

  • PROVA_API_KEY. API key from your dashboard. Unset = demo tier (rate-limited).
  • PROVA_API_BASE_URL. Override for self-hosted Prova. Default https://api.prova.cobound.dev.
  • PROVA_LEAN_BIN. Path to the Lean 4 executable. Default lean.
  • PROVA_DEFAULT_RETAIN. Whether verify_reasoning persists the original reasoning text. Default false.

Source & bug reports

github.com/insinuateai/prova-mcp (MIT-licensed).

Have a different MCP client and it doesn't work? Open an issue or ping us.