What can you do with this server?

This server provides an MCP interface for interactive theorem proving and program verification with Agda, supporting module loading, typechecking, goal inspection, code transformations, expression evaluation, and asynchronous job management. * Session & Workspace Management: Load and typecheck .agda, .lagda, .lagda.md files; manage multiple independent Agda sessions with dynamic workspace selection. * Goal Inspection: Retrieve current goals, inspect types and local contexts (single or batched), list constraints, and query metavariables. * Code Transformations: Preview or atomically apply case splits, refinements, and proof-search (auto) with SHA-256 fingerprint verification to prevent race conditions. * Expression Tools: Normalize expressions and infer types in top-level or goal-local scopes. * Asynchronous Operations: Long-running tasks return job handles; await, check status, cancel, or list jobs for non-blocking interaction. * Configuration & Robustness: Highly configurable via environment variables and per-call overrides (timeout, async mode, apply policy, etc.); includes rollback on failed application, output truncation reporting, and server info introspection.

How do I use agda-mcp?

1. Click on "Install Server". 2. Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state. 3. In the chat, type @ followed by the MCP server name and your instructions, e.g., "@agda-mcp type check src/Main.agda" 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.

agda-mcp

by peterthiemann

Overview Schema Related Servers Score Discussions

TypeScript

Local

agda-mcp

agda-mcp is a standalone MCP server for Agda's JSON interaction protocol. It keeps one long-lived agda --interaction-json process per active workspace and supports on-disk .agda, .lagda, and .lagda.md modules.

The server exposes normalized, transport-independent results while retaining bounded metadata about Agda's native responses in a raw field. Native events are available on request. Case split, refine, and auto are non-mutating by default. An explicit apply: true, or starting the server with --apply-edits, atomically writes the guarded proposal and typechecks it in the same operation.

End-to-end example

Suppose /workspace/Example.agda contains:

module Example where

data Bool : Set where
  true  : Bool
  false : Bool

not : Bool → Bool
not x = ?

An agent can take the file from one hole to two case-specific holes as follows. Responses below are abbreviated to their normalized data; opaque handles and the source fingerprint must be reused exactly as returned. This example assumes the server was started with --dynamic-workspaces, allowing the first call to select /workspace without per-project server configuration.

# 1. Load and typecheck the top-level module.
agda_load_module({
  "modulePath": "/workspace/Example.agda",
  "workspaceRoot": "/workspace",
  "includeRaw": false
})
→ data.workspace = "workspace_…"

# 2. Retrieve the current goals (the load response includes them too).
agda_retrieve_goals({
  "workspace": "workspace_…",
  "includeRaw": false
})
→ data.goals[0] = { "handle": "goal_…", "type": "Bool", … }

# 3. Inspect the selected goal's local context.
agda_retrieve_context({
  "goal": "goal_…",
  "includeRaw": false
})
→ data = {
    "goal": "goal_…",
    "goalType": "Bool",
    "context": [{ "reifiedName": "x", "type": "Bool", "inScope": true }]
  }

# 4. Ask Agda for a non-mutating case-split preview.
agda_case_split({
  "goal": "goal_…",
  "variables": "x",
  "includeRaw": false
})
→ data.edits[0] = {
    "file": "/workspace/Example.agda",
    "range": <exact UTF-16 range covering `not x = ?`>,
    "replacement": "not true = ?\nnot false = ?",
    "expectedSourceFingerprint": "…"
  }

# 5. Client filesystem action — not an agda-mcp tool:
#    verify the file's SHA-256 fingerprint, then replace precisely the returned
#    range with the returned replacement text.

# 6. Reload the edited file and obtain fresh goal handles.
agda_typecheck({
  "workspace": "workspace_…",
  "includeRaw": false
})
→ data.checked = true
→ data.goals = [{ "handle": "goal_…", … }, { "handle": "goal_…", … }]

For a refinement, use agda_refine in step 4 with an expression; it returns the same fingerprinted edits shape and follows the same apply-then-typecheck flow. Preview operations reload canonical Agda state before returning, so only goal handles from the latest response should be used.

For the faster compound forms, set includeContexts: true on step 1 to receive the goals and every goal context with the load result. Set apply: true on step 4—or enable --apply-edits once for the server—to have it perform steps 5 and 6 as one guarded transaction:

agda_case_split({ "goal": "goal_…", "variables": "x", "apply": true })
→ data.applied = true
→ data.checked = true
→ data.goals = <fresh handles from the edited module>

The preview flow remains the safe startup default and is useful when the client wants to inspect or revise the proposal before changing the file.

Related MCP server: agda-mcp-server

Requirements

Node.js 22 or newer
Agda installed separately and available as agda, or configured explicitly
Agda 2.8.0 for the currently verified protocol adapter

Other Agda versions start in unverified compatibility mode. The server does not bundle Agda or the standard library.

Installation and use

Install the CLI globally:

npm install --global agda-mcp
agda-mcp --help

Or run it without a global installation:

npx -y agda-mcp
# equivalent:
npm exec --yes agda-mcp

The default command starts an MCP stdio server. Stdout is reserved exclusively for MCP framing; operational diagnostics use stderr.

During MCP initialization the server publishes concise instructions that teach the client the core workflow: inspect effective policy, load an absolute module and optional request-selected workspace, prefer compound context retrieval, reuse only fresh opaque goal handles, and distinguish preview from guarded apply/typecheck transformations. The complete instruction block fits within the self-contained 512-character prefix recommended for Codex tool-selection guidance.

A generic model-selected workspace configuration looks like this:

{
  "mcpServers": {
    "agda": {
      "command": "npx",
      "args": ["-y", "agda-mcp", "--dynamic-workspaces"]
    }
  }
}

The server is installed once. The model then selects an active workspace on its first load instead of requiring a separate client entry for each project:

agda_load_module({
  "modulePath": "/absolute/path/to/project/Main.agda",
  "workspaceRoot": "/absolute/path/to/project"
})

Both paths must exist and be absolute. The server resolves symlinks, requires the module to remain within the selected root, discovers the nearest .agda-lib, and lazily starts or reuses that project's long-lived Agda process. agda_server_info reports this mode as capabilities.workspaceSelection: "request".

--dynamic-workspaces deliberately broadens the directories that MCP calls can target to anything accessible to the server process. Only enable it for a trusted local model/client. Without the flag, a supplied workspaceRoot must exactly match a configured root. The server otherwise uses MCP filesystem roots when the client publishes them, falling back to its working directory. The restricted configuration remains available when a fixed allowlist is preferred:

{
  "command": "npx",
  "args": ["-y", "agda-mcp"],
  "env": {
    "AGDA_MCP_OPTIONS": "{\"workspaceRoots\":[\"/absolute/path/to/project\"]}"
  }
}

Enable in-place transformations

Start the server with --apply-edits to make case split, refine, and auto write their proposed source changes and immediately typecheck them by default:

agda-mcp --apply-edits
# or
npx -y agda-mcp --apply-edits

For an MCP client configuration, add the flag to the command arguments:

{
  "command": "npx",
  "args": ["-y", "agda-mcp", "--apply-edits"]
}

It composes with runtime workspace selection:

npx -y agda-mcp --dynamic-workspaces --apply-edits

Clients that configure the server through the environment can equivalently set "applyEditsByDefault": true inside AGDA_MCP_OPTIONS. The command-line flag wins over an environment value. agda_server_info reports the effective mode as capabilities.transformationDefault.

This mode does not permit arbitrary writes: only edits proposed by Agda for the currently loaded, fingerprint-matching source are eligible. A particular tool call can still request apply: false to obtain a non-mutating preview.

Configuration

Initialization policy is supplied as a JSON object in AGDA_MCP_OPTIONS. Unknown fields and invalid limits are rejected before an Agda process starts.

Option	Meaning	Default
`agdaExecutable`	Executable name or path resolved at server startup	`agda`
`workspaceRoots`	Allowed absolute roots for direct module targets	MCP roots or cwd
`allowDynamicWorkspaces`	Allow a load request to select a root outside `workspaceRoots`	`false`
`includePaths`	Extra project-relative include paths	`[]`
`libraries`	Additional registered Agda libraries	`[]`
`libraryFile`	Alternate Agda libraries file	Agda default
`additionalFlags`	Extra `Cmd_load` flags	`[]`
`workspaceOverrides`	Per-workspace include/library/flag overrides	`[]`
`loadTimeoutMs`	Load and restoration command timeout	`120000`
`queryTimeoutMs`	Read/query command timeout	`30000`
`transformationTimeoutMs`	Case split/refine/auto timeout	`60000`
`commandTimeoutMs`	Compatibility umbrella and installation-probe timeout	`30000`
`maxQueuedCommands`	Maximum running plus queued calls per workspace	`64`
`rawResponseLimitBytes`	Soft native-event return budget per command	`131072`
`stderrReturnLimitBytes`	Soft captured-stderr return budget	`32768`
`maxCommandOutputBytes`	Hard aggregate child-output limit	`16777216`
`allowAgdaExec`	Permit `--allow-exec` in resolved flags	`false`
`abortGraceMs`	Grace period before escalating an aborted command	`1000`
`probeTimeoutMs`	Installation-probe timeout	`10000`
`probeMaxBufferBytes`	Installation-probe output buffer	`1048576`
`handleEntropyBytes`	Random bytes per workspace/goal/job handle (min `16`)	`24`
`asyncMode`	`never`, `auto`, or `always`; see below	`auto`
`deferAfterMs`	How long a tool call may block before deferring to a job	`1000`
`maxJobWaitMs`	Ceiling on a single `agda_job_await` wait	`30000`
`jobRetentionMs`	How long an uncollected finished job is kept	`300000`
`maxTrackedJobs`	Maximum concurrently tracked jobs	`64`
`progressIntervalMs`	Heartbeat for `notifications/progress`	`2000`
`includeRawByDefault`	Ship Agda's native event log	`false`
`maxBatchGoals`	Maximum goals one batched request may resolve	`32`
`applyEditsByDefault`	Apply/typecheck transformations when `apply` is omitted	`false`

Non-blocking operation

Typechecking a large development can take minutes, and holding the MCP request open for that whole time stalls the calling agent completely.

Slow calls defer by default so one expensive load does not hold an agent turn open indefinitely. A call that outruns deferAfterMs returns a job handle instead of blocking:

{
  "status": "pending",
  "job": { "id": "job_...", "tool": "agda_load_module", "state": "running", "elapsedMs": 1000 },
  "guidance": "Agda is still working ... call agda_job_await with job \"job_...\""
}

Agda keeps working in the background while the caller is free to do something else, and the result is collected later with agda_job_await. Calls that finish inside the window return their result inline, exactly as before, so fast operations are unchanged.

asyncMode controls the policy: auto (default) defers only calls slower than deferAfterMs, never always blocks until Agda finishes, and always defers every call. Set async: false on one call, or configure asyncMode: "never", when a client requires the legacy fully synchronous behavior.

Per-call overrides

The transport supports these per-call fields; the tool-specific ones are accepted only where indicated. Policy fields shadow configured values for one call only:

Field	Meaning
`timeoutMs`	Agda command timeout for this call
`deferAfterMs`	Defer window for this call, capped by `maxJobWaitMs`
`async`	`true` always returns a job handle; `false` blocks until Agda finishes
`includeRaw`	Include Agda's native event log (see below)
`diagnosticsOnly`	`agda_load_module` / `agda_typecheck` only: errors and warnings
`includeContexts`	`agda_load_module` / `agda_typecheck` only: include all goal contexts
`apply`	Transformation tools only: override server policy (`true` applies, `false` previews)

{ "modulePath": "/src/Slow.agda", "timeoutMs": 600000, "async": true }

The cap on deferAfterMs is deliberate: a per-call value can shorten the window but can never reintroduce unbounded blocking.

Progress and completion notices

While a request is open the server emits notifications/progress every progressIntervalMs, provided the client supplied a progress token. When any job settles it also emits a notifications/message log line. Neither can wake an agent mid-turn — MCP has no such mechanism — but they surface activity in clients that display progress or server logs.

When work is fanned out across several workspaces, agda_job_await_any waits once for whichever job finishes first instead of polling each id in turn.

A deferred job is deliberately detached from the request that created it — the transport closing that request does not cancel the Agda work. Use agda_job_cancel to abandon a job.

When only the legacy commandTimeoutMs is supplied, it applies to all three operation categories. Specific timeout fields override it.

The nearest ancestor .agda-lib inside the selected workspace supplies project includes, dependencies, and flags. Configuration is merged deterministically with global and workspace overrides. Direct source targets must remain inside the selected workspace after canonical path resolution; without --dynamic-workspaces, that selected root must also be configured. Registered imports may live elsewhere.

Tools

Tool	Purpose
`agda_server_info`	Report Agda discovery, compatibility, capabilities, and sessions
`agda_load_module`	Select a workspace and load/typecheck one top-level module
`agda_typecheck`	Reload/typecheck the active workspace module
`agda_retrieve_goals`	Retrieve current visible goals and opaque handles
`agda_retrieve_context`	Retrieve a goal type, local context, and boundary
`agda_retrieve_contexts`	Retrieve contexts for several goals in one round trip
`agda_retrieve_constraints`	Retrieve current constraints
`agda_case_split`	Preview case-split clauses, or apply and typecheck them
`agda_refine`	Preview a refinement/introduction, or apply and typecheck it
`agda_auto`	Preview proof search, or apply and typecheck its solution
`agda_normalize_expression`	Normalize in top-level or goal-local scope
`agda_infer_type`	Infer a type in top-level or goal-local scope
`agda_query_metavariables`	Query visible and backend-published invisible metas
`agda_job_await`	Collect a pending job's result, waiting up to `waitMs`
`agda_job_await_any`	Wait for the FIRST of several jobs to finish
`agda_job_status`	Report a job's state without waiting
`agda_job_cancel`	Abort a pending job
`agda_job_list`	List jobs still running or awaiting collection

agda_load_module returns an opaque workspace handle. Goal-producing results return opaque goal handles bound to the module path, revision, source fingerprint, interaction point, and range. Reloading, recovering, switching modules, or completing any transformation preview invalidates older goal handles.

Expression tools require exactly one of workspace or goal. Input schemas are strict, so contradictory selectors and unknown properties fail before reaching Agda.

Response size

Agda's native event log is the largest part of most responses, so it is omitted by default. The raw field instead contains a summary — eventsOmitted, eventCount, byte counts, completeness, and stderr — so truncation stays detectable:

{ "adapter": "agda-2.8.0", "eventsOmitted": true, "eventCount": 7,
  "capturedBytes": 812, "totalBytes": 812, "stderr": { "chunks": [] } }

Set includeRaw: true for a call that needs the native event sequence, or set includeRawByDefault: true to restore it globally. A per-call value always wins over the server default.

MCP content contains only a compact human-readable summary. The complete normalized result is sent once in structuredContent, avoiding the previous cost of serializing and transmitting the same large object twice.

diagnosticsOnly: true further drops goals and invisibleMetavariables from a load or typecheck, leaving the verdict and diagnostics — useful for the common "did it compile?" question.

Batched goal contexts

For the common load-and-inspect path, includeContexts: true on agda_load_module or agda_typecheck retrieves every newly returned goal context in that same operation. It uses the same bounded aggregation policy as the explicit batch tool below.

agda_retrieve_contexts takes a list of goal handles and returns one entry per goal, in request order:

{ "requested": 3, "succeeded": 2, "failed": 1,
  "contexts": [ { "goal": "goal_...", "ok": true, "context": { "goalType": "Bool", "context": [] } },
                { "goal": "goal_bad", "ok": false, "error": { "code": "STALE_GOAL_HANDLE" } } ] }

Agda still processes the goals one at a time — the interaction process is single-threaded — but the caller pays for one round trip instead of N.

A batch is limited to maxBatchGoals goals. Only failures attributable to one goal — a stale handle, or a command Agda rejected, timed out on, or answered too voluminously — become that goal's entry. Anything describing the session or the batch (SOURCE_CHANGED, NO_ACTIVE_MODULE, UNKNOWN_WORKSPACE, a dead process, a cancellation) aborts the whole call, because the remaining goals could not be answered either.

The returned raw merges every command that ran and is re-truncated against a single rawResponseLimitBytes budget, so a batch cannot build a response larger than one command may. The combined omittedSha256 covers each source transcript's own omission digest followed by every event the merge dropped.

Transformation previews and guarded direct edits

Case split, refine, and auto select their behavior from the per-call apply value when present, otherwise from the server policy. With the default policy or apply: false, they use the non-mutating preview transaction:

Validate the goal handle and loaded source fingerprint.
Ask Agda for a proposal.
Recheck the file fingerprint.
Map the native response to TextEdit values against the immutable snapshot.
Reload the active module before returning, even when the proposal is rejected.
Return fresh restored goals and separate operation/restore transcripts.

Each edit carries its absolute file path, exact UTF-16 range, replacement text, and expected SHA-256 source fingerprint. Clients should verify that fingerprint before applying an edit, then call agda_typecheck. If restoration fails, the server terminates and invalidates the session and returns no safe proposal.

With apply: true, or when --apply-edits supplies that default, the server verifies the proposal targets the active module and fingerprint, rechecks the source immediately before writing, replaces the file atomically, and reloads/typechecks it once. The result reports applied, checked, diagnostics, the new source fingerprint, and fresh goal handles. If the canonical reload itself fails, the server attempts a fingerprint-guarded rollback and refuses that rollback when the edited fingerprint no longer matches. Changes detected during proposal generation or immediately before an atomic replacement are rejected. File mutation is therefore opt-in per transformation call or server startup, while preview remains available as an explicit override. An ordinary Agda type error is a completed result (checked: false), so the applied source remains on disk and its diagnostics are returned for the caller to address; rollback is reserved for failures that prevent a trustworthy canonical result.

Literate prose and code delimiters are excluded from editable code regions. An ambiguous or cross-region proposal fails with UNSUPPORTED_EDIT_SHAPE.

Output limits and recovery

raw retains complete native JSON events up to the soft response budget. When the budget is exceeded, normalized data still returns with byte counts, omitted event count, and an omission digest. Stderr has an independent soft budget. Crossing the hard aggregate limit aborts the command with OUTPUT_LIMIT_EXCEEDED.

Workspace calls are FIFO; different workspaces progress concurrently. Active cancellation first asks Agda to abort and terminates it after a bounded grace period. After an unexpected exit, old handles are revoked. The next workspace operation starts a fresh process and reloads only if the source fingerprint is unchanged.

Upgrading Agda

After installing or switching Agda, restart the MCP server. On every server start it resolves agda again and reprobes the exact version, Agda application directory, and data directory; it does not cache installation or library locations across runs.

That restart is sufficient when the new version still speaks the supported interaction protocol. Agda 2.8.0 is verified. A different detected version is reported as unverified and uses the 2.8.0 adapter conservatively. If a required command or response shape changed, the affected call returns UNSUPPORTED_AGDA_PROTOCOL with native evidence. Upgrade agda-mcp to a version containing an adapter for that Agda release (or contribute one) before relying on those operations.

Development

npm ci
npm run typecheck
npm test
npm run test:fuzz
npm run test:integration
npm run build
npm run smoke
npm run test:package
npm pack --dry-run

The deterministic fuzz campaign combines grammar-aware properties, arbitrary protocol bytes, recorded-corpus mutation, Unicode range/edit properties, strict schema properties, and queue-policy properties. Defaults are 1,000 cases per property and 5,000 corpus mutations. Longer campaigns can be configured with AGDA_MCP_PROPERTY_RUNS, AGDA_MCP_FUZZ_RUNS, and AGDA_MCP_FUZZ_SEED.

Releasing

Subsequent releases are published to npm and GitHub by .github/workflows/release.yml. Before using the workflow for the first time, configure the agda-mcp package on npmjs.com with this trusted publisher:

Provider: GitHub Actions
Organization or user: peterthiemann
Repository: agda-mcp
Workflow filename: release.yml
Environment: none
Allowed action: npm publish

No npm token or GitHub Actions secret is required. The workflow uses a short-lived OpenID Connect credential and npm automatically records provenance for the public package.

For a release, update package.json and package-lock.json to the intended version, commit and push that change, then push an annotated tag named release-X.Y or release-X.Y.Z. The two-part form is normalized to X.Y.0; the resulting version must match package.json exactly. For example:

npm version 0.3.0 --no-git-tag-version
git add package.json package-lock.json
git commit -m "Release 0.3.0"
git push
git tag -a release-0.3.0 -m "Release 0.3.0"
git push origin release-0.3.0

The tag workflow validates the version, installs from the lockfile, runs the typecheck and complete test suite, builds and smoke-tests the executable, packs the exact tarball, publishes that tarball to npm through trusted publishing, and finally creates the GitHub release with the tarball and its SHA-256 file. Merely changing or pushing the workflow does not publish a package; only a new matching release-* tag triggers it. npm versions are immutable, so verify the version before pushing the tag.

Genesis and Codex involvement

This project began as a design dialogue between the project maintainer and OpenAI Codex, operating as a GPT-5-based coding agent. The maintainer set the goals and made the consequential design choices: a standalone TypeScript server, one long-lived Agda interaction process per workspace, a transport-independent application API with stdio first, support for all three on-disk Agda source formats, opaque goal handles, normalized responses retaining native events, and non-mutating transformation previews with mandatory reload.

Codex turned that dialogue into the initial design and implementation plan, then implemented the repository in reviewed checkpoints. Its work included the protocol codec and streaming parser, process/session management, the twelve MCP tools, literate-source edit planning, recovery and packaging, documentation, and the unit, integration, property-based, mutation-fuzz, live-Agda, and MCP stdio tests. Codex also staged, committed, pushed, and followed the CI results under the maintainer's explicit repository authorization. The maintainer remained the project owner and decision-maker throughout; this history records substantial AI-assisted design and implementation, not an OpenAI endorsement of the software.

Design and license

Available Tools

18 tools

agda_autoA

Preview Agda proof search, or atomically apply and typecheck it with apply:true

ParametersJSON Schema

Name	Required	Description
`goal`	Yes	Opaque goal handle returned by the latest module state
`apply`	No	Guardedly write the proposal and typecheck it in one transaction
`async`	No	true always returns a job handle; false blocks until Agda finishes
`query`	No	Agda auto search options
`timeoutMs`	No	Override the configured Agda command timeout for this call
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

A4.2/5.0

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.

agda_case_splitA

Preview a case split, or atomically apply and typecheck it with apply:true

ParametersJSON Schema

Name	Required	Description
`goal`	Yes	Opaque goal handle returned by the latest module state
`apply`	No	Guardedly write the proposal and typecheck it in one transaction
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`variables`	No	Pattern variables to split; empty splits the result
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

A3.8/5.0

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.

agda_infer_typeB

Infer the type of an expression in workspace or goal-local scope

ParametersJSON Schema

Name	Required	Description
`goal`	No
`async`	No	true always returns a job handle; false blocks until Agda finishes
`rewrite`	No
`timeoutMs`	No	Override the configured Agda command timeout for this call
`workspace`	No
`expression`	Yes
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

B3.3/5.0

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.

agda_job_awaitA

Collect the result of a pending Agda job, waiting up to waitMs; returns pending again if still running

ParametersJSON Schema

Name	Required	Description	Default
`job`	Yes	Job id returned by a pending tool result
`waitMs`	No	Milliseconds to wait for completion before returning pending again

TDQS

A4/5.0

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.

agda_job_await_anyA

Wait for the FIRST of several pending jobs to finish; use after fanning work out across workspaces

ParametersJSON Schema

Name	Required	Description	Default
`jobs`	No	Job ids to race; omit to await every tracked job
`waitMs`	No	Milliseconds to wait for the first completion before returning pending

TDQS

A4.2/5.0

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.

agda_job_cancelA

Abort a pending Agda job and release its Agda command slot

ParametersJSON Schema

Name	Required	Description	Default
`job`	Yes	Job id returned by a pending tool result

TDQS

A3.8/5.0

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.

agda_job_listA

List Agda jobs that are still running or awaiting collection

ParametersJSON Schema

Name	Required	Description	Default
No parameters

TDQS

A4.2/5.0

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.

agda_job_statusA

Report the state of a pending Agda job without waiting for it

ParametersJSON Schema

Name	Required	Description	Default
`job`	Yes	Job id returned by a pending tool result

TDQS

A3.9/5.0

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.

agda_load_moduleB

Load and typecheck one top-level Agda module from disk

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`modulePath`	Yes	Absolute path to an .agda, .lagda, or .lagda.md file
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs
`diagnosticsOnly`	No	Return only errors and warnings, dropping goals and metavariables
`includeContexts`	No	Retrieve every returned goal context in the same MCP operation

TDQS

B3.2/5.0

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.

agda_normalize_expressionB

Normalize an expression in workspace or goal-local scope

ParametersJSON Schema

Name	Required	Description
`goal`	No
`mode`	No
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`workspace`	No
`expression`	Yes
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

B3.2/5.0

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.

agda_query_metavariablesC

Query visible and interaction-backend invisible metavariables

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`workspace`	Yes	Opaque workspace handle returned by agda_load_module
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

C2.9/5.0

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.

agda_refineB

Preview a refinement, or atomically apply and typecheck it with apply:true

ParametersJSON Schema

Name	Required	Description
`goal`	Yes	Opaque goal handle returned by the latest module state
`apply`	No	Guardedly write the proposal and typecheck it in one transaction
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`expression`	No	Expression to give; empty or omitted requests intro/refine
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs
`usePatternLambda`	No

TDQS

B3.4/5.0

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.

agda_retrieve_constraintsB

Retrieve constraints for the active module in a workspace

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`workspace`	Yes	Opaque workspace handle returned by agda_load_module
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

B3.1/5.0

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.

agda_retrieve_contextC

Retrieve the type and local context for an opaque goal handle

ParametersJSON Schema

Name	Required	Description
`goal`	Yes	Opaque goal handle returned by the latest module state
`async`	No	true always returns a job handle; false blocks until Agda finishes
`rewrite`	No
`timeoutMs`	No	Override the configured Agda command timeout for this call
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

C2.9/5.0

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.

agda_retrieve_contextsB

Retrieve types and local contexts for several goal handles in one round trip

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`goals`	Yes	Goal handles to fetch contexts for, in one round trip
`rewrite`	No
`timeoutMs`	No	Override the configured Agda command timeout for this call
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

B3.4/5.0

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.

agda_retrieve_goalsC

Retrieve the current visible goals and opaque handles

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`workspace`	Yes	Opaque workspace handle returned by agda_load_module
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

C2.9/5.0

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.

agda_server_infoA

Report the detected Agda installation, compatibility, and active workspaces

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs

TDQS

A3.5/5.0

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.

agda_typecheckB

Reload and typecheck the active module in a workspace

ParametersJSON Schema

Name	Required	Description
`async`	No	true always returns a job handle; false blocks until Agda finishes
`timeoutMs`	No	Override the configured Agda command timeout for this call
`workspace`	Yes	Opaque workspace handle returned by agda_load_module
`includeRaw`	No	Include Agda's native event log; omitted by default because it is large
`deferAfterMs`	No	How long this call may block before returning a job handle; capped by maxJobWaitMs
`diagnosticsOnly`	No	Return only errors and warnings, dropping goals and metavariables
`includeContexts`	No	Retrieve every returned goal context in the same MCP operation

TDQS

B3.2/5.0

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.

Install Server

RayrunBuild, deploy, and operate MCP servers without becoming an infrastructure team.ray.runAd

TDQS

A3.7/5.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.

Maintenance

ActivityMaintained

ResponsivenessSyncing

Resources

Need Help?

Related Servers

Unclaimed servers have limited discoverability.

Looking for Admin?

If you are the server author, to access and configure the admin panel.

Related MCP Connectors

prover
com.axiomatic-ai
Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.
Developer Tools Code Analysis Research & Data
2
mcp-server
com.niftypm
Nifty's MCP server — exposes tasks, projects, messages, and files as tools for AI agents.
Project Management Communication File Systems
2
Agentic Mermaid A
io.github.adewale
Render, verify, describe, and safely edit Mermaid diagrams through MCP.
Data Visualization Software Architecture
9210
slima
io.github.slima-ai
MCP Server for Slima - AI Writing IDE for Novel Authors with AI Beta Reader.
Developer Tools
21

Related MCP Servers

lsp-tools-mcp
Code Analysis Developer Tools
code-yeongyu
A
license
Not graded
quality
C
maintenance
Exposes Language Server Protocol (LSP) tools such as diagnostics, goto definition, find references, symbols, and rename as a stdio MCP server.
Updated 11 days ago (2026-08-24 12:36 UTC)
7
MIT
agda-mcp-server
Developer Tools Code Analysis
InvariantHoldings
A
license
Not graded
quality
A
maintenance
A stateful Model Context Protocol server for interactive Agda proof development, enabling persistent sessions with goal-aware proof actions.
Updated a month ago (2026-08-09 14:54 UTC)
27
1
MIT
lean-lsp-mcp
Code Analysis Code Execution Developer Tools
project-numina
A
license
B
quality
D
maintenance
MCP server for agentic interaction with the Lean theorem prover via LSP, providing tools for understanding, analyzing, and interacting with Lean projects.
Updated 6 months ago (2026-03-11 16:28 UTC)
21
21
MIT
tsserver-mcp-server
Code Analysis Developer Tools
Chia1104
F
license
A
quality
D
maintenance
Exposes TypeScript language service tools (completions, go-to-definition, type info, diagnostics) via MCP for use by AI or IDE clients.
Updated 6 months ago (2026-03-01 09:51 UTC)
7
1

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