Server defines 8 tools with complete JSON schemas and descriptions. Naming follows verb_noun convention (coq_open_goals, coq_run_tactic, etc.). Descriptions are present but brief (avg ~60 chars, below the 194-char baseline). All tools have input schemas with typed properties. However, parameter descriptions are sparse or missing for many fields (e.g., 'memo', 'hash', 'compact' lack explanations of what they control). Output schemas are not documented, LLMs cannot predict response structure. Error handling is minimal; no recovery guidance or categorization. No tool annotations (readOnlyHint/destructiveHint) despite clear risk levels (READ_ONLY vs WRITE). Position object is reused across tools but lacks description of coordinate system (0-based vs 1-based is mentioned once in coq_open_goals but not consistently).

• Document output schemas for all tools. Example: coq_open_goals should return {goals: [{goal: string, hypotheses: string[]}], proof_name?: string}. This enables agents to extract and chain results.
• Add descriptions to all optional parameters. For 'memo': 'Enable memoization of proof states for faster re-execution (default: false)'. For 'compact': 'Omit verbose hypothesis details in goal display (default: false)'.
• Add tool annotations to schema. Mark coq_apply_edit and coq_insert_tactic with destructiveHint: true; mark all read-only tools with readOnlyHint: true. This enables agents to reason about side effects.
• Implement error recovery guidance. Wrap coq-lsp calls with try-catch; return structured errors like {error: 'document_not_ready', retry_after_ms: 500, message: 'File is still being parsed. Retry in 500ms.'}.
• Standardize position documentation. Add '(0-based line and character indices)' to the position parameter description in coq_proof_state, coq_get_state_at_pos, and coq_check to match coq_open_goals.

Inferred effective spec: <=2025-11-25.

• Relies on Sampling (deprecated) - integrate directly with the LLM provider API