MCP server for Axiom Lean Engine (AXLE) — exposes Lean verification tools to Claude Code and other MCP clients
Scoring was not performed
Endpoint tool definitions are loaded from external AXLE API at startup, not visible in source code. Their names, descriptions, parameter schemas, and output formats cannot be verified. Per hard scoring rules, inferred tool definitions cap at 50 overall.
No parameter descriptions provided for endpoint tools. The code calls field_to_json_schema() which copies 'description' from InputField if present, but there is no validation that API-provided field definitions include descriptions. Many endpoint parameters will likely lack descriptions, violating the 'every parameter must have a description' baseline (100% of A+ tools have this).
list_environments description is only 62 characters: 'List available Lean environments on the AXLE server.' This is below the baseline average of 194 chars (p10=34, p90=392). While technically compliant with the 10 - 1024 character range, it lacks context about WHEN to call this tool, what the output structure is, and any prerequisites. Should include: 'Use this tool before calling other endpoints to see available Lean environments (e.g. lean-4.0.0). Returns a list of environment objects with names and metadata. Often called first to select a default_environment.'
Input schema for list_environments is empty (no properties, no parameters). While correct for a discovery tool, the description should explicitly state 'This tool takes no parameters.' to avoid LLM confusion about whether a parameter is required or optional.
No output schema documented for list_environments or any endpoint tool. The code returns `json.dumps(ENVIRONMENTS, indent=2)` as raw JSON text, but LLMs need to know the structure: Are environments objects with 'name' and 'id'? What other fields? Is there pagination? Without a documented schema, LLMs cannot plan downstream calls or extract needed IDs. See baseline: '100% of A+ tools have documented return types.'
No error descriptions or recovery guidance. If an endpoint call fails with HTTP 200 but contains 'internal_error', 'user_error', or 'error' keys, the code raises RuntimeError with the API response text. An LLM receives only the raw error message and cannot determine: Is this retryable? Should I try a different parameter? What field did I get wrong? Per pattern:recovery-guide, error responses must guide the LLM on next steps.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-22 | F | 0 | 2026-07-28+ | v2 |
| 2026-03-09 | F | 43 | - | v1 |