Shannon Prover exposes 4 tools with complete JSON schemas and descriptions. However, descriptions are domain-specific and moderately detailed (100-250 chars), parameter descriptions are present but terse, and error handling guidance is absent. Tool naming follows verb_noun convention (submit_proof_intent, read_easycrypt_source, search_easycrypt_source, resolve_easycrypt_declaration). Schemas are well-formed with proper types and constraints (e.g., search_easycrypt_source has enums for scope, min/max for max_results). No output schemas are documented. The server lacks recovery guidance, error classification, and actionable error messages, critical for agent reasoning. Composition is sound: tools are single-responsibility and chainable (search → read → resolve). However, the domain is highly specialized (EasyCrypt proof assistant), limiting general applicability.

• Document output schemas for all 4 tools. Specify field names, types, and whether results are paginated. Example: 'Returns {matches: [{file: string, line: number, text: string, context?: string}], total: number}'.
• Add error handling guidance to each tool description. Example: 'If path not found, returns 404 with available paths. If search times out, retry with smaller max_results or narrower scope.'
• Expand resolve_easycrypt_declaration description to clarify: What is a 'declaration' (function, lemma, type, module)? What metadata is returned? When should agents call this vs search?
• Constrain submit_proof_intent payload. Document required/optional fields, valid intent types, and example payloads. Replace additionalProperties=true with a strict schema.
• Add pagination support to search_easycrypt_source if result sets can exceed 50 items. Include next_cursor or offset in response.