Skip to content

Commit 842bd35

Browse files
hyperpolymathclaude
andcommitted
feat(ai-manifest): add ECHIDNA call-protocol snippet (Package 8)
8-tool quick-reference + 3 JSON examples + CALL-PROTOCOL.adoc link. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 315feb3 commit 842bd35

1 file changed

Lines changed: 24 additions & 0 deletions

File tree

AI.a2ml

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,27 @@
1313
## Delivery Promises
1414
- Mention in summaries whether STATE, `contractiles/`, or `.bot_directives/` changed.
1515
- Keep this file in sync with the repository’s status; update it if the governance changes.
16+
17+
## Calling ECHIDNA via BoJ
18+
19+
All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
20+
**Never call ECHIDNA directly — always go through BoJ.**
21+
22+
| Tool | Description |
23+
|------|-------------|
24+
| `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
25+
| `echidna_prove` | Invoke a prover on proof content |
26+
| `echidna_verify` | Verify inline proof content (typed outcome) |
27+
| `echidna_verify_raw` | Direct binary invocation (EProver, CaDiCaL, SAT solvers) |
28+
| `echidna_suggest` | Neural tactic suggestions (Julia ML corpus-backed) |
29+
| `echidna_suggest_tactics` | Aspect-tag tactic suggestions — advisory only |
30+
| `echidna_search` | Keyword search over 66,674-proof corpus |
31+
| `echidna_session_create` | Start interactive tactic session |
32+
33+
```json
34+
{ "tool": "echidna_list_provers", "args": {} }
35+
{ "tool": "echidna_prove", "args": { "prover": "Lean", "content": "theorem t : 1 + 1 = 2 := rfl" } }
36+
{ "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
37+
```
38+
39+
Full protocol: `boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc`

0 commit comments

Comments
 (0)