diff --git a/crates/echidna-mcp/README.md b/crates/echidna-mcp/README.md new file mode 100644 index 0000000..34b99f2 --- /dev/null +++ b/crates/echidna-mcp/README.md @@ -0,0 +1,207 @@ + + + +# 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 | + +### `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 + +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}" + }] + } +} +``` + +### Check that Z3 is installed + +Request: +```json +{ + "jsonrpc": "2.0", + "id": 2, + "method": "tools/call", + "params": { + "name": "check_prover", + "arguments": { + "prover": "Z3" + } + } +} +``` + +Response: +```json +{ + "jsonrpc": "2.0", + "id": 2, + "result": { + "content": [{ + "type": "text", + "text": "{\n \"available\": true,\n \"message\": \"Z3 is available\"\n}" + }] + } +} +``` + +## 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 `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. + +**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/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)] diff --git a/examples/aspect_tagging_demo.rs b/examples/aspect_tagging_demo.rs index 0e1d813..46996a5 100644 --- a/examples/aspect_tagging_demo.rs +++ b/examples/aspect_tagging_demo.rs @@ -104,7 +104,8 @@ fn main() { // were dead. Removed 2026-04-25. Re-add when a real neural tagger // ships (likely via the Julia /predict endpoint or src/rust/neural.rs). let composite = CompositeTagger::new(AggregationStrategy::WeightedVoting) - .add_tagger(Box::new(RuleBasedTagger::new()), 1.0); + .add_tagger(Box::new(RuleBasedTagger::new()), 1.0) + .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 08528e1..c46d120 100644 --- a/tests/common/generators.rs +++ b/tests/common/generators.rs @@ -112,11 +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, - type_info: None, - }) + (var_name(), arb_term()).prop_map(|(name, ty)| Variable { name, ty, type_info: None }) } /// Strategy for generating contexts