File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 4646
4747### Machine-Readable: `.machine_readable/` ONLY
4848
49+ ## Calling ECHIDNA via BoJ
50+
51+ All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
52+ **Never call ECHIDNA directly — always go through BoJ.**
53+
54+ | Tool | Description |
55+ |------|-------------|
56+ | `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
57+ | `echidna_prove` | Invoke a prover on a file path (auto-detects from extension) |
58+ | `echidna_verify` | Verify inline proof content as a string |
59+ | `echidna_search` | Keyword search over the 66,674-proof corpus |
60+ | `echidna_suggest_tactics` | Advisory tactic suggestions for a goal |
61+ | `echidna_rank_provers` | Advisory prover ranking for a theorem |
62+
63+ ```json
64+ { "tool": "echidna_list_provers", "args": {} }
65+ { "tool": "echidna_prove", "args": { "file": "/path/to/proof.lean", "prover": "Lean" } }
66+ { "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
67+ ```
68+
69+ Full protocol: `boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc`
70+
4971## CORE INVARIANTS
5072
51731. **INDEPENDENCE** — No shared code, libraries, or state with StatistEase
You can’t perform that action at this time.
0 commit comments