Skip to content

Commit c95a347

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(echidna-llm-mcp): Package 8 — full 105-prover surface, CALL-PROTOCOL, consumer snippets
- mod.js: consolidated to single ECHIDNA_REST_URL (:8081 local, flycast:8090 prod); removed non-existent LLM port :7721; echidna_suggest_tactics → /api/tactics/suggest - cartridge.json v0.3.0: 15 tools with correct inputSchema, prover_count=105, fly_private URL documented - docs/CALL-PROTOCOL.adoc: full one-page protocol reference — 15 tools, workflows for verify/prove/suggest/SMT/sessions, prover quick-reference, trust model - README: 15-tool table, correct ports (8081/8090), 10 consumer repos listed Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 634f46a commit c95a347

2 files changed

Lines changed: 143 additions & 145 deletions

File tree

‎cartridges/echidna-llm-mcp/README.adoc‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -121,10 +121,13 @@ usage evidence.
121121
The following repos invoke ECHIDNA via this cartridge. Each has a
122122
call-protocol snippet in its `0-AI-MANIFEST.a2ml`:
123123

124+
* `verification-ecosystem/proven-servers` (active — nesy-solver-api calls echidna-nesy.flycast:8090)
125+
* `verification-ecosystem/nesy-solver`
124126
* `verification-ecosystem/typell`
125127
* `verification-ecosystem/panll`
126-
* `verification-ecosystem/nesy-solver`
127-
* `verification-ecosystem/proven-servers`
128+
* `verification-ecosystem/statistease`
129+
* `verification-ecosystem/ochrance-framework`
130+
* `verification-ecosystem/absolute-zero`
128131
* `verification-ecosystem/typed-wasm`
129-
* `007-lang`
130132
* `developer-ecosystem/aspasia`
133+
* `007-lang`

‎cartridges/echidna-llm-mcp/docs/CALL-PROTOCOL.adoc‎

Lines changed: 137 additions & 142 deletions
Original file line numberDiff line numberDiff line change
@@ -1,210 +1,205 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
22
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3-
= ECHIDNA Call Protocol
3+
= ECHIDNA Call Protocol — How to Invoke ECHIDNA from Any Repo
44
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
5-
:toc:
5+
:revdate: 2026-04-24
6+
:toc: left
67
:toclevels: 2
78

8-
== Overview
9+
== Rule Zero
910

10-
The `echidna-llm-mcp` BoJ cartridge is the *only* authorised entry point for
11-
all ECHIDNA invocations from other hyperpolymath repos. All 105 prover
12-
backends are reachable through 8 tools spread across two backend layers.
11+
**Never call ECHIDNA directly. Always use the `echidna-llm-mcp` BoJ cartridge.**
1312

14-
**NEVER call ECHIDNA directly.** All calls go through BoJ.
13+
The cartridge enforces the 30 s timeout, routes to the right backend URL,
14+
and maintains the trust invariant that advisory suggestions cannot affect
15+
prover trust levels (formally proved in `abi/EchidnaLlm/Protocol.idr`).
1516

16-
== Backend Layers
17+
== Backend
1718

18-
[cols="1,2,2,1"]
19-
|===
20-
| Layer | Env var | Default | Purpose
21-
22-
| REST | `ECHIDNA_REST_URL` | `http://127.0.0.1:8000` | Proof invocation, discovery, search
23-
| LLM | `ECHIDNA_LLM_URL` | `http://127.0.0.1:7721` | Advisory tactic suggestions, prover ranking
24-
|===
19+
All 15 tools route through a single ECHIDNA REST API endpoint:
2520

26-
The REST layer delegates to the ECHIDNA axum server.
27-
The LLM layer delegates to the ECHIDNA LLM proxy (advisory only —
28-
suggestions are hints, not trust-certified results).
21+
[source,bash]
22+
----
23+
# Local (echidna --port 8081, the main.rs default)
24+
export ECHIDNA_REST_URL=http://127.0.0.1:8081
2925
30-
== Tool Reference
26+
# Fly.io private 6PN (production — used by nesy-solver-api, etc.)
27+
export ECHIDNA_REST_URL=http://echidna-nesy.flycast:8090
28+
----
3129

32-
=== Discovery
30+
If `ECHIDNA_REST_URL` is unset the cartridge defaults to `http://127.0.0.1:8081`.
31+
Fly.io cold-start grace is 90 s (Isabelle heap maps on first use; Julia JIT
32+
initialises on first `/api/suggest` call).
3333

34-
`echidna_list_provers` — no required args::
35-
Returns all 105 prover backends with `name`, `tier`, `category`,
36-
and `complexity` fields. Call this first to enumerate valid prover IDs.
34+
== 15 Tools at a Glance
3735

38-
+
39-
[source,json]
40-
----
41-
{ "tool": "echidna_list_provers", "args": {} }
42-
----
36+
[cols="2,1,3"]
37+
|===
38+
| Tool | HTTP | What it does
39+
40+
| `echidna_list_provers` | GET /api/provers | **Start here.** Returns all 105 provers: name, tier, complexity.
41+
| `echidna_health` | GET /api/health | Is the backend up? Returns `{ status, version }`.
42+
| `echidna_rank_provers` | GET /api/provers | Same list — sort by tier/complexity to pick the best prover.
43+
| `echidna_aspect_tags` | GET /api/aspect-tags | Domain tags used by the tactic suggestion model.
44+
| `echidna_prove` | POST /api/prove | Parse + prove a theorem. Returns `{ success, goals, message }`.
45+
| `echidna_verify` | POST /api/verify | Parse → export → binary round-trip. Typed outcome.
46+
| `echidna_verify_raw` | POST /api/verify_raw | Raw binary invocation (EProver, CaDiCaL, etc.).
47+
| `echidna_suggest` | POST /api/suggest | GNN / Julia ML corpus-backed tactic suggestions.
48+
| `echidna_suggest_tactics` | POST /api/tactics/suggest | Aspect-tag model — takes goal text. Advisory only.
49+
| `echidna_search` | GET /api/search?q= | Keyword search over 66,674-proof corpus.
50+
| `echidna_search_theorems` | GET /api/theorems/search?q= | Theorem metadata search.
51+
| `echidna_session_create` | POST /api/session/create | Start interactive tactic session.
52+
| `echidna_session_state` | GET /api/session/:id/state | Current goals + completion flag.
53+
| `echidna_session_apply` | POST /api/session/:id/apply | Apply a tactic.
54+
| `echidna_session_tree` | GET /api/session/:id/tree | Proof tree JSON.
55+
|===
4356

44-
=== Proof Invocation
57+
== Typical Workflows
4558

46-
`echidna_prove` — required: `file`::
47-
Invokes a prover backend on an absolute file path.
48-
Prover is auto-detected from file extension when omitted.
59+
=== 1. Discover Provers, Then Verify
4960

50-
+
5161
[source,json]
5262
----
63+
{ "tool": "echidna_list_provers", "args": {} }
64+
5365
{
54-
"tool": "echidna_prove",
66+
"tool": "echidna_verify",
5567
"args": {
56-
"file": "/path/to/proof.lean",
5768
"prover": "Lean",
58-
"timeout_secs": 120
69+
"content": "theorem zero_add (n : Nat) : 0 + n = n := Nat.zero_add n"
5970
}
6071
}
6172
----
6273

63-
+
64-
Response shape: `{ verified, message, prover, raw_output, stderr }`
74+
Response shape: `{ valid, outcome, goals_remaining, tactics_used }`
75+
Outcome is one of: `PROVED`, `NO_PROOF_FOUND`, `INVALID_INPUT`,
76+
`UNSUPPORTED_FEATURE`, `TIMEOUT`, `INCONSISTENT_PREMISES`,
77+
`PROVER_ERROR`, `SYSTEM_ERROR`.
6578

66-
`echidna_verify` — required: `content`, `prover`::
67-
Verify inline proof content as a string.
68-
No auto-detection — `prover` is always required.
79+
=== 2. Prove with Neural Assistance
6980

70-
+
7181
[source,json]
7282
----
7383
{
74-
"tool": "echidna_verify",
84+
"tool": "echidna_prove",
7585
"args": {
76-
"content": "(assert (not true))\n(check-sat)",
77-
"prover": "Z3"
86+
"prover": "Coq",
87+
"content": "Theorem plus_comm : forall n m : nat, n + m = m + n.\nProof. intros. ring. Qed.",
88+
"neural": true,
89+
"timeout": 120
7890
}
7991
}
8092
----
8193

82-
=== Corpus Search
83-
84-
`echidna_search` — required: `query`::
85-
Keyword search over 66,674 proofs in the training corpus.
86-
Returns matching examples useful for tactic inspiration.
94+
=== 3. Get Tactic Suggestions
8795

88-
+
8996
[source,json]
9097
----
91-
{ "tool": "echidna_search", "args": { "query": "induction list append" } }
92-
----
93-
94-
=== LLM Advisory Ops (non-trust-certified)
95-
96-
`echidna_init`::
97-
Initialise the LLM advisory session. Call once per session.
98-
99-
`echidna_authenticate` — required: `token`::
100-
Authenticate for metered LLM calls.
101-
102-
`echidna_suggest_tactics` — required: `goal`::
103-
Get tactic suggestions from the LLM advisory layer for a proof goal.
104-
Optionally pass `hypotheses` (list of strings), `prover` ID, and `top_k`.
98+
// Corpus-backed neural suggestions (Julia ML layer)
99+
{
100+
"tool": "echidna_suggest",
101+
"args": { "prover": "Idris2", "content": "?hole : n + Z = n", "limit": 10 }
102+
}
105103
106-
+
107-
[source,json]
108-
----
104+
// Aspect-tag model (goal text in, tactics out — advisory only)
109105
{
110106
"tool": "echidna_suggest_tactics",
111-
"args": {
112-
"goal": "n + 0 = n",
113-
"prover": "Lean",
114-
"top_k": 5
115-
}
107+
"args": { "goal": "n + 0 = n", "prover": "Lean", "top_k": 5 }
116108
}
117109
----
118110

119-
`echidna_rank_provers` — required: `theorem`::
120-
Rank all applicable prover backends by expected success probability.
121-
Optionally pass `context` and `domain` (`arithmetic`, `logic`,
122-
`type-theory`, `program-verification`, `security-protocol`,
123-
`constraint-solving`, `model-checking`).
111+
=== 4. SMT / ATP Raw Invocation
124112

125-
+
126113
[source,json]
127114
----
128115
{
129-
"tool": "echidna_rank_provers",
116+
"tool": "echidna_verify_raw",
130117
"args": {
131-
"theorem": "forall n : nat, n + 0 = n",
132-
"domain": "arithmetic"
118+
"prover": "Z3",
119+
"content": "(declare-const x Int)\n(assert (not (= (+ x 1) (+ 1 x))))\n(check-sat)"
133120
}
134121
}
135122
----
136123

137-
== All 105 Prover IDs
124+
Expected: `{ valid: true, exit_code: 0, stdout: "unsat", stderr: "", message: "..." }`
138125

139-
Listed by tier. Use `echidna_list_provers` to get tier, category,
140-
and complexity metadata for each.
126+
=== 5. Interactive Tactic Session
141127

142-
[cols="1,3"]
143-
|===
144-
| Tier | Prover IDs
145-
146-
| 1 — Core ITPs | `Agda`, `Coq`, `Lean`, `Isabelle`, `Z3`, `CVC5`
147-
| 2 — Big Six | `Metamath`, `HOLLight`, `Mizar`
148-
| 3 — Additional | `PVS`, `ACL2`
149-
| 4 — Classic | `HOL4`
150-
| Extended | `Idris2`, `Lean3`
151-
| 5 — First-Order ATPs | `Vampire`, `EProver`, `SPASS`, `AltErgo`
152-
| 6 — Auto-active | `FStar`, `Dafny`, `Why3`
153-
| 7 — Specialised ITPs | `TLAPS`, `Twelf`, `Nuprl`, `Minlog`, `Imandra`
154-
| 8 — Constraint solvers | `GLPK`, `SCIP`, `MiniZinc`, `Chuffed`, `ORTools`
155-
| Oracle | `TypedWasm`
156-
| 9 — Program verifiers | `SPIN`, `CBMC`, `SeaHorn`, `FramaC`, `Viper`
157-
| 9 — SAT solvers | `CaDiCaL`, `Kissat`, `MiniSat`
158-
| 9 — Model checkers | `NuSMV`, `TLC`, `Alloy`, `Prism`, `UPPAAL`
159-
| 9 — Security protocols | `Tamarin`, `ProVerif`
160-
| 9 — Java deductive | `KeY`
161-
| 10 — Delta SMT | `DReal`
162-
| 10 — Logic synthesis | `ABC`
163-
| 11 — HP type checkers | `TypeLL`, `KatagoriaVerifier`, `TropicalTypeChecker`, `ChoreographicTypeChecker`, `EpistemicTypeChecker`, `EchoTypeChecker`, `SessionTypeChecker`, `ModalTypeChecker`, `QTTTypeChecker`, `EffectRowTypeChecker`, `DependentTypeChecker`, `RefinementTypeChecker`, `OrdinaryTypeChecker`, `PhantomTypeChecker`, `PolymorphicTypeChecker`, `ExistentialTypeChecker`, `HigherKindedTypeChecker`, `RowTypeChecker`, `SubtypingTypeChecker`, `IntersectionTypeChecker`, `UnionTypeChecker`, `GradualTypeChecker`, `HoareTypeChecker`, `IndexedTypeChecker`, `LinearTypeChecker`, `AffineTypeChecker`, `RelevantTypeChecker`, `OrderedTypeChecker`, `UniquenessTypeChecker`, `ImmutableTypeChecker`, `CapabilityTypeChecker`, `BunchedTypeChecker`, `TemporalTypeChecker`, `ProvabilityTypeChecker`, `ImpureTypeChecker`, `CoeffectTypeChecker`, `ProbabilisticTypeChecker`, `DyadicTypeChecker`, `HomotopyTypeChecker`, `CubicalTypeChecker`, `NominalTypeChecker`
164-
| Phase 4 variety | `Abella`, `Dedukti`, `Cameleer`, `ACL2s`, `IsabelleZF`, `Boogie`, `Naproche`, `Matita`, `Arend`, `Athena`, `LambdaProlog`, `Mercury`, `Nitpick`, `Nunchaku`
165-
|===
128+
[source,json]
129+
----
130+
// a. Open session
131+
{ "tool": "echidna_session_create", "args": { "prover": "Coq" } }
132+
// → { session_id: "abc123" }
133+
134+
// b. Apply tactics step by step
135+
{ "tool": "echidna_session_apply",
136+
"args": { "session_id": "abc123", "tactic": "intros n." } }
137+
{ "tool": "echidna_session_apply",
138+
"args": { "session_id": "abc123", "tactic": "ring." } }
139+
140+
// c. Confirm completion
141+
{ "tool": "echidna_session_state", "args": { "session_id": "abc123" } }
142+
// → { goals: 0, complete: true }
143+
----
166144

167-
== Trust Model
145+
== Prover Quick Reference
168146

169-
LLM advisory ops (suggest_tactics, rank_provers) are **advisory only**.
170-
They cannot influence ECHIDNA trust levels. This property is formally
171-
verified in `abi/EchidnaLlm/Protocol.idr::allOperationsAdvisory`.
147+
[cols="2,4,1"]
148+
|===
149+
| Domain | Recommended Provers | Tier
150+
151+
| Dependent types | Idris2, Agda, Lean, Coq | 1
152+
| SMT / arithmetic | Z3, CVC5, AltErgo, DReal | 1–2
153+
| Program verification | Dafny, FStar, Why3, Viper, FramaC, Boogie, Cameleer | 2
154+
| First-order ATP | Vampire, EProver, SPASS | 2
155+
| SAT solving | CaDiCaL, Kissat, MiniSat | 2
156+
| Model checking | SPIN, NuSMV, TLC, UPPAAL, Prism, Alloy | 2
157+
| Security protocols | Tamarin, ProVerif | 2
158+
| Hardware / synthesis | ABC | 3
159+
| HP type disciplines | TypeLL, KatagoriaVerifier, LinearTypeChecker, AffineTypeChecker, … | 3
160+
|===
172161

173-
Proof results from `echidna_prove` and `echidna_verify` carry the full
174-
ECHIDNA trust pipeline (solver integrity, certificate checking, axiom
175-
tracking, confidence scoring).
162+
All 105 prover IDs: call `echidna_list_provers`.
176163

177-
== File Extension Auto-Detection
164+
== Error Responses
178165

179-
When `prover` is omitted from `echidna_prove`, ECHIDNA selects by
180-
extension:
166+
All tools return `{ status: int, data: object }`.
181167

182-
[cols="1,2"]
168+
[cols="1,3"]
183169
|===
184-
| Extension | Default prover
185-
186-
| `.lean` | `Lean`
187-
| `.v` | `Coq`
188-
| `.agda` | `Agda`
189-
| `.smt2` | `Z3`
190-
| `.thy` | `Isabelle`
191-
| `.miz` | `Mizar`
192-
| `.fst` | `FStar`
193-
| `.dfy` | `Dafny`
194-
| `.whyml` | `Why3`
195-
| `.mm` | `Metamath`
196-
| `.idr` | `Idris2`
197-
| `.dfg` | `SPASS`
198-
| `.p` / `.tptp` | `Vampire`
170+
| Status | Meaning
171+
172+
| 200 | Success
173+
| 400 | Bad request (malformed prover name, missing required field)
174+
| 404 | Unknown tool, session not found
175+
| 503 | ECHIDNA backend unavailable — check `ECHIDNA_REST_URL`, wait 90 s for cold start
176+
| 504 | 30 s cartridge timeout exceeded
199177
|===
200178

201-
== Environment Quick Reference
179+
== Adding ECHIDNA to a New Repo
202180

203-
[source,bash]
181+
1. Add to `.machine_readable/6a2/ECOSYSTEM.a2ml`:
182+
+
183+
[source,toml]
204184
----
205-
# REST API (proof, discovery, search)
206-
export ECHIDNA_REST_URL=http://127.0.0.1:8000 # default
207-
208-
# LLM advisory layer (tactic suggestions, ranking)
209-
export ECHIDNA_LLM_URL=http://127.0.0.1:7721 # default
185+
{ name = "echidna", relationship = "active-integration",
186+
notes = "Proof verification via echidna-llm-mcp BoJ cartridge." }
210187
----
188+
189+
2. Add the call-protocol snippet to `0-AI-MANIFEST.a2ml` (see any existing
190+
consumer repo, e.g. `verification-ecosystem/proven-servers`).
191+
192+
3. Set `ECHIDNA_REST_URL` in `fly.toml` or your local shell profile.
193+
194+
4. Never import the echidna Rust crates or call the REST API directly —
195+
always go through the `echidna-llm-mcp` cartridge.
196+
197+
== Trust Model
198+
199+
`echidna_suggest` and `echidna_suggest_tactics` are **advisory only**.
200+
Their output is never fed back into the ECHIDNA trust pipeline.
201+
This is formally proved in `abi/EchidnaLlm/Protocol.idr::allOperationsAdvisory`.
202+
203+
`echidna_prove` and `echidna_verify` run the full 11-step trust pipeline:
204+
solver binary integrity (SHAKE3-512 + BLAKE3), SMT cross-checking, proof
205+
certificate verification, axiom tracking, sandboxing, and confidence scoring.

0 commit comments

Comments
 (0)