@@ -220,15 +220,17 @@ All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
220220| Tool | Description |
221221|------|-------------|
222222| `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
223- | `echidna_prove` | Invoke a prover on a file path (auto-detects from extension) |
224- | `echidna_verify` | Verify inline proof content as a string |
225- | `echidna_search` | Keyword search over the 66,674-proof corpus |
226- | `echidna_suggest_tactics` | Advisory tactic suggestions for a goal |
227- | `echidna_rank_provers` | Advisory prover ranking for a theorem |
223+ | `echidna_prove` | Invoke a prover on proof content (typed outcome) |
224+ | `echidna_verify` | Verify inline proof content (typed outcome) |
225+ | `echidna_verify_raw` | Direct binary invocation (EProver, CaDiCaL, SAT solvers) |
226+ | `echidna_suggest` | Neural tactic suggestions (Julia ML corpus-backed) |
227+ | `echidna_suggest_tactics` | Aspect-tag tactic suggestions — advisory only |
228+ | `echidna_search` | Keyword search over 66,674-proof corpus |
229+ | `echidna_session_create` | Start interactive tactic session |
228230
229231```json
230232{ "tool": "echidna_list_provers", "args": {} }
231- { "tool": "echidna_prove", "args": { "file ": "/path/to/proof.lean ", "prover ": "Lean " } }
233+ { "tool": "echidna_prove", "args": { "prover ": "Lean ", "content ": "theorem t : 1 + 1 = 2 := rfl " } }
232234{ "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
233235```
234236
0 commit comments