71 tools from the Agda MCP Server, categorised by risk level.
View the Agda policy →agda_auto Attempt to automatically solve a goal using Agda's proof search. By default, writes the solution to the file and reloads. File writes are capped at... agda_auto_all Attempt to automatically solve all goals using Agda's proof search. 2/5 agda_bug_report_bundle Emit a structured bundle for a new bug report or regression, suitable for issue filing or later updates. 2/5 agda_builtin_migration_map Return curated builtin rename/removal records across Agda versions. agda_bulk_status Run a multi-file status sweep and cluster failing files by likely root-cause file. 2/5 agda_cache_info Report the state of every `.agdai` interface artifact for a source file. Lists each artifact's path, the Agda version that produced it (for separat... 2/5 agda_case_split Case-split on a variable in a goal. Returns the new function clauses that replace the current clause. By default, writes changes to the file and re... agda_check_postulates Check an Agda file for postulate declarations. In Kernel/ files, postulates are forbidden by construction. 2/5 agda_compute Normalize (evaluate) an expression. If goalId is provided, evaluates in that goal's context; otherwise evaluates at the top level. agda_context Show only the local context for a specific goal, using Agda's exact Cmd_context query. agda_effective_options Return effective Agda options for a file with source attribution (OPTIONS pragma, .agda-lib flags, wrapper hints, and MCP defaults). agda_elaborate Elaborate an expression in a goal context: normalize and show the fully explicit form. agda_find_clash_source Given a symbol and file, identify local and imported binding sites and the likely `open import` introducing the clash. 2/5 agda_give Fill a goal with an expression. If the expression type-checks against the goal type, the goal is solved. By default, writes the change to the file ... agda_goal Show only the current goal type for a specific goal, using Agda's exact Cmd_goal_type query. agda_goal_analysis Analyze a goal: show its type, parsed context, splittable variables, and suggested next actions. Use this to decide what proof step to take. agda_goal_catalog Return a structured catalog of all goals in the current proof state: goal IDs, types, contexts, splittable variables, and per-goal suggestions. Req... agda_helper_function Generate a helper function type signature for an expression in a goal context. Useful for extracting a subproof into a named lemma. agda_highlight Highlight an expression in a goal context using Agda's Cmd_highlight command. agda_infer Infer the type of an expression. If goalId is provided, infers in that goal's context; otherwise infers at the top level. agda_infer_fixity_conflicts Detect user-defined operators missing fixity declarations that likely bind unexpectedly against imported operators. agda_intro Introduce a lambda or constructor using Agda's exact Cmd_intro command. By default, writes changes to the file and reloads. File writes are capped ... agda_list_modules List Agda modules in a directory tier (MathLib, Foundation, Kernel, Research, Extensions, etc.). Always reports the total module count; paginated t... agda_load Load and type-check an Agda file. This establishes the interactive session — subsequent commands operate on the loaded file's goals. 2/5 agda_load_highlighting_info Load highlighting information for a file using Agda's Cmd_load_highlighting_info. 2/5 agda_load_no_metas Load and type-check an Agda file, failing if unsolved metavariables remain after loading. Note: Cmd_load_no_metas does not accept command-line opti... 2/5 agda_metas List all unsolved metavariables (goals) in the currently loaded file, tagged by owning file so diagnostics from the loaded file can be distinguishe... agda_postulate_closure Return transitive postulate dependencies for a file (optionally scoped to a symbol) grouped by subdirectory. agda_project_progress Project-wide static progress summary by subdirectory: total files, files with holes, files with postulates, and clean-by-scan counts. agda_proof_status Get a complete proof state snapshot: loaded file, staleness, all goals with types, and constraints. Use this instead of calling agda_session_status... agda_protocol_parity Return the current Agda IOTCM parity matrix, distinguishing mapped commands from semantically verified commands and known gaps. agda_read_module Read an Agda module file and return its contents with line numbers. For literate files (.lagda.md, .lagda.tex, etc.), use `codeOnly: true` to extra... 2/5 agda_refine Refine a goal by applying a function. Creates new subgoals for the function's arguments. By default, writes changes to the file and reloads. File w... agda_refine_exact Refine a goal using Agda's exact Cmd_refine command. By default, writes changes to the file and reloads. File writes are capped at 512 KiB of Agda ... agda_reload Reload the currently loaded file and report what changed: which goals were solved, which are new, and the current proof state. agda_search_about Search for definitions in the loaded module matching a query string (searches by type components and name fragments). 2/5 agda_search_definitions Search for a definition, theorem, or type name across Agda modules. 2/5 agda_session_snapshot Return a structured snapshot of the current session state: loaded file, phase, goal counts, completeness, staleness, and suggested next actions. De... agda_session_status Show the current Agda session status: phase, loaded file, and available goal IDs. agda_show_implicit_args Set whether Agda should display implicit arguments. agda_show_irrelevant_args Set whether Agda should display irrelevant arguments. agda_show_module Show the exported contents of an Agda module. If goalId is provided, shows contents visible from that goal's context; otherwise shows top-level con... agda_show_version Show the Agda version and runtime capabilities: supported source extensions, feature flags, and protocol changes. agda_solve_all Attempt to solve all goals that have unique solutions. By default, writes the solutions to the file and reloads. File writes are capped at 512 KiB ... 2/5 agda_solve_one Attempt to solve one goal that has a unique solution using Agda's exact Cmd_solveOne command. By default, writes the solution to the file and reloa... agda_stdlib_migration_map Return the curated stdlib rename map keyed by source and target versions. Use this before applying mechanical rename repairs. agda_term_search Search the goal's context for terms whose type matches the goal type (or a custom target type). Returns candidate expressions that might fill the g... agda_toggle_implicit_args Toggle whether Agda displays implicit arguments. agda_toggle_irrelevant_args Toggle whether Agda displays irrelevant arguments. agda_token_highlighting Load token-based highlighting for a file using Agda's Cmd_tokenHighlighting. agda_tool_recommend Suggest likely next MCP tool calls based on the current semantic proof state. Returns recommendations ordered by priority with rationale, pre-fille... agda_tools_catalog Return the generated manifest view of exposed MCP tools, categories, protocol mappings, and schema field names. Also reports the detected Agda vers... agda_triage_error Classify a raw Agda error into mechanical/proof/toolchain categories with confidence and a machine-readable suggested action. agda_typecheck Type-check an Agda file and return a compact classification-only response. This routes through the same singleton session as agda_load (since issue... agda_verify_builtin Given a builtin name, report whether it is resolvable from the curated builtin map and provide migration hints. agda_why_in_scope Explain why a name is in scope. If goalId is provided, checks within that goal's context; otherwise checks at the top level. agda_abort Send Cmd_abort to the running Agda process. 2/5 agda_add_missing_clauses Generate and optionally insert a missing-clause stub for a function with coverage errors. 3/5 agda_apply_edit Apply a targeted text substitution to an Agda file and reload it. For edits that aren't goal actions — adding imports, renaming symbols, fixing typ... 3/5 agda_apply_rename Apply a scoped textual rename inside one Agda file, optionally re-load it, and return the resulting textual diff. 3/5 agda_backend_hole Send a backend-specific hole payload via Cmd_backend_hole. 2/5 agda_backend_top Send a backend-specific top-level payload via Cmd_backend_top. 2/5 agda_bug_report_update_bundle Emit a structured update bundle for an existing bug report, preserving stable fingerprints and issue linkage. 3/5 agda_constraints Show the current constraint set for the loaded file. 2/5 agda_exit Send Cmd_exit to the running Agda process and let the session shut down cleanly. 2/5 agda_goal_type Show the type and local context for a specific goal. Requires a file to be loaded first via agda_load. 2/5 agda_goal_type_context_check Show the goal context, goal type, and checked elaborated term for an expression in a goal context. 2/5 agda_goal_type_context_infer Show the goal context, goal type, and inferred type of an expression in a goal context. 2/5 agda_suggest_import Suggest `open import` candidates for a missing symbol by reverse-indexing symbol definitions across the repository. 3/5 The Agda MCP server exposes 71 tools across 3 categories: Read, Write, Execute.
Use Intercept, the open-source MCP proxy. Write YAML rules for each tool — rate limits, argument validation, or deny rules — then run Intercept in front of the Agda server.
Agda tools are categorised as Read (56), Write (13), Execute (2). Each category has a recommended default policy.
Open source. One binary. Zero dependencies.
npx -y @policylayer/intercept