I spent the past year asking why every MCP security tool is a scanner that runs before deployment — when the attacks that actually work (rug pulls, runtime tool poisoning, cross-server escalation) happen after. Scanners catch known patterns in config files. They can't catch a tool server that changes its schema after you approved it. So I built a runtime enforcement layer instead. VellaVeto is a proxy that sits between your MCP client and tool servers, evaluating every call against policy before it executes. If policy evaluation fails for any reason — missing context, internal error, no matching rule — the call is denied. Fail-closed, not fail-open. Try it: cargo install vellaveto-proxy && vellaveto-proxy --protect shield -- ./your-mcp-server That single flag blocks credential grabs (.aws/.ssh/.env), exfiltration domains, injection patterns, and DLP leaks with no config files. Two stricter modes (fortress, vault) go up to default-deny with human approval for writes. The core is Rust (~92%), <5ms P99 evaluation. Policy engine properties are formally verified in TLA+ (fail-closed under network partition, no policy bypass on concurrent evaluation) and Kani (no panics in library code). These cover the engine's core invariants — not a claim about the full system. I also built MCPSEC, a vendor-neutral benchmark for MCP gateways — 10 properties, 64 attack tests, 12 attack classes. Apache-2.0 licensed, runnable against any gateway: https://github.com/vellaveto/vellaveto/tree/main/mcpsec To be clear about what this doesn't solve: MCP's fundamental problem is that control and data share the same channel. No proxy fully fixes that. VellaVeto is a defense-in-depth layer — it catches a meaningful class of attacks at the tool-call boundary, but it's not a silver bullet against prompt injection. Licensing: core is MPL-2.0 (open source). Enterprise crates are source-available under BUSL-1.1, free for deployments under 3 nodes / 25 endpoints, and each version converts to MPL-2.0 after 3 years. Would love feedback on the approach, the benchmark methodology, or the threat model.