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.

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:

{ "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

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:

1. Validate the goal handle and loaded source fingerprint.

2. Ask Agda for a proposal.

3. Recheck the file fingerprint.

4. Map the native response to TextEdit values against the immutable snapshot.

5. Reload the active module before returning, even when the proposal is rejected.

6. 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

• Changelog

• Initial design

• Implementation plan

• MIT license