Claude/assess agent tier readiness w q od r

crates/echidna-mcp/README.md

@@ -0,0 +1,207 @@
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+
+# 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).

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<String, String>,
+}
+
 #[derive(Clone)]
 struct EchidnaMcp {
     tool_router: ToolRouter<Self>,
@@ -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<CheckProverParams>) -> 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::<Vec<_>>().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<String, String> = 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)]

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());

tests/common/generators.rs

@@ -112,11 +112,7 @@ pub fn arb_theorem() -> impl Strategy<Value = Theorem> {
 
 /// Strategy for generating a variable
 pub fn arb_variable() -> impl Strategy<Value = Variable> {
-    (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