Agda Mcp — independently scanned and version-tracked by SaferSkills.
SaferSkills independently audited Agda Mcp (Agent Skill) and scored it 100/100 (green). The audit ran 55 deterministic rules across Security, Supply Chain, Maintenance, Transparency, and Community; it found 0 high-severity and 0 lower-severity findings. The full rule-by-rule trace and per-finding evidence are below. Free, methodology-open.
Findings & checks · 0 flagged
Every scanned point with the score it earned and what moved between them.
First recorded scan — no prior version to compare against.
The primary manifest — the file an agent reads to learn what this artifact does.
MCP server for Agda, providing type checking, go-to-definition, case splitting, auto proof search, and more — directly from Claude Code or any MCP client.
Talks to agda --interaction-json (the same interface powering agda-mode in Emacs/VS Code), so it has access to all of Agda's interactive features without needing agda-language-server.
git clone https://github.com/DreamLinuxer/agda-mcp.git
cd agda-mcp
uv syncClaude Code (globally, for all projects):
claude mcp add --scope user agda-lsp -- uv run --directory /path/to/agda-mcp agda-mcpOther MCP clients — add to your client's MCP config:
{
"mcpServers": {
"agda-lsp": {
"command": "uv",
"args": ["run", "--directory", "/path/to/agda-mcp", "agda-mcp"],
"type": "stdio"
}
}
}Replace /path/to/agda-mcp with the absolute path where you cloned the repo.
| Tool | Description |
|---|---|
agda_load | Load/type-check a file, get goals + errors + warnings |
agda_hover | Symbol kind + definition site at a position |
agda_definition | Go to definition (file:line:col) |
| Tool | Description |
|---|---|
agda_give | Fill a hole with a complete solution |
agda_elaborate_give | Fill a hole with an elaborated solution |
agda_refine | Refine a goal (may create new subgoals) |
agda_intro | Introduce a constructor or lambda |
agda_refine_or_intro | Auto-choose between refine and intro |
agda_case_split | Case split on a variable in a goal |
agda_auto | Try to automatically solve a goal |
agda_solve_one | Solve a goal if determined by unification |
| Tool | Description |
|---|---|
agda_goal_info | Get the type and context of a goal |
agda_goal_type | Get just the type of a goal |
agda_context | Get the context (bindings) at a goal |
agda_goal_type_context_infer | Goal type + context + inferred type of expr |
agda_goal_type_context_check | Goal type + context + check expr against type |
agda_infer_in_goal | Infer type of an expression at a goal |
agda_compute_in_goal | Normalize an expression at a goal |
agda_helper_function | Generate helper function type for a goal |
agda_why_in_scope_goal | Explain where a name comes from (at a goal) |
agda_module_contents_goal | List module contents (at a goal) |
| Tool | Description |
|---|---|
agda_infer | Infer the type of an expression |
agda_compute | Normalize/evaluate an expression |
agda_why_in_scope | Explain where a name comes from |
agda_constraints | Show all unsolved constraints |
agda_metas | Show all open goals/meta-variables |
agda_search_about | Search for definitions mentioning given names |
agda_module_contents | List names exported by a module |
agda_solve_all | Solve all goals determined by unification |
agda_auto_all | Try to automatically solve all goals |
agda_load("/path/to/file.agda")
→ Checked. No errors, warnings, or goals.agda_infer("/path/to/file.agda", "map")
→ {a b : Set} {n : ℕ} → (a → b) → Vec a n → Vec b nagda_compute("/path/to/file.agda", "2 + 3")
→ 5agda_case_split("/path/to/file.agda", 0, "xs")
→ f [] = ?
f (x ∷ xs) = ?agda_auto("/path/to/file.agda", 0)
→ a , bThe server spawns a single persistent agda --interaction-json process and communicates via the IOTCM protocol over stdio. File state (highlighting data for go-to-definition, goal types, diagnostics) is cached per file and refreshed on each agda_load call.
~30 seconds. Free. No account. Every finding cites a rule and a line of evidence.