Skip to content

Commit 98a98d0

Browse files
hyperpolymathclaude
andcommitted
docs(manifest): add ECHIDNA BoJ call-protocol snippet
Package 8: all 8 cartridge tools documented. Protocol reference: boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 0a865ec commit 98a98d0

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
@@ -126,6 +126,28 @@ Nesy Solver/
126126
✅ Understand canonical location: `.machine_readable/`
127127
✅ State understanding of canonical locations
128128

129+
## Calling ECHIDNA via BoJ
130+
131+
All ECHIDNA invocations go through the `echidna-llm-mcp` BoJ cartridge.
132+
**Never call ECHIDNA directly — always go through BoJ.**
133+
134+
| Tool | Description |
135+
|------|-------------|
136+
| `echidna_list_provers` | Discover all 105 provers with tier/category/complexity |
137+
| `echidna_prove` | Invoke a prover on a file path (auto-detects from extension) |
138+
| `echidna_verify` | Verify inline proof content as a string |
139+
| `echidna_search` | Keyword search over the 66,674-proof corpus |
140+
| `echidna_suggest_tactics` | Advisory tactic suggestions for a goal |
141+
| `echidna_rank_provers` | Advisory prover ranking for a theorem |
142+
143+
```json
144+
{ "tool": "echidna_list_provers", "args": {} }
145+
{ "tool": "echidna_prove", "args": { "file": "/path/to/proof.lean", "prover": "Lean" } }
146+
{ "tool": "echidna_suggest_tactics", "args": { "goal": "n + 0 = n", "prover": "Lean" } }
147+
```
148+
149+
Full protocol: `boj-server/cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc`
150+
129151
## ATTESTATION PROOF
130152

131153
**"I have read the AI manifest. All machine-readable content (state files, anchors, policies, bot directives, contractiles, AI guides) is located in `.machine_readable/` ONLY, community metadata is in `.github/`, and `AUDIT.adoc` constrains release and publication claims. I will not create duplicate files in the root directory or make optimistic claims that bypass the audit gate."**

0 commit comments

Comments
 (0)