Loading ToolBench
Tiny local Lean search MCP server: tree-sitter + SQLite FTS5, no models.
17 tools with complete input schemas and descriptions, but quality is uneven. All tools have descriptions (10-200 chars), and all parameters are typed with descriptions. However, descriptions are often generic ('Get X', 'Search for Y') without explaining WHEN to use the tool or what distinguishes it from similar tools. Output schemas are not documented, LLMs cannot predict response structure. Error handling is absent; no guidance on retryability or recovery. Tool naming is verb-noun compliant but some tools overlap in purpose (search_graph, search_theorems, search_shape all search declarations differently, but this distinction is not explained in descriptions). No tool annotations (readOnlyHint, destructiveHint). index_repository is marked WRITE but lacks confirmation/dry-run pattern for a potentially destructive operation.
Get the status of the search cache
Analyze how well a consumer declaration fits with candidate providers
Look up declarations across multiple repositories
Debug parse a specific Lean file and search for patterns
Get the architecture/module structure of a repository
Get a code snippet for a specific declaration
Get context around a declaration (surrounding code)
Output schemas not documented. LLMs cannot predict response structure, forcing them to guess what fields are returned and how to chain tools. This violates pattern:tool and pattern:response-shaper.
Descriptions are generic and do not explain WHEN to use each tool or how they differ. 'Search for declarations using graph-based semantic search' vs 'Search for theorems and lemmas by name or content' vs 'Search for declarations by type shape', the distinctions are unclear to LLMs. Descriptions should be 50-200 chars and explain the use case.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | C | 63 | <=2025-11-25 | v2 |
Index a Lean repository with tree-sitter and SQLite FTS5
Get the current indexing status of a repository
Get visibility information about indexed declarations
Get available project templates
Search for code patterns in the repository
Search for declarations using graph-based semantic search
Search for declarations by type shape or signature pattern
Search for theorems and lemmas by name or content
Get detailed information card for a specific theorem
Trace dependency paths between declarations
No error handling guidance. Tools do not document what errors can occur, whether they are retryable, or what the LLM should do next. Violates pattern:recovery-guide and pattern:error-classification.
index_repository is a WRITE operation but lacks confirmation/dry-run pattern. Agents could accidentally reindex large repositories or corrupt indices without a safety gate. Violates pattern:confirmation-request.
No tool annotations (readOnlyHint, destructiveHint, idempotentHint). LLMs cannot determine which tools are safe to retry or which modify state. All 17 tools should be annotated per current MCP spec.