The rocq-mcp server provides three tools with explicit schemas and descriptions visible in mcp/server.go. All tools have non-empty descriptions (10-20 words each). Input schemas are present and typed (string, integer, boolean). However, descriptions lack depth and context, they state WHAT but not WHEN or WHY an agent should call each tool. Parameter descriptions are minimal (e.g., 'path to the .v file' is functional but doesn't explain file format constraints or error conditions). Output schema is documented via CheckResult struct with clear fields (CheckedTo, Errors, ProofGoals). Error handling is present but limited, the code calls fmt.Errorf with context, but error messages lack recovery guidance. No parameter validation is visible (e.g., checking file extensions, path validity). Security is reasonable (no secrets exposed), but the close_file tool's WRITE risk is not prominently warned in the description. Overall: functional definitions with basic quality, but missing LLM-optimization guidance and actionable error messages expected in production tools.

• Expand tool descriptions to 50-150 characters explaining WHEN and WHY to call them. E.g., 'check_to_end: Validate a complete Rocq proof file syntax and all proofs. Use after edits to catch errors. Returns line number of first error and proof goals at the end.' vs current 'Check a Rocq (.v) file to the end'.
• Replace internal jargon in descriptions. Change 'DelegationSkip; proofs are admitted and Qed failures appear as diagnostics' to 'Skip proof bodies to check faster, catches syntax errors but misses proof failures. Useful for quick validation during editing.'
• Add destructiveHint or idempotentHint annotations. For close_file, register it with destructiveHint=true to signal to the agent that it causes state mutation. For check tools, use idempotentHint=true to signal they are safe to retry.
• Document the output schema in tool descriptions. Add: 'Returns {checked_to (0-based line number of last checked line), errors (array of {line, message}), proof_goals (proof state if open proof exists at end)}' to each tool.
• Add parameter validation and detailed error messages. For example, when path is invalid, return: 'File not found: /path/to/file.v. Ensure the path is absolute or relative to current directory and the file exists.' instead of a raw error.
• Clarify the relationship between check and check_to_end in their descriptions. E.g., 'check: Validate up to a specific line for incremental checking during editing. check_to_end: Validate the entire file after edits are complete.' This helps the LLM choose between them.