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 — and, for VALID verdicts, 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=sk_live_...

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": "sk_live_..."
      }
    }
  }
}

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.