FEAT-066: scry-mcp — analyze + query as agent tools, verify structurally absent

.github/workflows/ci.yml

@@ -125,7 +125,7 @@ jobs:
       # and drifted independently, so the guard below now checks BOTH.
       - name: cargo clippy — analyzer core, viz, and the domain crates
         run: |
-          cargo clippy -p scry-sai-core -p scry-sai-viz -p scry-sai-interval \
+          cargo clippy -p scry-sai-core -p scry-sai-viz -p scry-sai-mcp -p scry-sai-interval \
                        -p scry-sai-bits -p scry-sai-float -p scry-sai-handle \
                        -p scry-sai-pentagon -p scry-sai-segment -p scry-sai-poly \
                        --all-targets -- -D warnings
@@ -227,7 +227,7 @@ jobs:
           python3 tools/check-gate-coverage.py
       - name: cargo test — analyzer core, viz, and the domain crates
         run: |
-          cargo test -p scry-sai-core -p scry-sai-viz -p scry-sai-interval \
+          cargo test -p scry-sai-core -p scry-sai-viz -p scry-sai-mcp -p scry-sai-interval \
                      -p scry-sai-bits -p scry-sai-float -p scry-sai-handle \
                      -p scry-sai-pentagon -p scry-sai-segment -p scry-sai-poly \
                      -- --nocapture

Cargo.toml

@@ -36,6 +36,7 @@ members = [
     "crates/scry-analyze-core",
     "crates/scry-host-tests",
     "crates/scry-viz",
+    "crates/scry-mcp",
 ]
 # `wasm-lattice` and `scry-analyzer` are the Wasm-component crates
 # (`crate-type = ["cdylib"]`, `#![no_std]`; `scry-analyzer` additionally
@@ -62,6 +63,7 @@ default-members = [
     "crates/scry-analyze-core",
     "crates/scry-host-tests",
     "crates/scry-viz",
+    "crates/scry-mcp",
 ]
 
 [workspace.package]

README.md

@@ -61,14 +61,15 @@ deductive-proof and bounded-model-checking layers do not staff.
 ## status
 
 <!-- claim id=version: "scry-sai-core" crates.io max_version == workspace version -->
-<!-- claim id=crates: publish.rs lists 12 scry-sai-* crates -->
+<!-- claim id=crates: publish.rs lists 13 scry-sai-* crates -->
 <!-- claim id=admit-free: 0 Admitted/admit/Axiom across proofs/rocq/*.v -->
 **v3.2.7 shipped** — the full v0.1 → v3.2 arc is done; scry is a working **sound
-abstract interpreter**, not a scaffold. Shipped and on crates.io: **12 pure
+abstract interpreter**, not a scaffold. Shipped and on crates.io: **13 pure
 `scry-sai-*` crates** (10 abstract domains — interval, region-memory, call-graph
 + reachability, octagon, pentagon, known-bits/congruence, IEEE-754 float,
 Component-Model handle-state, linear-memory segmentation, convex polyhedra —
-plus the analyzer core and the viz) driving `analyze()` over parsed Wasm; a host
+plus the analyzer core, the viz, and the `scry-mcp` MCP server) driving
+`analyze()` over parsed Wasm; a host
 wasmtime harness; runtime-trap classification (PROVEN-SAFE vs POTENTIAL-TRAP);
 ranked remediation guidance + a structured `guidance.json`; and a GitHub Pages
 [verification dashboard](https://pulseengine.github.io/scry).

artifacts/roadmap-3.0.yaml

@@ -1223,6 +1223,21 @@ artifacts:
       The `verify` tool follows FEAT-065 into v3.4.0 with REQ-021 — exposing a
       refuted adjudicator over MCP would put a wrong verdict directly into an
       agent's tool loop, which is the single worst place for it to land.
+
+      RELEASE-MACHINERY NOTE, verified 2026-08-27 and NOT introduced by this
+      feature: `cargo package -p scry-sai-mcp` fails its verify step against
+      the crates.io `scry-sai-core` 3.2.7, which predates the `Query` API
+      (FEAT-067, #188). MEASURED that `scry-sai-viz` ON MAIN fails identically
+      and for the same reason — it uses FEAT-065's `VerifyReport`, also absent
+      from 3.2.7. So this is a PRE-EXISTING MID-CYCLE condition affecting every
+      crate that consumes an unreleased scry-sai-core API, and it resolves at
+      release time via the version bump plus leaf-before-core publish order.
+      The consequence worth writing down: `cargo package` is NOT a valid
+      pre-release check mid-cycle. It will fail for a correct tree, so a
+      release runner who reaches for it as a smoke test gets a red that means
+      nothing. The publish path already handles the ordering (scripts/
+      publish.rs); nothing needs fixing, but nothing should be diagnosed from
+      that failure either.
     tags: [ai-agent, mcp, interop, v3.3]
     fields:
       phase: phase-3

claims.yaml

@@ -95,20 +95,20 @@ claims:
         max: 0
 
   # ── Published-crate count ─────────────────────────────────────────────────
-  # "12 pure scry-sai-* crates". Re-counted from the publish manifest; add a
-  # 13th crate and forget the README → 13 > 12 → red.
-  - id: CRATES-12
+  # "13 pure scry-sai-* crates". Re-counted from the publish manifest; add a
+  # 14th crate and forget the README → 14 > 13 → red.
+  - id: CRATES-13
     doc: README.md
-    text: "12 pure"
+    text: "13 pure"
     evidence:
       - kind: count-max
         pattern: '"scry-sai-[a-z]+"'
         glob: ['scripts/publish.rs']
-        max: 12
-      - kind: count-min       # pin exact: a REMOVED crate also makes "12" stale
+        max: 13
+      - kind: count-min       # pin exact: a REMOVED crate also makes "13" stale
         pattern: '"scry-sai-[a-z]+"'
         glob: ['scripts/publish.rs']
-        min: 12
+        min: 13
 
   # ── i32.add vs OFFICIAL wrapping semantics (the differentiator) ────────────
   # The README's scoped soundness claim rests on WrapAdd.v existing. If the proof

crates/scry-mcp/Cargo.toml

@@ -0,0 +1,33 @@
+[package]
+name = "scry-sai-mcp"
+description = "MCP (Model Context Protocol) server exposing the scry sound abstract interpreter to AI agents: `analyze` (module → structured summary) and `query` (FEAT-067 filters) as MCP tools over JSON-RPC 2.0 on stdio. Structured results only — never HTML, never a multi-MB dump (FEAT-066, TE-011 structured-primary)."
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+repository.workspace = true
+homepage.workspace = true
+authors.workspace = true
+keywords = ["wasm", "static-analysis", "mcp", "verification", "ai"]
+categories = ["development-tools", "wasm"]
+
+[lib]
+name = "scry_mcp"
+path = "src/lib.rs"
+
+[[bin]]
+name = "scry-mcp"
+path = "src/main.rs"
+
+[dependencies]
+# The analyzer library — same single-dependency pattern as scry-viz: a plain
+# `std` host tool consuming the published `AnalysisResult` plain-Rust types.
+scry-sai-core = { path = "../scry-analyze-core", version = "3.2.7" }
+# Hand-rolled JSON-RPC 2.0 (DELIBERATE — no MCP SDK dependency): MCP's stdio
+# transport is newline-delimited JSON-RPC and the server needs exactly three
+# methods (initialize / tools/list / tools/call). serde_json covers that; an
+# SDK would add a dependency tree that has to clear cargo-deny and buys
+# nothing here.
+serde_json = { workspace = true }
+# Accept both `.wat` text and `.wasm` binary module paths (assembled
+# in-process) — same input contract as the scry-viz CLI.
+wat = { workspace = true }

crates/scry-mcp/README.md

@@ -0,0 +1,31 @@
+# scry-sai-mcp
+
+MCP (Model Context Protocol) server exposing the scry sound abstract
+interpreter to AI agents (FEAT-066): JSON-RPC 2.0, newline-delimited, over
+stdio. Agents cannot run `cargo`; this crate replaces shelling out to a CLI or
+scraping a multi-MB JSON dump with two structured tools:
+
+- **`analyze`** — run scry over a Wasm module (`.wasm` or `.wat`, by path) and
+  get a compact summary: advisory counts by actionability class and code,
+  runtime-trap verdicts (proven-safe vs potential-trap), and precision-gap
+  counts. Never HTML, never a full dump.
+- **`query`** — filter the advisories (FEAT-067): `class`, `code`,
+  `func_index`, `op`, `gap_kind`, ANDed, each optional. Matches carry their
+  stable obligation identities (REQ-020) and honesty flags.
+
+`verify` is deliberately absent from the v3.3.0 tool list — the deferral is
+enforced structurally, not by documentation: REQ-021 measured that on real
+inputs the FEAT-065 adjudicator's `discharged` is 0 and every verdict degrades
+to `uncertain`, which must not sit inside an agent's tool loop. It follows
+FEAT-065 into v3.4.0.
+
+## Use
+
+```jsonc
+// MCP client config (stdio server):
+{ "command": "scry-mcp" }
+```
+
+Install: `cargo install scry-sai-mcp`.
+
+The JSON-RPC layer is hand-rolled on `serde_json` — no MCP SDK dependency.