certified-mcp

Give your agent something it cannot talk its way past.

An MCP server exposing certificate verification, equivalence proving, and pre-registration sealing as tools. An agent that edits a design, a proof, or a benchmark config has no way to check its own work — so it reports success. These tools return a verdict re-derived from the artifact, not asserted about it.

Install

Status: pre-release. Not yet on PyPI. Until then, install from a checkout:

pip install ./lcert-verify ./equiv-receipt ./prereg-seal ./cert-atlas ./certified-mcp

pip install certified-mcp

Related MCP server: Agent Identity MCP Server

30-second quickstart

Add to your MCP client config (Claude Desktop, Cursor, or any MCP host):

{
  "mcpServers": {
    "certified": { "command": "certified-mcp" }
  }
}

Then ask your agent something it would otherwise have to guess at:

"I refactored this adder. Prove it's still equivalent to the original."

prove_equivalence(inputs=["a","b"], circuit_a=[...], circuit_b=[...])
-> {"verdict": "EQUIVALENT", "receipt_verifies": true}

Or, when it isn't:

-> {"verdict": "COUNTEREXAMPLE", "counterexample": {"1": true, "2": false}}

The agent gets a concrete failing input, not "this appears correct."

Tools

Why an agent benefits specifically

Three failure modes this addresses directly:

1. Confident wrongness. An agent that refactors logic will say it preserved behaviour. prove_equivalence returns a counterexample input when it didn't.

2. Moving the goalposts. An agent tuning against a benchmark will quietly relax the threshold. seal_criteria before the run makes that detectable — including by the agent itself.

3. Trusting a proof it was handed. check_drat accepts proofs from any solver and re-checks every lemma, so a fabricated proof is caught rather than cited.

Everything here is local and read-only

No network. Nothing uploaded. No telemetry. Every tool either reads a file you name or computes over arguments you pass.

None of these tools can produce a manufacturing certificate — only check one. That asymmetry is deliberate and is enforced by a test. Checking is cheap and should be everywhere; producing a certificate worth checking requires the certification engine, which is a separate closed product.

Implementation

Standard library only, MCP stdio protocol, ~300 lines. You can read the whole server before deciding to run it — which, for something you are wiring into an agent with filesystem access, you should.

Licence

Apache-2.0.

Honest scope — what these tools prove, and what they do not

The rest of the toolkit

A recorded verdict is a claim to be checked, never an input to be trusted. Nine repositories are built on it.

The whole story, and the objections answered, live at certified-oss — start there if this is the first one you have opened.

Try it now, no install: 🔏 the verifier Space · Browse the forgeries: 📊 the atlas dataset

Where the free edition stops

Everything here checks. None of it produces a certificate that is physically meaningful — that needs sound enclosures over real process models, which is a separate commercial product. If you need certificates rather than a way to check them, that is the conversation to have.

Documentation

• PERFORMANCE.md — measured, including what was not optimised

• CONTRIBUTING.md — Contributing

Portfolio-wide: Tutorial · Concepts · FAQ · Architecture · API reference

Licence, citation, contributing

Apache-2.0 — see LICENSE. If you use this, please cite it: CITATION.cff.

The most valuable contribution is a forgery this project fails to catch — see CONTRIBUTING.md and the portfolio-wide guide.

A recorded verdict is a claim to be checked, never an input to be trusted.

certified-mcp is one of nine repositories built on that. The whole story, and the objections answered, live at certified-oss — start there if this is the first one you have opened.