agda-mcp

Server Quality Checklist

Profile completionA complete profile improves this server's visibility in search results.

Latest release: v0.3.0
Disambiguation5/5
Each tool targets a distinct aspect of Agda interaction: loading, typechecking, goal/context retrieval, constraints, proof actions (case split, refine, auto), expression/inference queries, and job management. Even similar-looking tools like agda_retrieve_context and agda_retrieve_contexts differ in singular vs batch semantics, and agda_retrieve_goals vs agda_query_metavariables distinguish visible vs all metavariables.
Naming Consistency5/5
All tools follow the uniform pattern agda_<verb>_<noun>, with clear verbs like load, typecheck, retrieve, refine, normalize, infer, query, and job actions (await, cancel, list). The naming is predictable and consistent, making it easy to guess tool purposes.
Tool Count4/5
18 tools is on the higher side (borderline heavy), but each tool maps to a necessary operation in the Agda proof assistant workflow. The count is justified by the breadth of features (module loading, typechecking, goal management, proof actions, metavariable queries, and async job handling) without redundant tools.
Completeness4/5
The toolset covers the core lifecycle of Agda development: loading/typechecking modules, inspecting goals/contexts/constraints, applying proof tactics (case split, refine, auto), normalizing/inferring expressions, and managing asynchronous jobs. Minor gaps include no explicit module list or workspace management, but the essential operations are present and no dead ends are apparent.
Average 3.5/5 across 18 of 18 tools scored. Lowest: 2.9/5.
See the Tool Scores section below for per-tool breakdowns.
- No community issues in the last 6 months
- 24 commits in the last 12 weeks
- Last stable release on August 7, 2026
- No critical vulnerability alerts
- No high-severity vulnerability alerts
- No code scanning findings
- CI is passing
This repository is licensed under MIT License.
This repository includes a README.md file.
No tool usage detected in the last 30 days. Usage tracking helps demonstrate server value.
Tip: use the "Try in Browser" feature on the server page to seed initial usage.
Add a glama.json file to provide metadata about your server.
If you are the author, simply .
If the server belongs to an organization, first add glama.json to the root of your repository:
```
{
  "$schema": "https://glama.ai/mcp/schemas/server.json",
  "maintainers": [
    "your-github-username"
  ]
}
```
Then . Browse examples.
Add related servers to improve discoverability.

How to sync the server with GitHub?

Servers are automatically synced at least once per day, but you can also sync manually at any time to instantly update the server profile.

To manually sync the server, click the "Sync Server" button in the MCP server admin interface.

How is the quality score calculated?

The overall quality score combines two components: Tool Definition Quality (70%) and Server Coherence (30%).

Tool Definition Quality measures how well each tool describes itself to AI agents. Every tool is scored 1–5 across six dimensions: Purpose Clarity (25%), Usage Guidelines (20%), Behavioral Transparency (20%), Parameter Semantics (15%), Conciseness & Structure (10%), and Contextual Completeness (10%). The server-level definition quality score is calculated as 60% mean TDQS + 40% minimum TDQS, so a single poorly described tool pulls the score down.

Server Coherence evaluates how well the tools work together as a set, scoring four dimensions equally: Disambiguation (can agents tell tools apart?), Naming Consistency, Tool Count Appropriateness, and Completeness (are there gaps in the tool surface?).

Tiers are derived from the overall score: A (≥3.5), B (≥3.0), C (≥2.0), D (≥1.0), F (<1.0). B and above is considered passing.

Tool Scores

Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It only labels the operation as 'Query' and mentions two categories of metavariables, but does not disclose return format, side effects, or whether the call blocks. The async parameter in the schema hints at blocking behavior, but the description does not address it.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single sentence, front-loaded with the key action and resource, and contains no fluff or repetition. It is appropriately concise for the information it conveys.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Despite having five parameters and no output schema, the description is only a short phrase. It does not explain what 'interaction-backend invisible' means, what the returned data looks like, or how this tool fits into the workflow. This is inadequate for a tool of this complexity.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all parameters and their meanings. The tool description adds no parameter detail, but the schema does the heavy lifting, making the baseline 3 appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose4/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses the specific verb 'Query' with the resource 'metavariables' and further qualifies 'visible and interaction-backend invisible', making the tool's scope clear. It does not explicitly contrast with sibling tools but the resource is distinct enough to avoid confusion.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives like agda_retrieve_goals or agda_retrieve_constraints. There are no exclusions or prerequisites mentioned beyond the required workspace parameter implied by the schema.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden of behavioral disclosure. It only says 'retrieve', implying a read operation, but gives no details about side effects, error conditions, asynchronous behavior, or the nature of the returned data. This is a significant gap for a 6-parameter tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler. Every word adds meaning and it is appropriately sized for stating the core purpose.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description is too terse for a tool with 6 parameters and no output schema. It does not explain the role of parameters like rewrite, async, or includeRaw, nor does it hint at the response format beyond 'type and local context'. Given the complexity, more context is needed for an agent to know how to compose calls correctly.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 83% (>80%), so the baseline is 3. The description itself does not explain any parameters, but the schema already documents most of them, so no additional compensation is needed.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose4/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb ('Retrieve') and specific resource ('type and local context for an opaque goal handle'). It is distinct from sibling tools like agda_retrieve_goals, but it does not explicitly differentiate itself, so it stops short of a 5.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided on when to use this tool vs alternatives. There is no mention of exclusions, prerequisites, or contexts where this tool is preferred. The description is purely definitional.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
There are no annotations, so the description must disclose behavioral traits itself. It indicates a read operation ('Retrieve') but omits whether the call may block, how async/deferAfterMs affect execution, whether a loaded workspace is required, and what the returned goals/handles structure looks like.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness4/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler words or redundant phrasing. It is concise and clear at a high level, though it sacrifices structured detail that would be useful for a complex tool.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the absence of annotations and output schema, this one-sentence description is insufficient. It does not explain job/async semantics, prerequisites, return values, or relationship to sibling tools, leaving an agent without enough context to use the tool reliably.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The input schema has 100% parameter coverage, with individual descriptions for workspace, async, timeoutMs, includeRaw, and deferAfterMs. The description adds no parameter-specific meaning, but the schema already carries the full burden, so a baseline score of 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose4/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb ('Retrieve') and identifies a precise resource ('current visible goals and opaque handles'). The phrase 'current visible' helps distinguish it from context/constraint retrieval siblings, though 'opaque handles' is not explained and no explicit contrast with agda_query_metavariables is given.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided about when to use this tool versus alternatives like agda_retrieve_contexts, agda_retrieve_constraints, or agda_query_metavariables. It simply states the action without any context, prerequisites, or exclusions.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It only states 'Retrieve constraints' without revealing whether the operation is read-only, whether it can block (despite async parameters), error behavior, or the nature of the returned data. This is insufficient for safe invocation.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness4/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence that directly states the core purpose. It is appropriately terse and every word contributes to conveying intent, though it sacrifices contextual depth for brevity.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a tool in the complex Agda domain, this description is under-specified. With no output schema and no annotations, an agent needs more context about what 'constraints' means, what constitutes an 'active module', and what the response contains. The schema covers parameters, but overall tool semantics are incomplete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100% with all five parameters documented individually, so the baseline is 3. The description adds no parameter-level detail beyond the schema, merely referencing the workspace indirectly. It does not enhance understanding of async, includeRaw, or deferAfterMs.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb ('Retrieve') and specifies a distinct resource ('constraints for the active module in a workspace'), clearly differentiating it from sibling tools like agda_retrieve_goals and agda_retrieve_context. It conveys exactly what the tool does.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool over alternatives, nor does it mention prerequisites such as loading a module first. It only states the action without contextual cues or exclusions.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
The description is minimally transparent, revealing only that the operation loads and typechecks. It does not disclose the asynchronous nature suggested by the async/deferAfterMs parameters and job-handle sibling tools, nor does it mention side effects, blocking behavior, or return value characteristics. With no annotations, the description carries the full behavioral burden but does not meet it.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler. It efficiently communicates the core action and resource, and every word contributes to the tool's meaning.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Despite rich schema parameter documentation, the description omits important operational context for a complex tool: async behavior, job-handle returns, and output shape. Since there is no output schema and no annotations, the agent cannot fully predict the tool's behavior from this description alone.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
All seven parameters are fully documented in the schema (100% coverage), so the description does not need to repeat parameter syntax or formats. It adds only the high-level context that modulePath refers to a file on disk, which the schema already conveys; this meets the baseline for schema-covered parameters.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb phrase ('Load and typecheck') and identifies the resource ('one top-level Agda module from disk'), making the tool's function immediately clear. It also implicitly distinguishes itself from sibling tools that focus on goals, contexts, or expressions.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to choose this tool over siblings like agda_typecheck or agda_retrieve_goals, nor does it state prerequisites or exclusions. It only states what the tool does, leaving usage decisions entirely to the agent.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It does not state whether the operation is read-only, whether it requires an active goal, what side effects may occur, or what the return value looks like. The one-sentence description is insufficient for a tool with no annotation safety profile.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single sentence that is concise and front-loaded. Every word contributes meaning: the action, the target, and the scoping. There is no wasted verbiage or repetition of schema details.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The tool has 8 parameters, no annotations, and no output schema, yet the description provides no information about return values, error conditions, ordering constraints, or the differences between workspace and goal-local scopes. This is a sparse description for a complex tool, leaving the agent with insufficient context to invoke it correctly.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 50%, leaving goal, mode, workspace, and expression undocumented. The description's mention of 'workspace or goal-local scope' adds partial meaning to the workspace and goal parameters, clarifying their role as scope selectors. However, it does not explain the 'mode' parameter or provide details on how the scopes interact with 'expression', so it only partially compensates for the coverage gap.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Normalize an expression') with a specific resource and scoping ('in workspace or goal-local scope'). The verb 'normalize' is unique among sibling tools (agda_infer_type, agda_typecheck, etc.), so it distinguishes this tool from alternatives.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided on when to use this tool versus alternatives. The description only states what the tool does, without any context about prerequisites, exclusions, or preferred use cases. The mention of workspace/goal-local scope is a hint but not explicit when-to-use guidance.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description must disclose side effects, return behavior, and other traits. It only says 'reload and typecheck' without mentioning that reloading may change Agda state, that the call can block or return a job handle, or what the output contains. This leaves critical behavioral aspects undocumented.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler. It is appropriately sized for a tool with a well-structured schema, and every word contributes to defining the tool's core purpose.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Despite full schema coverage, the tool has 7 parameters, no output schema, and no annotations. The one-sentence description is insufficient for an agent to understand the tool's place in the workflow, its return values, or side effects. It lacks behavioral context that would normally come from the description or annotations.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the baseline is 3. The description adds no extra parameter semantics beyond what the schema already provides. It does not clarify how parameters like async, diagnosticsOnly, or includeContexts affect the operation, but that is not required given the rich schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Reload and typecheck') and the resource ('active module in a workspace'), distinguishing it from siblings like agda_load_module or goal retrieval tools. The verb-resource pair is specific and unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
There is no guidance on when to use this tool versus alternatives. It does not mention that it should be called after editing a module or that it is the primary way to get type errors, nor does it exclude any contexts. A single sentence describing the action provides no usage context.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It only states the core action and does not mention asynchronous behavior, potential side effects, or prerequisites. This is insufficient for a tool with async parameters and no output schema.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, focused sentence with no filler. It front-loads the key action and scope, earning a perfect score.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the 8-parameter schema and the absence of an output schema or annotations, the description is too sparse. It fails to mention return behavior, error conditions, or the role of key parameters like goal and rewrite.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters2/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Half of the parameters (goal, rewrite, workspace, expression) lack schema descriptions. The description does not explain these or any other parameter meanings, leaving the agent to infer from names. It adds no semantic value beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb 'infer', the resource 'type of an expression', and the scope (workspace or goal-local). This distinguishes it from sibling tools like agda_typecheck or agda_normalize_expression.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines3/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description gives no explicit guidance on when to prefer this tool over siblings like agda_typecheck or agda_normalize_expression. The use case is implied by the name and description but not explicitly contrasted.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description must carry the full burden of behavioral disclosure. It does mention 'atomically apply and typecheck' which hints at transactional semantics, but it fails to disclose async behavior (async, deferAfterMs), job handles, error handling, or the guarded nature of writes beyond what the schema already says. The description adds minimal context over the schema.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single sentence, front-loaded with the action, and contains no filler or redundant phrases. Every word contributes to understanding the tool's primary purpose and key mode switch.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool has 8 parameters, no annotations, and no output schema, the description is too sparse. It does not explain typical workflows, expected results, or edge-case behavior. The schema covers parameter semantics, but the overall usage context remains incomplete, especially for an agent choosing among many similar Agda tools.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters4/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 88%, so most parameters are already well-documented. The description adds valuable context by clarifying that the default is preview mode and that apply:true switches to atomic apply-and-typecheck, which maps directly to the 'apply' parameter and enhances understanding of the tool's behavior.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly identifies the tool as Agda's refine operation, with two explicit modes: previewing a refinement or applying and typechecking it atomically with apply:true. This distinguishes it from sibling tools like agda_auto and agda_case_split by naming the specific action and its key parameter.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines2/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use refine versus alternatives like agda_auto, agda_case_split, or agda_normalize_expression. It lacks any prerequisites, exclusions, or typical invocation scenarios, leaving the agent to infer usage from the name alone.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the transparency burden. It only describes the basic retrieval action and omits important behaviors like async/job-handle semantics, timeout overrides, rewrite modes, and return format. This leaves the agent uncertain about side effects and execution behavior.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler or redundant details. It efficiently communicates the core purpose.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Despite high schema coverage, there is no output schema and no annotations. The description does not mention return shape, async blocking behavior, or how contexts are presented. Given the complexity of parameters like async, rewrite, and deferAfterMs, the one-sentence description is insufficient for confident invocation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The schema descriptions cover 83% of parameters, including goals, async, timeoutMs, and includeRaw. The tool description adds little beyond the schema, mostly repeating 'several goal handles' already in the goals parameter description. It does not clarify less-documented parameters like rewrite.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb ('Retrieve') and a clear resource ('types and local contexts for several goal handles'). The phrase 'in one round trip' highlights the batch nature and distinguishes it from the singular sibling agda_retrieve_context.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines3/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
There is no explicit when-to-use or alternative guidance, but 'for several goal handles in one round trip' implies it is the batch version of agda_retrieve_context. Sibling names reinforce this, but the description itself does not name alternatives or exclusions.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior2/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It only states that the tool reports information; it does not disclose whether the operation is read-only, whether it can block or return a job handle, what the response format is, or any side effects. This is minimal for a tool with 4 parameters and no output schema.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, well-structured sentence that is concise and to the point. Every word contributes to the meaning, with no fluff or repetition. It is appropriately sized for the tool's purpose.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness3/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description lists the kinds of information returned (installation, compatibility, workspaces), providing a reasonable overview. However, given the absence of an output schema and annotations, it does not explain the output structure, potential job-handle behavior, or the effect of parameters like includeRaw. The description is adequate but could be more complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so all four parameters (async, timeoutMs, includeRaw, deferAfterMs) are fully documented in the schema. The description adds no parameter information, but the schema already provides complete semantics, so the baseline of 3 applies.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb 'Report' and names the resource: Agda installation, compatibility, and active workspaces. This clearly differentiates it from sibling tools that load modules, typecheck, or retrieve goals, making the tool's purpose unambiguous.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines3/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
Usage is implied by the tool's name and description: use it when you need server/installation information. However, there is no explicit 'when to use' vs alternatives, no examples, and no exclusions, so the guidance remains implicit rather than explicit.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior3/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full responsibility for behavioral disclosure. It does disclose that apply:true atomically applies and typechecks, and that applying is a guarded write. However, it does not explain what happens after preview (return value), side effects on the buffer/file, or fallback behavior if typecheck fails. It provides some transparency but leaves significant gaps.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single sentence that is concise, front-loaded with the action, and free of filler. It communicates the two modes efficiently without redundancy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness2/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
This is a complex tool with 7 parameters, two modes, and no output schema. The description explains only the core purpose and apply behavior, but omits important context such as return formats (preview output, job handles), how async/defer behavior affects the call, and what happens when apply:true fails. The absence of an output schema makes this omission more impactful. The description is inadequate for the tool's complexity.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all seven parameters. The description adds no extra parameter-level detail beyond noting the apply:true behavior, which is already covered in the schema. Thus the baseline of 3 stands.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly identifies the tool as performing a case split operation with two modes: preview and apply-and-typecheck. It uses a specific verb ('Preview'/'apply') and resource ('case split'), and is distinct from sibling tools like refine or auto, which handle different operations.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines4/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides clear context for when to use this tool: to preview a case split or to apply and typecheck it with apply:true. It doesn't explicitly mention when not to use it or compare to alternatives, but the mode distinction implicitly guides usage. This is clear context without exclusions, so a 4 is appropriate.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior3/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It does disclose the destructive action ('Abort') and the resource release side effect, which is helpful. However, it does not describe behavior for invalid or non-pending job IDs, nor what the response looks like after cancellation.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler. Every word carries meaning: the action, the target, and the consequence. It is appropriately concise for a simple tool.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness4/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a one-parameter cancellation tool, the description adequately covers purpose and effect. It lacks details on error handling or edge cases (e.g., canceling a completed job), but given the simplicity of the tool and the rich parameter schema, it is nearly complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The input schema already fully describes the 'job' parameter as 'Job id returned by a pending tool result' (100% coverage). The description reinforces the requirement that the job must be pending but does not add new semantic information beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb 'Abort' and clearly identifies the resource ('pending Agda job') plus a unique side effect ('release its Agda command slot'). It is immediately distinguishable from sibling job management tools like agda_job_await, agda_job_status, and agda_job_list.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines3/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies the tool is for canceling pending jobs, but it does not explicitly state when to use it versus alternatives like agda_job_await. There are no exclusions or alternative tool references, leaving usage context implicit rather than explicit.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior3/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full burden. It discloses that the tool is non-blocking ('without waiting') and reports state, but it doesn't describe possible state values, error behavior for invalid/completed jobs, or return format. This leaves significant unknowns for the agent.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, well-structured sentence that front-loads the core action and includes a key differentiator. Every word earns its place with no redundancy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness3/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The tool is simple with one parameter and no output schema, so the description doesn't need to be extensive. However, it doesn't explain what the 'state' includes or how the result is returned, leaving the agent uncertain about interpreting the tool's output. It's adequate but with clear gaps.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The only parameter 'job' is fully described in the schema as 'Job id returned by a pending tool result', giving 100% schema coverage. The description adds no extra parameter detail, but the baseline of 3 is appropriate since the schema already explains the parameter's source and meaning.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb 'report' and the resource 'state of a pending Agda job', and the phrase 'without waiting' distinguishes it from sibling tools like agda_job_await. This makes the tool's purpose immediately obvious.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines4/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies when to use this tool (to check status instead of blocking) and contrasts with waiting via the phrase 'without waiting for it'. It doesn't explicitly name alternatives, but the sibling context (await/cancel/list) makes the intended usage clear.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior3/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden for behavioral transparency. It discloses the key waiting behavior and the fact that it returns 'pending' if still running. However, this information is largely a paraphrase of the schema's waitMs description ('Milliseconds to wait for completion before returning pending again'). It adds little beyond the schema, and does not mention side effects, error handling, or whether the job is consumed after collection.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, well-structured sentence that front-loads the main action and then clarifies the waiting behavior with a semicolon. Every word earns its place; there is no redundancy or filler.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness4/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The tool is simple with two parameters and no output schema. The description covers the essential contract: collect the result of a pending job, wait up to waitMs, and return pending if still running. It doesn't describe the success return format or any error conditions, but for a straightforward await operation, the description is sufficiently complete. A 5 would require more detail about return values or edge cases.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the parameters 'job' and 'waitMs' are already well-documented. The description's mention of 'waiting up to waitMs' essentially restates the schema, adding no new semantic meaning. Baseline for high schema coverage is 3, and this description does not exceed it.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb ('Collect the result') and identifies the resource ('a pending Agda job'), clearly distinguishing from sibling tools like agda_job_status (which likely just checks status) and agda_job_await_any (which awaits any job). The phrase 'waiting up to waitMs' and 'returns pending again if still running' further clarifies the tool's specific role.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines4/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description clearly implies when to use this tool: when you have a job ID from a pending tool result and want to collect its result. It does not explicitly mention alternatives or exclusions, but the context is clear enough. No mention of when-not-to-use or alternative tools, so it doesn't reach a 5.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior4/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden. It discloses that the tool is a preview by default and performs an atomic apply+typecheck when apply:true is set, which is key safety-relevant behavior. It does not cover failure modes or return values, but it does add meaningful context beyond the schema.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
One sentence with no filler. It front-loads the primary action, uses 'atomically' to pack meaning, and every word earns its place.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness4/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given a rich schema with full parameter documentation and no output schema, the description adequately covers the core purpose and the two key modes. It omits async behavior and return values, but those are documented or implied by the schema, so the description is reasonably complete for an agent to select and invoke the tool.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so baseline is 3. The description reinforces the role of apply:true but adds no new semantics beyond what the schema already describes. It neither compensates nor detracts from the parameter documentation.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool previews Agda proof search and optionally applies and typechecks it when apply:true is set. This specific verb+resource combination distinguishes it from siblings like agda_refine and agda_case_split by focusing on proof search and the atomic apply behavior.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines4/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage context: use this tool for proof search, and set apply:true to apply the result. It clearly communicates the two modes of operation (preview vs. apply) but does not explicitly name alternatives or exclusion criteria, so it lacks the 'when not to use' clarity.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior4/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the burden of disclosing behavior. It clearly reveals the key trait: the tool returns as soon as the first of several pending jobs finishes, not waiting for all. It also implies non-blocking behavior via waitMs in the schema. However, it does not describe return format or timeout specifics, but those are partially covered by parameter descriptions.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single sentence that is front-loaded with the core action ('Wait for the FIRST of several pending jobs to finish') and immediately provides practical context ('use after fanning work out across workspaces'). Every word earns its place with no fluff.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness4/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The tool is simple, has no output schema, and the parameters are fully described in the schema. The description covers the essential behavior and usage context, but does not explicitly state what happens when waitMs expires or what the return value looks like. However, given the schema clarity and simplicity of the operation, the combination is reasonably complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters3/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so both parameters (jobs and waitMs) are already well-documented. The description adds the conceptual framing of a 'race' and the fan-out context, but that is more about usage than parameter meaning. No additional parameter-level detail beyond the schema is provided, so baseline 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific action: wait for the FIRST of several pending jobs to finish. This distinguishes it from sibling agda_job_await (which likely waits for a specific job) by emphasizing the race semantics and the 'several' vs. 'one' distinction.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines4/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description gives an explicit usage context: 'use after fanning work out across workspaces.' This tells the agent when this tool is appropriate, implying a multi-job parallel scenario. It does not explicitly list exclusions or alternatives, but the sibling names (agda_job_await) make the contrast clear enough.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Behavior3/5
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
There are no annotations, so the description carries the full transparency burden. It discloses an important behavioral filter ('still running or awaiting collection') but does not state whether the call is read-only, what the returned job representation looks like, or whether listing consumes/removes jobs. This is minimal but not misleading.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Conciseness5/5
Is the description appropriately sized, front-loaded, and free of redundancy?
One short, front-loaded sentence with no redundant words. Every word contributes meaning, and the structure is immediately scannable.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Completeness4/5
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a zero-parameter list operation, the description is complete enough: it identifies the resource and filter condition. It does not explain the output format, but the verb 'List' implies a list of jobs, and the lack of an output schema keeps expectations simple. A minor gap is the absence of explicit detail about what is returned.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Parameters4/5
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool has zero parameters, so the input schema imposes no burden. The baseline for no-parameter tools is 4, and the description does not need to explain parameter semantics that do not exist.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Purpose5/5
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses the specific verb 'List' with resource 'Agda jobs' and a clear state qualifier ('still running or awaiting collection'). This makes the tool's purpose immediately obvious and helps distinguish it from sibling tools like agda_job_status (single job status) and agda_job_cancel (mutating operation).
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Usage Guidelines4/5
Does the description explain when to use this tool, when not to, or what alternatives exist?
The state qualifier clearly sets expectations: this tool is for discovering active or uncollected jobs, not all jobs or historical results. It does not explicitly name alternatives like agda_job_status for individual job checks, but the context is clear enough for an agent to infer the appropriate use case.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

GitHub Badge

Glama performs regular codebase and documentation scans to:

Confirm that the MCP server is working as expected.
Confirm that there are no obvious security issues.
Evaluate tool definition quality.

Our badge communicates server capabilities, safety, and installation instructions.

Card Badge

Copy to your README.md:

[![agda-mcp MCP server](https://glama.ai/mcp/servers/peterthiemann/agda-mcp/badges/card.svg)](https://glama.ai/mcp/servers/peterthiemann/agda-mcp)

Score Badge

Copy to your README.md:

[![agda-mcp MCP server](https://glama.ai/mcp/servers/peterthiemann/agda-mcp/badges/score.svg)](https://glama.ai/mcp/servers/peterthiemann/agda-mcp)

Latest Blog Posts

Who's Calling? MCP Hosts Are an Identity Blind Spot (And the Spec Knows It)
By Om-Shree-0709 on July 25, 2026.
mcp
Agent Identity
OAuth 2.1
Your AI Chatbot Just Exposed Your CEO's Salary to an Intern
By Om-Shree-0709 on July 2, 2026.
Agent Identity
MCP Security
OAuth Delegation
Why MCP Servers Need Execution Sandboxing (And Why Your Current Stack Isn't Enough)
By Om-Shree-0709 on June 30, 2026.
Agentic Ai
Prompt Injection
WebAssembly

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/peterthiemann/agda-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server