How do I use prova-mcp?

1. Click on "Install Server". 2. Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state. 3. In the chat, type @ followed by the MCP server name and your instructions, e.g., "@prova-mcp verify this reasoning: 'A implies B, A, therefore B.'" That's it! The server will respond to your query, and you can continue using it as needed. Here is a step-by-step guide with screenshots.

prova-mcp

by insinuateai

Overview Schema Related Servers Score Discussions

Python

Hybrid

prova-mcp

PyPI Python License: MIT Docs

Let any AI agent verify its own reasoning before answering — and kernel-check the proof on its own machine.

prova-mcp is a Model Context Protocol server that exposes the Prova reasoning verifier as tools any MCP client can call. Drop it into Claude Code, Cursor, Windsurf, Zed, or ChatGPT desktop and the host model gains a self-verification loop:

The agent drafts a multi-step argument.
It calls verify_reasoning on the draft. Prova returns a verdict (VALID / INVALID), a confidence score, and — for INVALID — the exact step that's broken.
If VALID, the agent calls kernel_check_proof on the emitted Lean 4 proof. The local Lean kernel either accepts every step or rejects the proof. There is no third option, and Prova is not in that loop — it's purely a property of the proof and the kernel on your machine.

Result: agents that catch their own circular arguments, contradictions, and unsupported leaps before they reach a user — with a tamper-evident certificate as audit trail.

Tools

Tool	What it does
`verify_reasoning(reasoning, retain?, source_url?, domain?, metadata?)`	Verify a reasoning chain. Returns verdict, confidence, certificate URL, and (if invalid) the failing step.
`get_certificate(certificate_id)`	Look up an existing certificate by ID (e.g. `PRV-2026-A7X4`).
`download_lean_proof(certificate_id)`	Fetch the self-contained Lean 4 proof source for a `VALID` certificate.
`kernel_check_proof(lean_source)`	Run the local `lean` binary on a proof string. Exit 0 = accepted.
`verify_and_kernel_check(reasoning, ...)`	One-shot: verify, then locally kernel-check the emitted proof.

It also exposes each certificate as a resource at prova://certificate/{id} for clients that consume MCP resources.

Related MCP server: lean-lsp-mcp

Install

pip install prova-mcp

Optional but recommended — install Lean 4 so kernel_check_proof actually runs:

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

Configure

Set environment variables wherever your MCP client launches the server:

Variable	Default	Purpose
`PROVA_API_KEY`	(unset → demo tier)	API key from prova.cobound.dev. Demo is rate-limited.
`PROVA_API_BASE_URL`	`https://api.prova.cobound.dev`	Override for self-hosted Prova.
`PROVA_LEAN_BIN`	`lean`	Path to the Lean 4 executable.
`PROVA_DEFAULT_RETAIN`	`false`	Whether `verify_reasoning` defaults to persisting the original reasoning text.
`PROVA_MCP_LOG_LEVEL`	`WARNING`	Server log level.

Wire it up

Claude Code

claude mcp add prova prova-mcp -e PROVA_API_KEY=sk_live_...

Cursor / Windsurf / Zed / ChatGPT desktop

Add to your client's MCP config (typically mcp.json or claude_desktop_config.json):

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

A copy of this config is shipped at examples/claude_desktop_config.json.

How an agent uses it

A good system prompt nudge:

Before producing a multi-step argument, call prova.verify_reasoning on your draft. If the verdict is INVALID, repair the failing step and re-verify. If VALID, attach the certificate URL to your answer.

That single line turns Prova into a default reflex for the model — every reasoning answer ships with a verifiable certificate, and broken arguments are caught before the user ever sees them.

Why this exists

Verifiers are only useful if they sit where the reasoning happens. MCP is now the universal bridge between LLM clients and external tools — so shipping Prova as an MCP server makes formal reasoning verification the easiest thing to add to any agent stack on the planet. Install one package, set one key, get a tamper-evident proof of every important argument your agent makes.

Prova — the reasoning verifier itself; Lean 4 proofs, certificates, and the public API this server wraps.
insinuateai/prova-action — sibling GitHub Action (uses: insinuateai/prova-action@v1) that gates CI on reasoning validity.
Verify independently — kernel-check any Prova proof on your own machine in five minutes.

Changelog

0.1.0 — first release

5 tools: verify_reasoning, get_certificate, download_lean_proof, kernel_check_proof, verify_and_kernel_check.
Resource: prova://certificate/{id}.
Stdio transport; works with any MCP-compliant client.
Configurable via PROVA_API_KEY, PROVA_API_BASE_URL, PROVA_LEAN_BIN, PROVA_DEFAULT_RETAIN.

License

MIT. See LICENSE.

Available Tools

5 tools

download_lean_proofA

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

INVALID certificates do not have a proof — the call will return an error. The returned lean_source can be passed straight into kernel_check_proof to verify it on the local machine without trusting Prova.

Returns: {certificate_id, lean_source, byte_count}

ParametersJSON Schema

Name	Required	Description	Default
`certificate_id`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A3.9/5.0

Behavior3/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description must carry full burden. It discloses the error condition for invalid certificates and the return structure. However, it omits safety aspects (read-only implied but not stated) and does not detail behavior like idempotency or rate limits.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Very concise: two sentences and a return list. Front-loaded with purpose, no fluff. Every sentence adds value.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given one required parameter and an output schema described in text, the description covers return values and integration with kernel_check_proof. Lacks details on potential limitations (e.g., proof size), but is largely complete.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters2/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The parameter certificate_id has 0% schema coverage and the description does not explain what it is or how to obtain it. It only uses the term 'certificate' in context, which weakly implies the ID's role. This is insufficient.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Clearly states 'Download the self-contained Lean 4 proof for a VALID certificate', using a specific verb and resource. Distinguishes from siblings like kernel_check_proof (verification) and get_certificate (retrieval).

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Explicitly mentions that the returned lean_source can be passed to kernel_check_proof, suggesting a usage flow. Also warns that INVALID certificates result in an error. Lacks explicit exclusion of alternatives like verifying locally without downloading.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

get_certificateA

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

Returns the same compact summary as verify_reasoning. Use this to re-check a verdict, share a link, or inspect a failure that someone else's pipeline produced.

ParametersJSON Schema

Name	Required	Description	Default
`certificate_id`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A4.5/5.0

Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations provided, the description carries the full burden. It indicates a read-only fetch operation and mentions that the return format matches verify_reasoning, which adds behavioral context. It does not disclose authentication or error conditions, but for a simple retrieval tool, this is adequate.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is two concise sentences in the first paragraph and a brief second paragraph. It front-loads the purpose and uses no superfluous words. Every sentence earns its place.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the tool's simplicity (one parameter), the presence of an output schema (so return values are defined elsewhere), and the clear references to sibling tools, the description provides sufficient context for an agent to understand when and how to use it.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The input schema has 0% description coverage and only a parameter name 'certificate_id'. The description adds value by providing an example format ('PRV-2026-A7X4') and clarifying that it is a certificate ID, which goes beyond what the schema offers.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the verb ('Fetch'), the resource ('previously issued certificate'), and the unique identifier ('by ID'). It provides an example format ('PRV-2026-A7X4') and distinguishes the tool from siblings like verify_reasoning by specifying its use case for re-checking, sharing, or inspecting failures from other pipelines.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explicitly suggests when to use this tool (re-check a verdict, share a link, inspect a failure) and implicitly contrasts it with verify_reasoning by saying it returns the same summary. It does not explicitly state when not to use it, but the context is clear enough for an agent to decide.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

kernel_check_proofA

Run the Lean 4 kernel on a proof string locally.

This is the trust-anchor: Prova's verdict is only as strong as its server, but lean on the local machine is independent. Exit code 0 means the kernel accepted every step of the proof. Anything else means the proof is wrong and the certificate must not be trusted.

Requires the lean binary on PATH (override with PROVA_LEAN_BIN). Install via elan: https://github.com/leanprover/elan

Returns: {accepted, exit_code, stdout, stderr, lean_binary, lean_version}

ParametersJSON Schema

Name	Required	Description	Default
`lean_source`	Yes

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A4.7/5.0

Behavior5/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations provided, the description fully discloses behavior: it runs locally, exit code 0 means accepted, else proof is wrong, requires lean binary, and overridable via environment variable. It also describes the return format including fields like accepted, exit_code, etc.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is concise and well-structured: purpose first, then trust significance, exit code meaning, prerequisites, and return format. Every sentence adds value without redundancy.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness5/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The tool has one parameter and an output schema. The description covers prerequisites, error handling (non-zero exit), return fields, and even an environment variable override. It is fully complete for a tool of this complexity.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters4/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The single parameter lean_source has 0% schema description coverage, but its name and title are self-explanatory. The description mentions 'proof string' in the first line, giving context. A direct parameter description would improve clarity, but it is still adequate.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool 'Run the Lean 4 kernel on a proof string locally', specifying the verb, resource, and scope. It distinguishes from siblings like download_lean_proof (download) and verify_reasoning (other verification) by emphasizing it is the trust anchor and runs locally.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description explains the exit code meaning and the requirement for the lean binary, including installation via elan. While it doesn't explicitly contrast with siblings, the context of being the trust anchor implies when to use this tool for final kernel verification.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

verify_and_kernel_checkA

Verify reasoning, then locally kernel-check the emitted Lean proof.

The complete trust loop in one call. If the verdict is VALID, the Lean proof is downloaded and handed to the local Lean kernel; the result tells you whether the proof is mathematically sound on your own machine, not Prova's. INVALID verdicts skip the kernel step and return the failure.

Returns: {certificate, kernel_check} — kernel_check is null when verdict != VALID or no proof was emitted.

ParametersJSON Schema

Name	Required	Description	Default
`reasoning`	Yes
`retain`	No
`source_url`	No
`domain`	No

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A3.6/5.0

Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations provided. Description explains that the Lean proof is downloaded and run locally, and kernel_check is null for non-VALID verdicts. Discloses that result is on user's machine, not Prova's. Does not mention side effects but reasonable for a verification tool.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Description is front-loaded with main action and uses clear structure. Bullet points for return values are helpful. Slightly verbose but still efficient. Could be more concise without losing clarity.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness2/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given 4 parameters with 0% schema coverage and no param descriptions, the description is incomplete. It covers behavioral output well but leaves parameter semantics entirely unaddressed, which is critical for correct invocation.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters1/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 0%. Description provides no information about parameters (reasoning, retain, source_url, domain). Agent cannot infer their meaning or constraints beyond schema types.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Description clearly states 'Verify reasoning, then locally kernel-check the emitted Lean proof.' and distinguishes from siblings by combining both steps in one call. Specific verb (verify, kernel-check) and resource (reasoning, Lean proof).

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Description says 'The complete trust loop in one call.' implying when to use. It explains that INVALID verdicts skip kernel step but does not explicitly mention when not to use or alternatives. Usage context is clear but lacks exclusions.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

verify_reasoningA

Verify a multi-step reasoning chain and return a Prova certificate summary.

Use this on any draft chain-of-thought before producing a final answer. A VALID verdict means the argument is structurally sound (no circularity, no contradiction, no unsupported leap). An INVALID verdict tells you exactly which step is broken in the failure field — repair that step and re-verify.

Args: reasoning: The reasoning chain as plain text (numbered steps or prose). retain: If True, the original reasoning text is persisted on the certificate row. Default follows PROVA_DEFAULT_RETAIN env var (False if unset). source_url: Optional URL of a paper or document this reasoning came from — surfaced on the certificate page. domain: Optional hint: medical | legal | financial | code | general. Improves failure-classification accuracy. metadata: Optional caller-defined key/value pairs (<=20 keys, <=8 KB) attached to the certificate.

Returns: Compact certificate summary including verdict, confidence_score, certificate_id, certificate_url, and (if INVALID) a failure block pinpointing the broken step.

ParametersJSON Schema

Name	Required	Description	Default
`reasoning`	Yes
`retain`	No
`source_url`	No
`domain`	No
`metadata`	No

Output Schema

ParametersJSON Schema

Name	Required	Description
No output parameters

TDQS

A4.5/5.0

Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations are provided, so the description carries the full burden. It discloses the return value (verdict, confidence_score, certificate_id, etc.) and explains the meaning of VALID/INVALID verdicts. It does not mention any side effects or state changes, but the tool appears read-only.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description is well-structured: purpose sentence, usage context, parameter list, and return summary. It is concise yet comprehensive, with no extraneous words.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

Given the 5 parameters, 1 required, and no annotations, the description adequately covers the tool's behavior and return values. It could mention prerequisites or error handling, but the output schema exists to supplement this.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters5/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The schema has 0% description coverage, but the description provides detailed explanations for each parameter: reasoning (plain text), retain (default from env var), source_url (optional), domain (hints for classification), and metadata (constraints on keys and size). This adds significant value beyond the schema.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool verifies a multi-step reasoning chain and returns a Prova certificate summary. It specifies the intended use case ('before producing a final answer') and the tool's distinct role compared to sibling tools that focus on formal proof verification.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description provides explicit guidance on when to use the tool ('on any draft chain-of-thought before producing a final answer') and what to do in case of an INVALID verdict (repair and re-verify). However, it does not explicitly mention alternatives or when not to use this tool.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Install Server

RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A4.3/5.0

Disambiguation5/5

Each tool has a clear and distinct purpose: downloading proofs, fetching certificates, kernel checking, verifying reasoning, and a combined verify-and-check. There is minimal overlap and descriptions clearly differentiate them.

Naming Consistency5/5

All tools use consistent snake_case naming with a verb_noun pattern (e.g., download_lean_proof, verify_reasoning). The naming is predictable and follows a clear convention.

Tool Count5/5

With five tools, the server is appropriately scoped for its purpose of reasoning verification and proof checking. Each tool serves a necessary function without being overly numerous or sparse.

Completeness5/5

The tool set covers the core workflow: verifying reasoning, retrieving certificates, downloading proofs, local kernel checking, and a combined operation. There are no obvious gaps for the intended use case.

Maintenance

ActivityInactive

ResponsivenessNo issues

Resources

GitHub Repository

Need Help?

Related Servers

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

prover
com.axiomatic-ai
Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.
Developer Tools Code Analysis Research & Data
2
microservices.sh
sh.microservices
MCP server for AI agents to plan, verify, and deploy Cloudflare-native apps.
Cloud Platforms Agent Orchestration Developer Tools
21
mcp-aichat
io.github.AceDataCloud
MCP server for AI dialogue using various LLM models via AceDataCloud
AI & Machine Learning
2
DevSpeak
io.github.juanjaragavi
Official DevSpeak MCP server — translate technical text into formal specs from any AI IDE or agent
Developer Tools AI & Machine Learning Documentation Access
2

Related MCP Servers

math-logic-mcp
Code Execution Education & Learning Tools
ismailkerimov
A
license
A
quality
D
maintenance
MCP server that gives small LLMs verified symbolic-math & logic tools.
Updated 6 months ago (2026-02-20 12:40 UTC)
6
1
Apache 2.0
lean-lsp-mcp
Code Analysis Code Execution Developer Tools
project-numina
A
license
B
quality
D
maintenance
MCP server for agentic interaction with the Lean theorem prover via LSP, providing tools for understanding, analyzing, and interacting with Lean projects.
Updated 6 months ago (2026-03-11 16:28 UTC)
21
21
MIT
Chiasmus
Code Analysis Developer Tools
yogthos
A
license
Not graded
quality
B
maintenance
MCP server that gives LLMs access to formal verification via Z3 and SWI-Prolog, plus tree-sitter-based source code analysis. Translates natural language problems into formal logic using a template-based pipeline, verifies results with mathematical certainty, and analyzes call graphs for reachability, dead code, and impact analysis.
Updated 2 months ago (2026-06-29 12:19 UTC)
79
210
Apache 2.0
Aristotle MCP Server
AI & Machine Learning Education & Learning Tools
septract
A
license
Not graded
quality
F
maintenance
An MCP server that wraps Aristotle's automated theorem prover for Lean 4, allowing AI assistants to fill in proofs, verify lemmas, and formalize natural language into Lean code.
Updated 6 months ago (2026-03-05 18:47 UTC)
13
MIT

Latest Blog Posts

Who's Calling? MCP Hosts Are an Identity Blind Spot (And the Spec Knows It)
By Om-Shree-0709 on July 25, 2026.
mcp
Agent Identity
OAuth 2.1
Your AI Chatbot Just Exposed Your CEO's Salary to an Intern
By Om-Shree-0709 on July 2, 2026.
Agent Identity
MCP Security
OAuth Delegation
Why MCP Servers Need Execution Sandboxing (And Why Your Current Stack Isn't Enough)
By Om-Shree-0709 on June 30, 2026.
Agentic Ai
Prompt Injection
WebAssembly

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/insinuateai/prova-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server