Skip to content

Commit 00d94cd

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(echidna-llm-mcp): Package 8 — full 105-prover invocation surface
- Cartridge v0.2.0: 8 tools across REST (:8000) + LLM (:7721) backends - Add echidna_list_provers (tool-discovery), echidna_prove, echidna_verify, echidna_search tools routing to ECHIDNA REST API - Expand existing advisory tools to accept any of 105 prover IDs - Fix ABI ProverId bound: Fin 30 → Fin 105 - Create docs/CALL-PROTOCOL.adoc with full per-tool reference - Register 7 consumer repos in ECOSYSTEM.a2ml Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent bbbf22d commit 00d94cd

7 files changed

Lines changed: 493 additions & 51 deletions

File tree

‎.machine_readable/6a2/ECOSYSTEM.a2ml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ projects = [
2020
{ name = "proven-servers", relationship = "dependency", notes = "108 components (94 protocols + 8 core primitives + 6 connectors). BoJ imports proven-mcp types, dbconn, authconn, etc. All zero believe_me." },
2121
{ name = "polystack", relationship = "supersedes", notes = "BoJ replaces polystack's 13 components. poly-cloud/container/db/k8s/git/iac/secret/queue/observability/proof/ssg become cartridges in the BoJ matrix." },
2222
{ name = "PanLL", relationship = "primary-consumer", notes = "PanLL is the primary consumer. Panels need diverse capabilities dynamically — the BoJ catalogue tells them what's available." },
23+
{ name = "echidna", relationship = "dependency", notes = "ECHIDNA 105-prover portfolio exposed via echidna-llm-mcp cartridge (v0.2.0). 8 tools: list_provers, prove, verify, search (REST :8000) + init, authenticate, suggest_tactics, rank_provers (LLM :7721). Consumer repos: typell, panll, nesy-solver, proven-servers, typed-wasm, 007-lang, aspasia." },
2324
{ name = "hypatia", relationship = "integration", notes = "Hypatia scans cartridges for security. SafeReasoning harmonizes Neural (Hypatia) + Symbolic (Echidna) verdicts." },
2425
{ name = "gitbot-fleet", relationship = "integration", notes = "SafeFleet enforces 6-bot gate policy. FleetCertified proof type requires all gates passed." },
2526
{ name = "stapeln", relationship = "dependency", notes = "Container supply chain for node hosting. Chainguard base images, selur-compose, vordr, svalinn, cerro-torre." },

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

Lines changed: 69 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -9,20 +9,52 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
99

1010
== Overview
1111

12-
ECHIDNA LLM proof-tactic neurosymbolic interface
12+
ECHIDNA 105-prover cross-repo invocation surface. Exposes all 105 ECHIDNA
13+
prover backends (proof invocation, tool discovery, tactic advisory) as BoJ
14+
cartridge tools. **All ECHIDNA calls from any hyperpolymath repo must go
15+
through this cartridge — never call ECHIDNA directly.**
1316

14-
== Tools (4)
17+
== Tools (8)
1518

16-
[cols="2,4"]
19+
[cols="2,4,2"]
1720
|===
18-
| Tool | Description
21+
| Tool | Description | Backend
1922

20-
| `echidna_init` | Initialise ECHIDNA LLM endpoint
21-
| `echidna_authenticate` | Authenticate with ECHIDNA token
22-
| `echidna_suggest_tactics` | Get proof tactic suggestions for a goal
23-
| `echidna_rank_provers` | Rank proof strategies by expected success
23+
| `echidna_list_provers` | Tool-discovery: returns all 105 provers with tier/category/complexity | REST :8000
24+
| `echidna_prove` | Invoke a prover on a file path (auto-detects from extension) | REST :8000
25+
| `echidna_verify` | Verify inline proof content as a string | REST :8000
26+
| `echidna_search` | Keyword search over the 66,674-proof corpus | REST :8000
27+
| `echidna_init` | Initialise LLM advisory session | LLM :7721
28+
| `echidna_authenticate` | Authenticate for metered LLM calls | LLM :7721
29+
| `echidna_suggest_tactics` | Advisory tactic suggestions for a proof goal | LLM :7721
30+
| `echidna_rank_provers` | Advisory prover ranking for a theorem | LLM :7721
2431
|===
2532

33+
Advisory tools (suggest_tactics, rank_provers) cannot influence ECHIDNA
34+
trust levels — formally verified in `abi/EchidnaLlm/Protocol.idr`.
35+
36+
== Quick Start
37+
38+
[source,json]
39+
----
40+
// 1. Discover available provers
41+
{ "tool": "echidna_list_provers", "args": {} }
42+
43+
// 2. Prove a Lean 4 file
44+
{
45+
"tool": "echidna_prove",
46+
"args": { "file": "/path/to/proof.lean", "prover": "Lean" }
47+
}
48+
49+
// 3. Verify inline Z3 content
50+
{
51+
"tool": "echidna_verify",
52+
"args": { "content": "(assert (not true))\n(check-sat)", "prover": "Z3" }
53+
}
54+
----
55+
56+
Full protocol documentation: `docs/CALL-PROTOCOL.adoc`
57+
2658
== Architecture
2759

2860
Three-layer stack per the BoJ cartridge standard:
@@ -31,11 +63,22 @@ Three-layer stack per the BoJ cartridge standard:
3163
|===
3264
| Layer | Language | Purpose
3365

34-
| ABI | Idris2 | Formally verified state machine with dependent-type proofs
66+
| ABI | Idris2 | Formally verified state machine; proves advisory-only invariant for all 5 LLM operations; `ProverId` bounded to `Fin 105`
3567
| FFI | Zig | C-ABI implementation: session pool, action metrics, thread safety
36-
| Adapter| Zig | Adapter bridge to the BoJ unified adapter protocol (V-lang predecessors sidelined)
68+
| Adapter| Zig | Adapter bridge to the BoJ unified adapter protocol
3769
|===
3870

71+
== Backend URLs
72+
73+
[source,bash]
74+
----
75+
# REST API (proof, discovery, search) — full 105-prover portfolio
76+
export ECHIDNA_REST_URL=http://127.0.0.1:8000 # default
77+
78+
# LLM advisory layer (tactic suggestions, ranking)
79+
export ECHIDNA_LLM_URL=http://127.0.0.1:7721 # default
80+
----
81+
3982
== Building
4083

4184
[source,bash]
@@ -53,6 +96,19 @@ cd adapter && zig build
5396

5497
== Status
5598

56-
Alpha (CRG D). Cartridge metadata declared in `cartridge.json`; 4 tool(s) exposed.
57-
Not yet dogfooded externally. See `docs/READINESS.md` at repo root for the
58-
project-wide grade table and `docs/practice/DOGFOOD-LOG.adoc` for usage evidence.
99+
Alpha (CRG D). Cartridge metadata declared in `cartridge.json`; 8 tools exposed
100+
across two backend layers (REST + LLM advisory). Not yet dogfooded externally.
101+
See `docs/practice/DOGFOOD-LOG.adoc` for usage evidence.
102+
103+
== Consumer Repos
104+
105+
The following repos invoke ECHIDNA via this cartridge. Each has a
106+
call-protocol snippet in its `0-AI-MANIFEST.a2ml`:
107+
108+
* `verification-ecosystem/typell`
109+
* `verification-ecosystem/panll`
110+
* `verification-ecosystem/nesy-solver`
111+
* `verification-ecosystem/proven-servers`
112+
* `verification-ecosystem/typed-wasm`
113+
* `007-lang`
114+
* `developer-ecosystem/aspasia`

‎cartridges/echidna-llm-mcp/abi/EchidnaLlm/Protocol.idr‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,10 +36,10 @@ public export
3636
confidenceToInt : Confidence -> Int
3737
confidenceToInt (MkConfidence n) = cast (finToNat n)
3838

39-
||| Prover identifier (matches ECHIDNA's 30 backends)
39+
||| Prover identifier (matches ECHIDNA's 105 backends)
4040
public export
4141
data ProverId : Type where
42-
MkProverId : (id : Fin 30) -> ProverId
42+
MkProverId : (id : Fin 105) -> ProverId
4343

4444
||| Operation that the cartridge can perform
4545
public export

‎cartridges/echidna-llm-mcp/cartridge.json‎

Lines changed: 106 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@
33
"spdx": "PMPL-1.0-or-later",
44
"copyright": "Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>",
55
"name": "echidna-llm-mcp",
6-
"version": "0.1.0",
7-
"description": "ECHIDNA LLM proof-tactic neurosymbolic interface",
6+
"version": "0.2.0",
7+
"description": "ECHIDNA 105-prover invocation surface — discovery, proof, verification, and LLM advisory",
88
"domain": "ai",
99
"tier": "Ayo",
1010
"protocols": [
@@ -20,23 +20,102 @@
2020
"base_url": "local://echidna-llm-mcp",
2121
"content_type": "application/json"
2222
},
23+
"backends": {
24+
"rest": {
25+
"env_var": "ECHIDNA_REST_URL",
26+
"default": "http://127.0.0.1:8000",
27+
"description": "ECHIDNA REST API — full 105-prover portfolio"
28+
},
29+
"llm": {
30+
"env_var": "ECHIDNA_LLM_URL",
31+
"default": "http://127.0.0.1:7721",
32+
"description": "ECHIDNA LLM advisory layer — tactic suggestions, prover ranking"
33+
}
34+
},
35+
"provers": "105 backends: Agda, Coq, Lean, Isabelle, Z3, CVC5, Metamath, HOLLight, Mizar, PVS, ACL2, HOL4, Idris2, Lean3, Vampire, EProver, SPASS, AltErgo, FStar, Dafny, Why3, TLAPS, Twelf, Nuprl, Minlog, Imandra, GLPK, SCIP, MiniZinc, Chuffed, ORTools, TypedWasm, SPIN, CBMC, SeaHorn, CaDiCaL, Kissat, MiniSat, NuSMV, TLC, Alloy, Prism, UPPAAL, FramaC, Viper, Tamarin, ProVerif, KeY, DReal, ABC, 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, Abella, Dedukti, Cameleer, ACL2s, IsabelleZF, Boogie, Naproche, Matita, Arend, Athena, LambdaProlog, Mercury, Nitpick, Nunchaku",
2336
"tools": [
37+
{
38+
"name": "echidna_list_provers",
39+
"description": "Tool-discovery endpoint. Returns all 105 prover backends with name, tier, category, and complexity metadata. Call this first to know which prover ID to pass to other tools.",
40+
"inputSchema": {
41+
"type": "object",
42+
"properties": {}
43+
}
44+
},
45+
{
46+
"name": "echidna_prove",
47+
"description": "Invoke a prover backend on a file path. Returns {verified, message, prover, raw_output, stderr}. Auto-detects prover from file extension when prover is omitted.",
48+
"inputSchema": {
49+
"type": "object",
50+
"properties": {
51+
"file": {
52+
"type": "string",
53+
"description": "Absolute path to the proof file. Extension determines default prover: .lean → Lean, .v → Coq, .agda → Agda, .smt2 → Z3, .thy → Isabelle, .miz → Mizar, .fst → FStar, etc."
54+
},
55+
"prover": {
56+
"type": "string",
57+
"description": "Prover backend ID (case-sensitive). One of 105 values — call echidna_list_provers for the full list. Common: Agda, Coq, Lean, Isabelle, Z3, CVC5, Idris2, FStar, Dafny, Why3, Metamath, Vampire, SPASS, EProver."
58+
},
59+
"timeout_secs": {
60+
"type": "integer",
61+
"description": "Timeout in seconds. Default 300."
62+
}
63+
},
64+
"required": ["file"]
65+
}
66+
},
67+
{
68+
"name": "echidna_verify",
69+
"description": "Verify proof content from an inline string rather than a file. Requires prover ID — content is passed directly to the prover binary with no extension-based auto-detection.",
70+
"inputSchema": {
71+
"type": "object",
72+
"properties": {
73+
"content": {
74+
"type": "string",
75+
"description": "Proof content to verify (raw prover syntax)"
76+
},
77+
"prover": {
78+
"type": "string",
79+
"description": "Prover backend ID. One of 105 values — call echidna_list_provers for the full list."
80+
},
81+
"timeout_secs": {
82+
"type": "integer",
83+
"description": "Timeout in seconds. Default 300."
84+
}
85+
},
86+
"required": ["content", "prover"]
87+
}
88+
},
89+
{
90+
"name": "echidna_search",
91+
"description": "Keyword search over the ECHIDNA proof corpus (66,674 proofs across 16 prover systems). Returns matching proof examples useful for tactic inspiration.",
92+
"inputSchema": {
93+
"type": "object",
94+
"properties": {
95+
"query": {
96+
"type": "string",
97+
"description": "Search query (keywords, tactic names, theorem types)"
98+
}
99+
},
100+
"required": ["query"]
101+
}
102+
},
24103
{
25104
"name": "echidna_init",
26-
"description": "Initialise ECHIDNA LLM endpoint",
105+
"description": "Initialise ECHIDNA LLM advisory endpoint",
27106
"inputSchema": {
28107
"type": "object",
29108
"properties": {
30109
"endpoint": {
31110
"type": "string",
32-
"description": "ECHIDNA backend endpoint URL"
111+
"description": "ECHIDNA LLM backend endpoint URL"
33112
}
34113
}
35114
}
36115
},
37116
{
38117
"name": "echidna_authenticate",
39-
"description": "Authenticate with ECHIDNA token",
118+
"description": "Authenticate with ECHIDNA LLM advisory token",
40119
"inputSchema": {
41120
"type": "object",
42121
"properties": {
@@ -49,49 +128,56 @@
49128
"description": "Max calls per session"
50129
}
51130
},
52-
"required": [
53-
"token"
54-
]
131+
"required": ["token"]
55132
}
56133
},
57134
{
58135
"name": "echidna_suggest_tactics",
59-
"description": "Get proof tactic suggestions for a goal",
136+
"description": "LLM-advisory: get proof tactic suggestions for a goal. Advisory only — suggestions are hints, not verified results. Does not affect ECHIDNA trust levels.",
60137
"inputSchema": {
61138
"type": "object",
62139
"properties": {
63140
"goal": {
64141
"type": "string",
65-
"description": "Proof goal (Lean/Idris2/Coq syntax)"
142+
"description": "Proof goal (in target prover's syntax)"
143+
},
144+
"hypotheses": {
145+
"type": "array",
146+
"items": { "type": "string" },
147+
"description": "Available hypotheses in the proof context"
66148
},
67149
"prover": {
68150
"type": "string",
69-
"description": "Target prover: lean4|idris2|coq"
151+
"description": "Target prover ID. One of 105 values — call echidna_list_provers for the full list. Common: Agda, Coq, Lean, Idris2, Isabelle, FStar, Dafny, Z3, CVC5, Why3, Vampire."
152+
},
153+
"top_k": {
154+
"type": "integer",
155+
"description": "Number of tactic suggestions to return (1-50, default 5)"
70156
}
71157
},
72-
"required": [
73-
"goal"
74-
]
158+
"required": ["goal"]
75159
}
76160
},
77161
{
78162
"name": "echidna_rank_provers",
79-
"description": "Rank proof strategies by expected success",
163+
"description": "LLM-advisory: rank all applicable prover backends by expected success probability for a given theorem. Returns ranked list with confidence scores. Advisory only.",
80164
"inputSchema": {
81165
"type": "object",
82166
"properties": {
83167
"theorem": {
84168
"type": "string",
85-
"description": "Theorem statement"
169+
"description": "Theorem statement to rank provers for"
86170
},
87171
"context": {
88172
"type": "string",
89-
"description": "Proof context"
173+
"description": "Proof context (available lemmas, type environment)"
174+
},
175+
"domain": {
176+
"type": "string",
177+
"description": "Proof domain hint: arithmetic, logic, type-theory, program-verification, security-protocol, constraint-solving, model-checking"
90178
}
91179
},
92-
"required": [
93-
"theorem"
94-
]
180+
"required": ["theorem"]
95181
}
96182
}
97183
]

0 commit comments

Comments
 (0)