axle-mcp
Integrates the AXLE (Axiom Lean Engine) CLI with AI assistants to provide comprehensive tools for Lean 4 proof engineering. It enables users to validate, repair, and transform Lean theorems through a remote API without requiring a local Lean installation.
Caution. Specific findings reduced this grade. They are listed on the page. Grades reflect the full trust pyramid: code, verification depth, and reputation. New projects cap at C until adoption is earned.
How we verified
Verified is a snapshot. Live keeps it current, and builds your track record.
⚡ Connect GitHub → continuous verification on every pushwhy connect →Who stands behind it
Vilin97
Source: Glama
Claim it to get a verified publisher badge, a free copy of our full audit findings, and direct contact for any high-priority issues we find. Or connect your repo for our deepest verification, Live Monitored: read-only, revoke anytime. What we access →
Install from
The grade above is for the source repository. Registries can serve a different version, so we mark the ones we were not able to read.
These names and descriptions are the publisher's own, read from the source code. We print them as written. Our assessment is the findings above, not this list.
axle_environmentsList all available Lean environments (versions + Mathlib combinations).
axle_checkEvaluate Lean code and report all messages (errors, warnings, info). Use this to check if Lean code is valid. Faster than verify-proof.
axle_verify_proofValidate a candidate Lean proof against a formal statement (sorry'd theorem). Returns whether the proof correctly proves the stated theorem.
axle_extract_theoremsSplit a Lean file into separate units, each containing a single theorem with its required dependencies. Returns rich metadata per theorem including dependency analysis, tactic counts, type information, and token lists.
axle_renameRename declarations in Lean code. Updates all references automatically.
axle_theorem2lemmaConvert between `theorem` and `lemma` declaration keywords.
axle_theorem2sorryReplace theorem proof bodies with `sorry`. Useful for creating problem templates or proof obligations from complete solutions.
axle_mergeCombine multiple Lean code snippets into a single file, deduplicating imports and shared definitions.
axle_simplify_theoremsSimplify theorem proofs by removing redundant tactics, unused `have` statements, and unnecessary steps.
axle_repair_proofsAttempt to repair broken theorem proofs (e.g. those using `sorry`) by applying various fix strategies. Default terminal tactic is `grind`.
axle_have2lemmaExtract `have` statements from theorem proofs and lift them into standalone top-level lemmas with the appropriate context as parameters.
axle_have2sorryReplace `have` statement proof bodies with `sorry`, keeping the statements. Useful for creating targeted exercises from complete proofs.
axle_sorry2lemmaExtract `sorry` placeholders and type errors from proofs and lift them into standalone top-level lemmas with the full proof context as parameters.
axle_disproveAttempt to disprove theorems by proving their negation and finding counterexamples using property-based testing (plausible).
axle_normalizeStandardize Lean file formatting to prepare for merge operations.
AXLE_BINe =/path/to/axle \AXLE_DEFAULT_ENVIRONMENTe =lean-4.28.0 \Tool annotations
No tools have read-only/destructive annotations
Add readOnlyHint or destructiveHint annotations to every tool so hosts can warn users before invoking.
All four hints declared on every tool
15/15 tools missing one or more hints — axle_environments (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint); axle_check (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint); axle_verify_proof (missing: readOnlyHint, destructiveHint, idempotentHint, openWorldHint), +12 more. OpenAI's directory rejects tools where any of the four hints are missing or non-boolean.
For every tool, set all four hints (readOnlyHint, destructiveHint, idempotentHint, openWorldHint) to explicit true/false values that match the handler’s actual behaviour.
Destructive tools are labelled
2 tools perform destructive updates without destructiveHint — axle_verify_proof deletes at line 140 (os.unlink(stmt_path)); axle_merge deletes at line 293 (os.unlink(path))
Add destructiveHint:true to any tool whose handler calls .delete(), .upsert(), .update(), unlink, rm, DELETE, DROP, REPLACE INTO, or any operation that overwrites existing data.
Tool inputs are validated
14/15 tool handlers declare input schemas (93%)
Declare an inputSchema with zod/joi/yup on every tool definition.
Tool handlers catch errors
Only 2/15 tool handlers wrap calls in try/catch (13%)
Wrap each tool handler body in try/catch and return a structured error response.
License file
No license file
Add a LICENSE file (MIT, Apache-2.0, etc.).
Tests exist
No test files found
Add tests that exercise each declared tool.
Claim the listing to review these findings one by one and send us a correction where you disagree, straight to the team. Claiming also means we tell you when the grade moves, and reach you first if we find anything urgent.
[](https://m8ven.ai/mcp/vilin97/axle-mcp)?variant=verified from the URL.Vetting this one by hand? Tool Check is an MCP that scores other MCPs. Add it once and ask Claude, ChatGPT, or any MCP client to grade a server, surface CVEs, check the publisher, and suggest safer alternatives — before you install.
https://m8ven.ai/api/mcp/tool-check