@@ -134,15 +134,17 @@ All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
134134| Tool | Description |
135135|------|-------------|
136136| `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
137- | `echidna_prove` | Invoke a prover on a file path (auto-detects from extension) |
138- | `echidna_verify` | Verify inline proof content as a string |
139- | `echidna_search` | Keyword search over the 66,674-proof corpus |
140- | `echidna_suggest_tactics` | Advisory tactic suggestions for a goal |
141- | `echidna_rank_provers` | Advisory prover ranking for a theorem |
137+ | `echidna_prove` | Invoke a prover on proof content (typed outcome) |
138+ | `echidna_verify` | Verify inline proof content (typed outcome) |
139+ | `echidna_verify_raw` | Direct binary invocation (EProver, CaDiCaL, SAT solvers) |
140+ | `echidna_suggest` | Neural tactic suggestions (Julia ML corpus-backed) |
141+ | `echidna_suggest_tactics` | Aspect-tag tactic suggestions — advisory only |
142+ | `echidna_search` | Keyword search over 66,674-proof corpus |
143+ | `echidna_session_create` | Start interactive tactic session |
142144
143145```json
144146{ "tool": "echidna_list_provers", "args": {} }
145- { "tool": "echidna_prove", "args": { "file ": "/path/to/proof.lean ", "prover ": "Lean " } }
147+ { "tool": "echidna_prove", "args": { "prover ": "Lean ", "content ": "theorem t : 1 + 1 = 2 := rfl " } }
146148{ "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
147149```
148150
0 commit comments