From 526bc5ec72ffe11d9a92f180bac6f272821b3278 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 23 Apr 2026 22:09:43 +0000 Subject: [PATCH 1/3] fix(tests): add missing type_info field and remove stale NeuralTagger import Struct initialisers in test helpers and sanity suite were missing the `type_info: None` field added to Hypothesis/Definition/Variable in core.rs. NeuralTagger import in the aspect demo was removed alongside the struct. 625/625 unit tests green after these fixes. docs(echidna-mcp): add README with usage, tool reference, and examples Covers installation, Claude Code settings.json integration, the `prove` tool's parameters and return shape, two JSON-RPC exchange examples, and a troubleshooting section. https://claude.ai/code/session_019HQFtXfCRbUBMDu9dwabGe --- crates/echidna-mcp/README.md | 159 ++++++++++++++++++++++++++++++++ examples/aspect_tagging_demo.rs | 4 +- tests/common/generators.rs | 4 +- tests/common/mod.rs | 1 + tests/sanity_suite.rs | 3 + 5 files changed, 168 insertions(+), 3 deletions(-) create mode 100644 crates/echidna-mcp/README.md diff --git a/crates/echidna-mcp/README.md b/crates/echidna-mcp/README.md new file mode 100644 index 0000000..8648bc9 --- /dev/null +++ b/crates/echidna-mcp/README.md @@ -0,0 +1,159 @@ +# echidna-mcp + +Model Context Protocol server that exposes [ECHIDNA](https://github.com/hyperpolymath/echidna)'s +105-prover portfolio to AI coding agents (Claude Code, Claude API, etc.) as first-class +tool-use actions over stdio. + +## Installation + +```sh +# From source (workspace root) +cargo install --path crates/echidna-mcp + +# Or build without installing +cargo build -p echidna-mcp --release +``` + +The `echidna` binary must be on `PATH` (or set `ECHIDNA_BIN=/abs/path/echidna`). + +## Claude Code integration + +Add to your project's `.claude/settings.json`: + +```json +{ + "mcpServers": { + "echidna": { + "command": "echidna-mcp" + } + } +} +``` + +Or with an explicit binary path: + +```json +{ + "mcpServers": { + "echidna": { + "command": "echidna-mcp", + "env": { "ECHIDNA_BIN": "/usr/local/bin/echidna" } + } + } +} +``` + +## Tools + +### `prove` + +Prove a theorem from a file using one of ECHIDNA's 105 backends. + +| Parameter | Type | Required | Description | +|-----------|------|----------|-------------| +| `file` | string | yes | Absolute path to the proof file | +| `prover` | string | no | Backend name (e.g. `Z3`, `Coq`, `Lean`, `Isabelle`). Auto-detected from extension if omitted. | +| `timeout_secs` | integer | no | Prover timeout in seconds. Default: 300. | + +**Returns** a JSON object: +```json +{ + "verified": true, + "message": "Goal discharged.", + "prover": "Z3", + "raw_output": "...", + "stderr": "" +} +``` + +**Accepted file formats** (by prover): + +| Extension | Prover | +|-----------|--------| +| `.smt2` | Z3, CVC5, Alt-Ergo | +| `.lean` | Lean 4 | +| `.v` | Coq / Rocq | +| `.agda` | Agda | +| `.thy` | Isabelle/HOL | +| `.miz` | Mizar | +| `.fst` | F* | +| `.dfg` | SPASS | +| `.mm` | Metamath | + +## Example JSON-RPC exchanges + +### Prove a trivial SMT goal with Z3 + +Request: +```json +{ + "jsonrpc": "2.0", + "id": 1, + "method": "tools/call", + "params": { + "name": "prove", + "arguments": { + "file": "/tmp/reflexivity.smt2", + "prover": "Z3", + "timeout_secs": 10 + } + } +} +``` + +`/tmp/reflexivity.smt2`: +```smt2 +(declare-const x Int) +(assert (not (= x x))) +(check-sat) +``` + +Response: +```json +{ + "jsonrpc": "2.0", + "id": 1, + "result": { + "content": [{ + "type": "text", + "text": "{\n \"verified\": true,\n \"message\": \"unsat\",\n \"prover\": \"Z3\",\n \"raw_output\": \"unsat\\n\",\n \"stderr\": \"\"\n}" + }] + } +} +``` + +### Auto-detect prover from extension + +```json +{ + "jsonrpc": "2.0", + "id": 2, + "method": "tools/call", + "params": { + "name": "prove", + "arguments": { + "file": "/workspace/lemmas/associativity.v" + } + } +} +``` + +ECHIDNA detects `.v` → Coq and routes accordingly. + +## Troubleshooting + +**`Failed to invoke echidna: No such file or directory`** +: The `echidna` binary is not on PATH. Either install it or set `ECHIDNA_BIN=/full/path/echidna` in the MCP server env config. + +**`verified: false` with empty `message`** +: The prover binary itself is missing. Confirm the target prover is installed: `which z3`, `which coqc`, etc. The `echidna check-prover ` command also reports availability. + +**Timeout / `verified: false` with partial output** +: Increase `timeout_secs`. Complex goals in interactive provers (Isabelle, Coq) may need 60–600 s. Default is 300 s. + +**Wrong prover selected** +: Pass `"prover": "Z3"` (or whichever backend) explicitly rather than relying on auto-detection. + +## License + +PMPL-1.0-or-later — see [LICENSE](../../LICENSE). diff --git a/examples/aspect_tagging_demo.rs b/examples/aspect_tagging_demo.rs index 33da2bc..fdd6fe4 100644 --- a/examples/aspect_tagging_demo.rs +++ b/examples/aspect_tagging_demo.rs @@ -4,7 +4,7 @@ //! Example demonstrating aspect tagging system usage use echidna::aspect::{ - AggregationStrategy, Aspect, AspectTagger, CompositeTagger, NeuralTagger, RuleBasedTagger, + AggregationStrategy, Aspect, AspectTagger, CompositeTagger, RuleBasedTagger, }; use echidna::core::Term; @@ -101,7 +101,7 @@ fn main() { println!("6. Composite Tagger:"); let composite = CompositeTagger::new(AggregationStrategy::WeightedVoting) .add_tagger(Box::new(RuleBasedTagger::new()), 1.0) - .add_tagger(Box::new(NeuralTagger::new()), 0.5); // Neural tagger stub + .add_tagger(Box::new(RuleBasedTagger::with_threshold(0.3)), 0.5); let theorem_name = "functor_category_theory"; let statement = Term::Const("functor".to_string()); diff --git a/tests/common/generators.rs b/tests/common/generators.rs index 3e665f1..c46d120 100644 --- a/tests/common/generators.rs +++ b/tests/common/generators.rs @@ -72,6 +72,7 @@ pub fn arb_hypothesis() -> impl Strategy { name, ty, body, + type_info: None, }) } @@ -95,6 +96,7 @@ pub fn arb_definition() -> impl Strategy { name, ty, body, + type_info: None, }) } @@ -110,7 +112,7 @@ pub fn arb_theorem() -> impl Strategy { /// Strategy for generating a variable pub fn arb_variable() -> impl Strategy { - (var_name(), arb_term()).prop_map(|(name, ty)| Variable { name, ty }) + (var_name(), arb_term()).prop_map(|(name, ty)| Variable { name, ty, type_info: None }) } /// Strategy for generating contexts diff --git a/tests/common/mod.rs b/tests/common/mod.rs index 80904b8..9402331 100644 --- a/tests/common/mod.rs +++ b/tests/common/mod.rs @@ -45,6 +45,7 @@ pub fn multi_goal_proof_state() -> ProofState { name: "h".to_string(), ty: Term::Const("P".to_string()), body: None, + type_info: None, }], target: Term::Const("Q".to_string()), }, diff --git a/tests/sanity_suite.rs b/tests/sanity_suite.rs index 211f1fc..1afb8e6 100644 --- a/tests/sanity_suite.rs +++ b/tests/sanity_suite.rs @@ -53,6 +53,7 @@ fn make_proof_state(bool_vars: &[&str], axioms: &[&str], goal_term: &str) -> Pro ctx.variables.push(Variable { name: v.to_string(), ty: Term::Const("Bool".to_string()), + type_info: None, }); } for ax in axioms { @@ -76,6 +77,7 @@ fn make_proof_state_int(int_vars: &[&str], axioms: &[&str], goal_term: &str) -> ctx.variables.push(Variable { name: v.to_string(), ty: Term::Const("Int".to_string()), + type_info: None, }); } for ax in axioms { @@ -510,6 +512,7 @@ async fn sanity_goal_set_inconsistency() { ctx.variables.push(echidna::core::Variable { name: "P".to_string(), ty: echidna::core::Term::Const("Bool".to_string()), + type_info: None, }); let state = ProofState { goals: vec![ From 470b4ebfd95266d3a0e36be9a7b6790ecb3ef84e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 23 Apr 2026 22:13:22 +0000 Subject: [PATCH 2/3] feat(echidna-mcp): add check_prover and list_provers tools Implements the two remaining MCP tools alongside the existing `prove` tool, completing the three-tool surface described in the project spec. `check_prover` delegates to `echidna check-prover ` and returns `{available, message}`; `list_provers` delegates to `echidna list-provers --format json` and returns `{total, provers}`. https://claude.ai/code/session_019HQFtXfCRbUBMDu9dwabGe --- crates/echidna-mcp/src/main.rs | 114 +++++++++++++++++++++++++++++++++ 1 file changed, 114 insertions(+) diff --git a/crates/echidna-mcp/src/main.rs b/crates/echidna-mcp/src/main.rs index 01541a1..3c4d2ea 100644 --- a/crates/echidna-mcp/src/main.rs +++ b/crates/echidna-mcp/src/main.rs @@ -28,6 +28,7 @@ use rmcp::{ ServerHandler, ServiceExt, }; use serde::{Deserialize, Serialize}; +use std::collections::HashMap; use tokio::process::Command; fn echidna_bin() -> String { @@ -63,6 +64,29 @@ struct ProveResult { stderr: String, } +#[derive(Debug, Deserialize, Serialize, JsonSchema)] +struct CheckProverParams { + /// Prover backend name to check (case-sensitive). Examples: `Z3`, `Lean`, + /// `Coq`, `Agda`, `Isabelle`, `Vampire`, `CVC5`, `Metamath`. + pub prover: String, +} + +#[derive(Debug, Serialize)] +struct CheckProverResult { + /// Whether the prover binary was found and is executable. + available: bool, + /// Human-readable status message. + message: String, +} + +#[derive(Debug, Serialize)] +struct ListProversResult { + /// Total number of supported prover backends. + total: usize, + /// Map from prover name to a brief description. + provers: HashMap, +} + #[derive(Clone)] struct EchidnaMcp { tool_router: ToolRouter, @@ -137,6 +161,96 @@ impl EchidnaMcp { }; serde_json::to_string_pretty(&result).unwrap_or_default() } + + /// Check whether a named prover backend is available on this system. + #[tool( + name = "check_prover", + description = "Check whether a named prover backend is installed and \ + reachable. Returns {available: bool, message: string}. \ + Example: check_prover({\"prover\": \"Z3\"})." + )] + pub async fn check_prover(&self, params: Parameters) -> String { + let prover = params.0.prover; + + let mut cmd = Command::new(echidna_bin()); + cmd.arg("check-prover").arg(&prover); + + let result = match cmd.output().await { + Ok(output) => { + let stdout = String::from_utf8_lossy(&output.stdout).into_owned(); + let available = output.status.success() + || stdout.contains("available") + || stdout.contains("found"); + let message = if stdout.trim().is_empty() { + let stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + if stderr.trim().is_empty() { + if available { + format!("{prover} is available") + } else { + format!("{prover} is not available") + } + } else { + stderr.lines().take(3).collect::>().join("\n") + } + } else { + stdout.trim().to_string() + }; + CheckProverResult { available, message } + } + Err(e) => CheckProverResult { + available: false, + message: format!("Failed to invoke echidna: {e}"), + }, + }; + + serde_json::to_string_pretty(&result).unwrap_or_default() + } + + /// List all 105 prover backends supported by ECHIDNA. + #[tool( + name = "list_provers", + description = "List all 105 prover backends supported by ECHIDNA, \ + grouped by category. Returns {total: int, provers: {name: description}}." + )] + pub async fn list_provers(&self, _params: Parameters<()>) -> String { + let mut cmd = Command::new(echidna_bin()); + cmd.arg("list-provers").arg("--format").arg("json"); + + match cmd.output().await { + Ok(output) if output.status.success() => { + let stdout = String::from_utf8_lossy(&output.stdout).into_owned(); + // Return the raw JSON from the CLI if it looks like JSON, else wrap it. + if stdout.trim_start().starts_with('{') || stdout.trim_start().starts_with('[') { + stdout + } else { + // Wrap plain-text listing as a simple result object. + let lines: Vec<&str> = stdout.lines().filter(|l| !l.trim().is_empty()).collect(); + let provers: HashMap = lines + .iter() + .map(|l| (l.trim().to_string(), String::new())) + .collect(); + let result = ListProversResult { + total: provers.len(), + provers, + }; + serde_json::to_string_pretty(&result).unwrap_or_default() + } + } + Ok(output) => { + let stderr = String::from_utf8_lossy(&output.stderr).into_owned(); + let result = serde_json::json!({ + "error": format!("echidna list-provers failed: {}", stderr.trim()) + }); + serde_json::to_string_pretty(&result).unwrap_or_default() + } + Err(e) => { + let result = serde_json::json!({ + "error": format!("Failed to invoke echidna: {e}") + }); + serde_json::to_string_pretty(&result).unwrap_or_default() + } + } + } } #[tool_handler(router = self.tool_router)] From fb06ae8959ad4f4d7a92e1d87cd7265f1bf25165 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 23 Apr 2026 22:13:28 +0000 Subject: [PATCH 3/3] docs(echidna-mcp): add README with usage, tool reference, examples Covers installation, Claude Code integration (copy-paste JSON block), all three tools (prove, check_prover, list_provers) with parameter tables and return schemas, two example JSON-RPC exchanges (Z3 prove + check_prover), and a troubleshooting section. Adds SPDX header. https://claude.ai/code/session_019HQFtXfCRbUBMDu9dwabGe --- crates/echidna-mcp/README.md | 58 ++++++++++++++++++++++++++++++++---- 1 file changed, 53 insertions(+), 5 deletions(-) diff --git a/crates/echidna-mcp/README.md b/crates/echidna-mcp/README.md index 8648bc9..34b99f2 100644 --- a/crates/echidna-mcp/README.md +++ b/crates/echidna-mcp/README.md @@ -1,3 +1,6 @@ + + + # echidna-mcp Model Context Protocol server that exposes [ECHIDNA](https://github.com/hyperpolymath/echidna)'s @@ -80,6 +83,38 @@ Prove a theorem from a file using one of ECHIDNA's 105 backends. | `.dfg` | SPASS | | `.mm` | Metamath | +### `check_prover` + +Check whether a named prover backend is installed and reachable on the current system. + +| Parameter | Type | Required | Description | +|-----------|------|----------|-------------| +| `prover` | string | yes | Prover backend name (case-sensitive). Examples: `Z3`, `Lean`, `Coq`, `Vampire`. | + +**Returns** a JSON object: +```json +{ + "available": true, + "message": "Z3 is available" +} +``` + +### `list_provers` + +List all 105 prover backends supported by ECHIDNA. Takes no parameters. + +**Returns** a JSON object: +```json +{ + "total": 105, + "provers": { + "Z3": "SMT solver (Microsoft Research)", + "Lean": "Lean 4 interactive proof assistant", + "...": "..." + } +} +``` + ## Example JSON-RPC exchanges ### Prove a trivial SMT goal with Z3 @@ -122,23 +157,36 @@ Response: } ``` -### Auto-detect prover from extension +### Check that Z3 is installed +Request: ```json { "jsonrpc": "2.0", "id": 2, "method": "tools/call", "params": { - "name": "prove", + "name": "check_prover", "arguments": { - "file": "/workspace/lemmas/associativity.v" + "prover": "Z3" } } } ``` -ECHIDNA detects `.v` → Coq and routes accordingly. +Response: +```json +{ + "jsonrpc": "2.0", + "id": 2, + "result": { + "content": [{ + "type": "text", + "text": "{\n \"available\": true,\n \"message\": \"Z3 is available\"\n}" + }] + } +} +``` ## Troubleshooting @@ -146,7 +194,7 @@ ECHIDNA detects `.v` → Coq and routes accordingly. : The `echidna` binary is not on PATH. Either install it or set `ECHIDNA_BIN=/full/path/echidna` in the MCP server env config. **`verified: false` with empty `message`** -: The prover binary itself is missing. Confirm the target prover is installed: `which z3`, `which coqc`, etc. The `echidna check-prover ` command also reports availability. +: The prover binary itself is missing. Confirm the target prover is installed: `which z3`, `which coqc`, etc. The `check_prover` tool also reports availability. **Timeout / `verified: false` with partial output** : Increase `timeout_secs`. Complex goals in interactive provers (Isabelle, Coq) may need 60–600 s. Default is 300 s.