Skip to content

Commit a6c8456

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(echidna-llm-mcp): implement consult + suggest_tactics cartridge
Adds the echidna-llm-mcp BoJ cartridge that ECHIDNA's llm.rs calls for proof-tactic generation and free-form consultation. Also normalises the router to accept the echidna wire format (operation/params) alongside the canonical BoJ format (tool/arguments) so neither side needs to change. - cartridges/echidna-llm-mcp/mod.js: Deno JS cartridge; routes consult and suggest_tactics to Anthropic Claude via ANTHROPIC_API_KEY. consult returns {answer, model, latency_ms}; suggest_tactics parses the structured JSON that echidna's build_system_prompt instructs the LLM to produce (tactics/recommended_provers/decomposition/auxiliary_lemmas/ reasoning) with a plain-text fallback if JSON parse fails. - cartridges/echidna-llm-mcp/cartridge.json: manifest (Formal Verification domain, Ayo tier, api_key_header auth against vault-mcp). - cartridges/echidna-llm-mcp/README.adoc: wire-protocol and field docs. - elixir/lib/boj_rest/router.ex: accept "operation"/"params" as aliases for "tool"/"arguments" in POST /cartridge/:name/invoke. - elixir/test/router_test.exs: tests for echidna-llm-mcp catalog presence and the operation/params alias path. All 176 tests pass. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 9a8361c commit a6c8456

5 files changed

Lines changed: 587 additions & 2 deletions

File tree

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

Lines changed: 90 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,90 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= echidna-llm-mcp — LLM Advisor Cartridge for ECHIDNA
4+
:toc:
5+
:toc-placement: preamble
6+
7+
LLM advisor cartridge for the ECHIDNA formal verification engine.
8+
Routes proof-guidance requests from `echidna/src/rust/llm.rs` to
9+
Anthropic Claude via the BoJ cartridge host.
10+
11+
== Operations
12+
13+
=== `consult`
14+
15+
Free-form Q&A. ECHIDNA calls this from `/api/v1/consult`.
16+
17+
Request fields (all nested under `params` when sent as `operation`/`params`
18+
or under `arguments` when sent as `tool`/`arguments`):
19+
20+
[cols="1,1,3"]
21+
|===
22+
| Field | Type | Description
23+
| `question` | string | Natural-language question *(required)*
24+
| `context` | string | Optional proof-state context or recent job log
25+
| `model` | string | `opus` / `sonnet` / `haiku` or full model ID (default: `sonnet`)
26+
| `max_tokens` | int | Maximum LLM response tokens (default: 2048)
27+
| `temperature` | float | 0.0–1.0 (default: 0.3)
28+
| `response_format` | string | `markdown` (default) or `text`
29+
|===
30+
31+
Response:
32+
33+
[source,json]
34+
----
35+
{ "answer": "...", "model": "claude-sonnet-4-6", "latency_ms": 1234 }
36+
----
37+
38+
=== `suggest_tactics`
39+
40+
Structured tactic generation for proof search. ECHIDNA builds the prompts
41+
via `build_system_prompt()` and `build_user_prompt()` in `llm.rs` and sends
42+
them verbatim.
43+
44+
Request fields:
45+
46+
[cols="1,1,3"]
47+
|===
48+
| Field | Type | Description
49+
| `system` | string | System prompt (role + JSON schema) from `build_system_prompt()`
50+
| `prompt` | string | User prompt (goal + hypotheses + history) from `build_user_prompt()` *(required)*
51+
| `model` | string | `opus` / `sonnet` / `haiku` or full model ID (default: `sonnet`)
52+
| `max_tokens` | int | Maximum tokens (default: 2048)
53+
| `temperature` | float | 0.0–1.0 (default: 0.2)
54+
| `response_format` | string | `json`
55+
|===
56+
57+
Response (`TacticSuggestionResponse` shape):
58+
59+
[source,json]
60+
----
61+
{
62+
"tactics": [
63+
{ "tactic": "induction n", "confidence": 0.9,
64+
"target_prover": "coq", "rationale": "..." }
65+
],
66+
"recommended_provers": [
67+
{ "prover": "z3", "confidence": 0.8, "reason": "..." }
68+
],
69+
"decomposition": null,
70+
"auxiliary_lemmas": [],
71+
"reasoning": "...",
72+
"model": "claude-sonnet-4-6",
73+
"latency_ms": 2345
74+
}
75+
----
76+
77+
== Auth
78+
79+
Set `ANTHROPIC_API_KEY` in the environment before starting BoJ. In production
80+
this is injected by `vault-mcp`.
81+
82+
== Wire protocol
83+
84+
ECHIDNA sends either:
85+
86+
* `{ "tool": "consult", "arguments": {...} }` — canonical BoJ form
87+
* `{ "operation": "consult", "params": {...} }` — echidna-native form
88+
89+
The BoJ router (`BojRest.Router`) normalises both: `operation` → `tool`,
90+
`params` → `arguments`.

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

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
{
2+
"$schema": "https://boj.dev/schemas/cartridge/v1.json",
3+
"spdx": "PMPL-1.0-or-later",
4+
"copyright": "Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>",
5+
"name": "echidna-llm-mcp",
6+
"version": "0.1.0",
7+
"description": "LLM advisor cartridge for the ECHIDNA formal verification engine. Provides free-form consultation (consult) and structured proof-tactic generation (suggest_tactics) by routing to Anthropic Claude via ANTHROPIC_API_KEY.",
8+
"domain": "Formal Verification",
9+
"tier": "Ayo",
10+
"protocols": [
11+
"REST"
12+
],
13+
"auth": {
14+
"method": "api_key_header",
15+
"header": "x-api-key",
16+
"env_var": "ANTHROPIC_API_KEY",
17+
"credential_source": "vault-mcp"
18+
},
19+
"api": {
20+
"base_url": "https://api.anthropic.com/v1",
21+
"content_type": "application/json",
22+
"extra_headers": {
23+
"anthropic-version": "2023-06-01"
24+
}
25+
},
26+
"tools": [
27+
{
28+
"name": "consult",
29+
"description": "Free-form Q&A with the LLM advisor. Accepts a natural-language question and optional proof-state context; returns a Markdown-formatted answer. Intended for /api/v1/consult calls from ECHIDNA.",
30+
"inputSchema": {
31+
"type": "object",
32+
"properties": {
33+
"question": {
34+
"type": "string",
35+
"description": "The question to answer (natural language)."
36+
},
37+
"context": {
38+
"type": "string",
39+
"description": "Optional additional context (e.g. current proof state summary, recent job log)."
40+
},
41+
"model": {
42+
"type": "string",
43+
"description": "Model hint: 'opus', 'sonnet', 'haiku', or a full Claude model ID. Defaults to claude-sonnet-4-6.",
44+
"default": "sonnet"
45+
},
46+
"max_tokens": {
47+
"type": "integer",
48+
"description": "Maximum tokens in the LLM response.",
49+
"default": 2048
50+
},
51+
"temperature": {
52+
"type": "number",
53+
"description": "Sampling temperature 0.0–1.0.",
54+
"default": 0.3
55+
},
56+
"response_format": {
57+
"type": "string",
58+
"description": "Output style hint: 'markdown' (default) or 'text'.",
59+
"default": "markdown"
60+
}
61+
},
62+
"required": [
63+
"question"
64+
]
65+
}
66+
},
67+
{
68+
"name": "suggest_tactics",
69+
"description": "Structured tactic generation for ECHIDNA proof search. The caller supplies a fully-formed system prompt (role + JSON schema) and user prompt (goal + hypotheses + history). Returns a TacticSuggestionResponse JSON with tactics, recommended_provers, decomposition, auxiliary_lemmas, and reasoning.",
70+
"inputSchema": {
71+
"type": "object",
72+
"properties": {
73+
"system": {
74+
"type": "string",
75+
"description": "System prompt from echidna's build_system_prompt() — defines the advisor role and required JSON response schema."
76+
},
77+
"prompt": {
78+
"type": "string",
79+
"description": "User prompt from echidna's build_user_prompt() — encodes the proof goal, hypotheses, history, and top-k count."
80+
},
81+
"model": {
82+
"type": "string",
83+
"description": "Model hint: 'opus', 'sonnet', 'haiku', or a full Claude model ID. Defaults to claude-sonnet-4-6.",
84+
"default": "sonnet"
85+
},
86+
"max_tokens": {
87+
"type": "integer",
88+
"description": "Maximum tokens in the LLM response.",
89+
"default": 2048
90+
},
91+
"temperature": {
92+
"type": "number",
93+
"description": "Sampling temperature 0.0–1.0. Lower = more deterministic tactic suggestions.",
94+
"default": 0.2
95+
},
96+
"response_format": {
97+
"type": "string",
98+
"description": "Expected output format: 'json' (required for correct TacticSuggestionResponse parsing).",
99+
"default": "json"
100+
}
101+
},
102+
"required": [
103+
"prompt"
104+
]
105+
}
106+
}
107+
]
108+
}

0 commit comments

Comments
 (0)