certified-mcp
Click on "Install 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-mcpprove 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
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-mcpRelated 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
Tool | What it does |
| Re-derives a manufacturing admission verdict from the certificate's own numbers; checks integrity; refuses a bundle that certifies nothing |
| 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.
The rest of the toolkit
One idea, six pieces: a recorded verdict is a claim to be checked, never an input to be trusted.
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. | |
21 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.
This server cannot be installed
Maintenance
Resources
Unclaimed servers have limited discoverability.
Looking for Admin?
If you are the server author, to access and configure the admin panel.
Latest Blog Posts
- Who's Calling? MCP Hosts Are an Identity Blind Spot (And the Spec Knows It)By Om-Shree-0709 on .mcpAgent IdentityOAuth 2.1
- Your AI Chatbot Just Exposed Your CEO's Salary to an InternBy Om-Shree-0709 on .Agent IdentityMCP SecurityOAuth Delegation
- Why MCP Servers Need Execution Sandboxing (And Why Your Current Stack Isn't Enough)By Om-Shree-0709 on .Agentic AiPrompt InjectionWebAssembly
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/nickharris808/certified-mcp'
If you have feedback or need assistance with the MCP directory API, please join our Discord server