Loading ToolBench
MCP server for querying the ACL2 Knowledge Graph in Weaviate
This server demonstrates solid tool engineering with well-defined schemas, clear naming conventions, and comprehensive descriptions. All 6 tools follow verb_noun naming patterns (kg_stats, kg_search, kg_get_*). Tool descriptions are detailed (avg ~220 chars) and explain WHAT, WHEN, and WHAT_RETURNS. Input schemas are complete with proper types, enums, and constraints. However, there are gaps in output schema documentation and error handling guidance. The server lacks explicit guidance on recoverable vs fatal errors, and output structures are not formally documented in tool descriptions. Security and composition are solid for a READ_ONLY knowledge graph tool.
Get a single cell's full content from an ACL2 notebook. Returns the complete code or comment text, cell type, package, execution count, defined symbols, stdout, execute_result, and LLM-generated summaries (a list of what/why/how dicts, one per distinct idea) if available.
Get an ACL2 notebook (source file) with metadata and cell listing. Returns cell count, code cell count, source type, ACL2 version, notebook-level summary, and a paginated list of cells with their code/comments and defined symbols.
Get an LLM-generated summary by its reference key. Returns the what/why/how summaries, scope (cell/notebook/directory), source file, cell index, directory, and symbol names.
Get full details for an ACL2 symbol by its qualified name (e.g. ACL2::APPEND, COMMON-LISP::CAR). Returns the symbol's kind, package, defining code, dependencies (what it calls), dependents (what calls it), and LLM-generated summaries (a list of what/why/how dicts, one per distinct idea). Dependencies and dependents are paginated.
Unified ranked search across the ACL2 Knowledge Graph. Search targets: symbol (ACL2 definitions), code (cell source code), comment (markdown/comment cells), summary (LLM-generated summaries), docs (academic papers from DoclingPapers), acl2_docs (READMEs, HTML, PDFs from the ACL2 source tree). Results are ranked by semantic distance (semantic mode) or relevance (keyword mode). Supports pagination via offset/limit.
Output schemas not documented in tool descriptions. LLMs cannot plan downstream operations without knowing returned fields (e.g., does kg_search return qualified_name, reference_id, confidence_score?). Tool descriptions mention 'returns' but do not formally specify field structure, types, or pagination metadata.
No error classification or recovery guidance. Tool descriptions do not distinguish between retryable errors (network timeout, rate limit), user-fixable errors (invalid query syntax, nonexistent symbol), and fatal errors. Agents cannot plan recovery without this classification.
Parameter 'version' (in kg_get_symbol, kg_get_notebook, kg_get_cell, kg_get_summary) lacks sufficient guidance on valid format and discovery. Description says 'e.g. v1-qwen3-coder' but does not explain how to discover available versions or what happens if an invalid version is specified. This forces trial-and-error or requires a separate discovery tool.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-22 | C | 66 | <=2025-11-25 | v2 |
| 2026-03-09 | F | 26 | - | v1 |
Get overview statistics for the ACL2 Knowledge Graph: collection counts (notebooks, cells, symbols, summaries, docs), symbol kind distribution, and summary scope breakdown.
Pagination behavior underdocumented. Tools accept offset/limit or deps_offset/deps_limit but descriptions do not state whether responses include total_count, has_more, or next_offset. This leaves agents unsure when pagination is exhausted.
Parameter 'paper_filter' (kg_search, docs target) is optional and vaguely described as 'Filter by paper title substring' but does not clarify whether it is substring-match or case-sensitive, or how it interacts with the primary query. LLMs may assume conflicting filter semantics.