Loading ToolBench
MCP server wrapper for proofyloops (Lean excerpt/patch/verify + prompt construction)
Server exposes 11 tools with partial schema coverage. Most tools have descriptions (good), but schemas are inferred from code rather than explicitly registered via rmcp macros. The unified dispatcher pattern (tool #1) obscures individual tool contracts. Parameter descriptions exist but lack detail on constraints, ranges, and error recovery. No tool annotations (readOnlyHint/destructiveHint). Output schemas are not documented. Error handling is minimal, most tools return generic error strings without recovery guidance.
Single-entrypoint tool to simplify the MCP surface. Callers pass { "action": "...", "arguments": { ... } } and we dispatch to the underlying tool implementations.
Build a context pack for a declaration: excerpt, nearby declarations, imports, and metadata
Locate all sorry/admit declarations in a Lean file with context
Generate a patch for the nearest sorry/error in a Lean file
Apply a patch to a specific region of a Lean file
Extract proof prompt for a lemma from a Lean repository
Probe an SMT solver for satisfiability of a Lean expression
Unified dispatcher (proofyloops tool #1) obscures individual tool contracts. LLMs cannot see distinct tool names, descriptions, or schemas, only a generic 'action' string parameter. This violates the single-responsibility principle and forces LLMs to reason about action dispatch rather than tool selection.
No tool annotations (readOnlyHint, destructiveHint, idempotentHint). Tools #8 and #9 (patch_nearest, patch_region) are marked WRITE but lack destructiveHint annotation. LLMs cannot distinguish safe from unsafe operations without explicit hints.
Output schemas not documented. Tools return Value/JSON but LLMs have no schema for expected fields, structure, or pagination. This forces LLMs to guess at response shape and breaks downstream tool chaining.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 51 | <=2025-11-25 | v2 |
Reproduce an SMT counterexample for a Lean expression
Tree search for nearest proof candidates using heuristic guidance
Triage a Lean file: verify it, locate sorries, and provide next-action recommendations
Verify a Lean file and return a summary of errors, warnings, and sorry declarations
Parameter descriptions lack constraint details. 'timeout_s' appears in 8 tools but no description specifies valid range (e.g., 1 - 300 seconds). 'max_sorries', 'context_lines', 'max_nearby_decls' lack min/max bounds. LLMs will pass arbitrary values.
Error handling returns generic strings ('missing required string argument: X') without recovery guidance. No distinction between retryable (timeout) vs user-fixable (invalid repo_root) vs fatal errors. LLMs cannot plan recovery.