File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -195,6 +195,30 @@ ochrance-framework/
1951953. Summarize outcomes
1961964. Ensure all Idris2 files compile: `idris2 --check`
197197
198+ ## Calling ECHIDNA via BoJ
199+
200+ All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
201+ **Never call ECHIDNA directly — always go through BoJ.**
202+
203+ | Tool | Description |
204+ |------|-------------|
205+ | `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
206+ | `echidna_prove` | Invoke a prover on proof content |
207+ | `echidna_verify` | Verify inline proof content (typed outcome) |
208+ | `echidna_verify_raw` | Direct binary invocation (EProver, CaDiCaL, SAT solvers) |
209+ | `echidna_suggest` | Neural tactic suggestions (Julia ML corpus-backed) |
210+ | `echidna_suggest_tactics` | Aspect-tag tactic suggestions — advisory only |
211+ | `echidna_search` | Keyword search over 66,674-proof corpus |
212+ | `echidna_session_create` | Start interactive tactic session |
213+
214+ ```json
215+ { "tool": "echidna_list_provers", "args": {} }
216+ { "tool": "echidna_prove", "args": { "prover": "Lean", "content": "theorem t : 1 + 1 = 2 := rfl" } }
217+ { "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
218+ ```
219+
220+ Full protocol: `boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc`
221+
198222## ATTESTATION PROOF
199223
200224After reading this file, demonstrate understanding by stating:
You can’t perform that action at this time.
0 commit comments