certified-mcp
This MCP server exposes tools for verifying and explaining certificates, proofs, and seals, plus equivalence proving and verifier scoring—all local and read-only.
Verify manufacturing certificates (
verify_certificate) — re-derives a verdict (VERIFIED/REFUTED/VACUOUS/UNVERIFIED) from the bundle’s own numbers; requires an out-of-band fingerprint for trust; abstains otherwise.Explain certificate verdicts (
explain_certificate) — turns REFUTED/REJECT into a per-locus breakdown of margins and shortfalls.Verify logic-equivalence receipts (
verify_receipt) — re-runs DRAT proof or counterexample simulation over the committed formula.Prove circuit equivalence (
prove_equivalence) — proves two small combinational circuits equivalent or returns a counterexample input, with a re-checkable receipt.Check DRAT refutations (
check_drat) — validates any solver’s DRAT proof against a CNF, naming the first invalid lemma.Seal acceptance criteria (
seal_criteria) — commits to a spec before measuring, without revealing it.Check sealed criteria (
check_seal) — detects if a spec was changed after sealing.Score a verifier (
score_verifier) — evaluates a verifier command against the failure atlas, returning detection/precision/atlas_score and which forgeries got through.Explain defect classes (
explain_defect) — describes why a forgery looks valid and which check catches it.
Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type
@followed by the MCP server name and your instructions, e.g., "@certified-mcp prove equivalence of my two circuit designs"
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.
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
pip install "certified-mcp @ git+https://github.com/nickharris808/certified-mcp.git@main"Not on PyPI yet. The name certified-mcp is unregistered, so pip install certified-mcp installs nothing today — use the line above, which installs exactly the same code. When the package is published this note goes and the plain name works.
Its four dependencies are declared as git references, so that one line pulls them too.
Related MCP server: agent-gate
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
Tool | What it does |
| Re-derives a manufacturing admission verdict from the certificate's own numbers; checks integrity; refuses a bundle that certifies nothing |
| Turns a REFUTED/REJECT verdict into a specific list: which loci are safe, unsafe or straddling, the margin each had, the margin it needed, and how far short it fell. Computes nothing new — it re-presents the arithmetic the verdict already rests on |
| Re-runs a DRAT proof (or re-simulates a counterexample) over the committed formula |
| Proves two small combinational circuits equivalent, or returns a differing input |
| Checks a DRAT refutation from any solver; names the first lemma that doesn't follow |
| Seals acceptance criteria before measuring, without revealing them |
| Detects criteria changed after sealing |
| Scores a verifier against the failure atlas |
| Explains a defect class: why the forgery looks valid, and what catches it |
Why an agent benefits specifically
Three failure modes this addresses directly:
Confident wrongness. An agent that refactors logic will say it preserved behaviour.
prove_equivalencereturns a counterexample input when it didn't.Moving the goalposts. An agent tuning against a benchmark will quietly relax the threshold.
seal_criteriabefore the run makes that detectable — including by the agent itself.Trusting a proof it was handed.
check_drataccepts 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
Question | Answer |
Can an agent check a certificate, proof or seal with these? | Yes, all locally and read-only. |
Does | No. It means the tool abstained for want of a trust anchor. An agent must not report it as either pass or fail. |
Can any tool here produce a certificate? | No — enforced by a test. These are checkers. |
Does anything here validate physics? | Never. |
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.
Re-derive a manufacturing certificate's verdict. Stdlib only. | |
Prove two circuits equivalent, with a receipt anyone can re-check. | |
Seal acceptance criteria before you measure. | |
28 labelled forgeries and a metric no degenerate verifier can win. | |
The above, as tools your AI agent can call. | |
The verifier in a browser. Nothing uploaded. |
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.
Available Tools
9 toolscheck_dratA
Check a DRAT refutation against a CNF in DIMACS form. Accepts proofs from any solver. Returns whether every lemma is RUP and, on failure, the index and content of the first lemma that does not follow.
Inputs: cnf_path (required), drat_path (required).
check_sealA
Check that an acceptance specification still matches its seal. Detects criteria that were changed after sealing. Returns matched=false with the two digests if they diverge.
Inputs: spec (required), seal, seal_path.
explain_certificateA
Explain WHY a certificate reached its verdict, locus by locus: which loci are safe, unsafe or straddling, the margin each had, the margin it needed, and how far short it fell. Use this after verify_certificate returns REFUTED or a certificate records a REJECT — it turns an opaque refusal into a specific, actionable list. Computes nothing new; it re-presents the arithmetic the verdict already rests on.
Inputs: bundle_dir (required), limit.
explain_defectA
Explain a certificate defect class from the atlas taxonomy: why the forgery looks valid, and which check catches it. Call with no key to list every defect.
Inputs: key.
prove_equivalenceA
Prove two small combinational circuits equivalent, or return a counterexample input. Circuits are given as gate lists over named signals. Returns a receipt any third party can re-check. Small instances only — this is a demonstration prover, not a production one.
Inputs: inputs (required), circuit_a (required), circuit_b (required), out_path.
score_verifierA
Score a verifier command against the certificate failure atlas. Returns detection (forgeries rejected), precision (valid artifacts accepted), and atlas_score = the minimum of the two, plus exactly which forgeries got through.
Inputs: command (required), atlas_dir (required).
seal_criteriaA
Seal an acceptance specification BEFORE measuring, so it cannot be adjusted afterward. Returns a digest that commits to the criteria without revealing them. Call this before running an experiment, not after.
Inputs: spec (required), note, out_path.
verify_certificateA
Verify a manufacturing certificate bundle. Re-derives the admission verdict from the certificate's own numbers rather than reading it, and checks integrity. Returns a verdict: VERIFIED, REFUTED, VACUOUS, or UNVERIFIED. IMPORTANT: without an expected_sha256 (a fingerprint obtained OUT OF BAND, not from the bundle itself) the verdict is UNVERIFIED — the tool abstains, because internal consistency alone cannot rule out a forgery whose inputs and verdict were edited together. UNVERIFIED means 'cannot tell', NOT 'the certificate is bad'. Do not report it as either pass or fail.
Inputs: bundle_dir (required), allow_empty, expected_sha256, accept_without_anchor.
verify_receiptA
Verify a logic-equivalence receipt. Re-runs the DRAT proof check (or re-simulates the counterexample) over the committed formula, and recomputes the hash chain. The verdict is re-derived, never read from the receipt.
Inputs: receipt_path (required).
Tool Schema Changelog
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
Loading tool schema changelog…
TDQS
Scored across 9 tools
Most tools have distinct purposes, but the verify_* family (verify_certificate, verify_receipt) and check_drat all involve checking proofs, which could cause confusion. However, the descriptions clearly differentiate artifact types and workflows.
Tool names consistently follow a verb_noun pattern (e.g., verify_certificate, check_drat, explain_defect). No mixed conventions or vague verbs; every name conveys its action and target.
With 9 tools, the server is well-scoped for a certification/verification domain. Each tool serves a clear role, and the count is within the ideal 3-15 range.
The toolset covers the core verification lifecycle: proving, checking, verifying, explaining, and sealing. Minor gaps exist (e.g., no tool to create certificates or manage the atlas), but these are likely external to this server's purpose.
Maintenance
Related MCP Connectors
Tamper-evident proof creation and verification for AI agents via MCP, A2A, and REST.
MCP server for AI agents to plan, verify, and deploy Cloudflare-native apps.
MCP server for building and testing AI agents with multi-model experimentation and insights.
MCP server for secureFlows: token-free URL builders and integration-linting tools for AI agents.
Related MCP Servers
- AlicenseNot gradedqualityDmaintenanceAn MCP server that provides fact-checking capabilities and truth anchoring for AI agents using verified data sources.MIT
- AlicenseBqualityCmaintenanceAn MCP server that enforces fail-closed deterministic checks, independent refute-first review, and tamper-evident hash-chained receipts for AI agent outputs before claiming completion.43MIT
- AlicenseAqualityBmaintenanceMCP server for checking supply-chain trust before connecting to AI agents, frameworks, or MCP servers.871 npm1MIT
- AlicenseAqualityDmaintenanceMCP server that enables AI agents to verify each other's trust scores, register, submit reviews, and find trusted agents before transacting.420 npmMIT