rocq-piler (scidonia/rocq-piler) is an MCP server listed on the M8ven Trust Index. It scores 74 out of 100, grade C. It declares 18 tools. No publisher has claimed this listing.

Back to MCP Trust IndexM8ven
C
Caution
74/100

rocq-piler

MCP server that bridges LLMs with the Rocq (Coq) proof assistant via LSP, enabling interactive theorem proving with AI.

→ scidonia/rocq-piler· listed on glama

Caution. Specific findings reduced this grade. They are listed on the page. Grades reflect the full trust pyramid: code, verification depth, and reputation. New projects cap at C until adoption is earned.

How we verified

Code Verified⚡ Live Monitored: not connected

Verified is a snapshot. Live keeps it current, and builds your track record.

⚡ Connect GitHub → continuous verification on every pushwhy connect →

Who stands behind it

scidonia

Source: Glama

Is this your MCP?

Claim it to get a verified publisher badge, a free copy of our full audit findings, and direct contact for any high-priority issues we find. Or connect your repo for our deepest verification, Live Monitored: read-only, revoke anytime. What we access →

⚡ Connect GitHub for Live Monitored

Install from

Glamanot scored here

The grade above is for the source repository. Registries can serve a different version, so we mark the ones we were not able to read.

// key findings
⚠️
Known vulnerabilities in dependencies: 1 high
Affects packages this MCP installs at runtime. Upgrade or remove the affected dependency.
✅
No credential exfiltration, no sensitive file access, no obfuscation
Static analysis found nothing flowing your secrets to unexpected places.
✅
Open source with a license and README
Anyone can audit the code, the license is declared, and the publisher documents what it does.
// tools this server exposes18 tools

These names and descriptions are the publisher's own, read from the source code. We print them as written. Our assessment is the findings above, not this list.

insert_tactics
search_lemmas
inspect_term

Check the type of a term speculatively. Runs `Check <term>.` and returns the result.

inspect_about

Get information about a term/definition speculatively. Runs `About <term>.` and returns the result.

stratify
close_admits
check_file

Check the file and report errors with diagnostic messages. Each FAILED proof shows the Coq error message, line number, and goal state. Use mode to control output verbosity. If you get a timeout, retry with a larger timeout_ms (e.g. 120000).

require_lib
locate_term
focus_proof
reset_proof
add_lemma
add_block
delete_lemma
move_lemma
verdict
certify_witness
edit_file

Apply text edits to a file and re-sync with rocq-lsp. Replaces bash+coqc entirely — reports the first errors with goal states after every edit, so you always know if it compiled. Use for anything: single-tactic fixes, entire lemma proofs, or bulk edits replacing many admits at once. Use "find"/"repl…

// known CVEs in dependencies1 high

Disclosed vulnerabilities in this server's declared npm dependencies (via OSV). Whether each is reachable depends on the installed versions.

high@modelcontextprotocol/sdk@0.5.0GHSA-w48q-cv73-mx4w

Model Context Protocol (MCP) TypeScript SDK does not enable DNS rebinding protection by default

Depend on this server? Get alerted when its CVEs change.Watch this server free →
// environment variables
To run this server yourself, you supply these values. They go in your own MCP client configuration and stay on your machine. The secret label means the value is sensitive, not that the server mishandles it.
configROCQ_PILER_DEBUG_COQC
configROCQ_PILER_DISABLE_EDIT_FILE
configROCQ_PILER_POSITIONAL_ONLY
// quality suggestions

Tool annotations

No tools have read-only/destructive annotations

Add readOnlyHint or destructiveHint annotations to every tool so hosts can warn users before invoking.

All four hints declared on every tool

18/18 tools missing one or more hints — insert_tactics (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint); search_lemmas (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint); inspect_term (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint), +15 more. OpenAI's directory rejects tools where any of the four hints are missing or non-boolean.

For every tool, set all four hints (readOnlyHint, destructiveHint, idempotentHint, openWorldHint) to explicit true/false values that match the handler’s actual behaviour.

Tool test coverage

8/18 tools referenced in tests (44%)

Write tests that reference each tool by name so every tool has at least one test.

Shell command execution

3 child_process calls — runs shell commands

Prefer library functions over shell-outs. If you must shell out, ensure all inputs are properly escaped.

Production dependencies are patched

0 critical, 1 high severity in production deps — @modelcontextprotocol/sdk@0.5.0 (high)

Run npm audit fix, or upgrade the affected packages to a non-vulnerable version.

Claim the listing to review these findings one by one and send us a correction where you disagree, straight to the team. Claiming also means we tell you when the grade moves, and reach you first if we find anything urgent.

// full audit trail
The findings above are the summary. The full trail, every check we ran, each deduction, the network hosts observed and the dependency advisories, goes to verified publishers, along with an alert whenever a new one lands. Verified publishers can also review each finding and dispute it in one click. Publisher corrections have sharpened several of our checks this month, because the maintainer knows the codebase better than any scanner.
// improvement guidance — verified publishers only
We have 5 concrete improvements we can share with the publisher of this MCP. Each comes with specific guidance to raise the trust score.
// embed badge in your README
[![M8ven Verified](https://m8ven.ai/badge/mcp/scidonia/rocq-piler?variant=verified)](https://m8ven.ai/mcp/scidonia/rocq-piler)
Shows verification status without the grade. Want the grade badge instead? Remove ?variant=verified from the URL.
commit: 16497750d6275ae2050ea6e5f15f469463aaf018
code hash: 86d5b1f7ec4667ec5d766904584cf21b63d918e3404955e84e33e0ea29526809
view raw JSON →
Check MCPs from inside your assistant
Tool Check · MCP

Vetting this one by hand? Tool Check is an MCP that scores other MCPs. Add it once and ask Claude, ChatGPT, or any MCP client to grade a server, surface CVEs, check the publisher, and suggest safer alternatives — before you install.

https://m8ven.ai/api/mcp/tool-check
check_toolsearch_toolscompare_toolsrecommend_alternativescheck_publisherreport_concern
How to add it →Free · no account needed · works in any MCP client