Skip to content

Commit 8d7e83b

Browse files
hyperpolymathclaude
andcommitted
docs(manifest): add ECHIDNA BoJ call-protocol snippet
Package 8: add one-page how-to-call-echidna section to AI manifest. All 8 tools documented; full protocol in boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 412de02 commit 8d7e83b

1 file changed

Lines changed: 22 additions & 0 deletions

File tree

0-AI-MANIFEST.a2ml

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -212,6 +212,28 @@ not a standalone IDE. All machine-readable content is in `.machine_readable/`
212212
ONLY. The verification protocol is the primary interface. Idris2 provides
213213
formal specs, Rust implements the kernel, Zig provides FFI."**
214214

215+
## Calling ECHIDNA via BoJ
216+
217+
All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
218+
**Never call ECHIDNA directly — always go through BoJ.**
219+
220+
| Tool | Description |
221+
|------|-------------|
222+
| `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 |
228+
229+
```json
230+
{ "tool": "echidna_list_provers", "args": {} }
231+
{ "tool": "echidna_prove", "args": { "file": "/path/to/proof.lean", "prover": "Lean" } }
232+
{ "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
233+
```
234+
235+
Full protocol: `boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc`
236+
215237
## META
216238

217239
- **Format Version:** 1.0.0

0 commit comments

Comments
 (0)