Policy-first · Verified semantics · Multi-chain

Safe execution
for onchain agents.

Envoy gives AI agents controlled wallet access, simulation-aware protocol actions, and blockchain-native tools across Tezos, Solana, Etherlink, and EVM. The wedge is not more connectors. It is policy and wallet control that can survive production.

Not another toolkit. A control plane for agent wallets.
Most adjacent products sell wallet infrastructure, generic MCP breadth, or broad agent tooling. Envoy is sharper: policy-first wallet control, simulation-aware execution, and a path to higher-assurance policy enforcement. It is built for teams putting real agents in front of real wallets and real protocol actions.
Without a control plane
The agent has keys, broad tools, and a prompt. It can transfer, swap, stake, or route through MCP tools faster than a human can react. When it is wrong, the mistake is already onchain.
With Envoy: rejected before signing — policy violation, delegated-scope mismatch, or failed simulation.
“Envoy sits between agent intent and chain execution.”
Policy and wallet control for AI agents.
🛡
Policy-first execution
Limits, allowlists, delegated scope, and fail-closed rejection semantics sit in front of every onchain action instead of being buried in prompts.
🔐
Wallet-control native
Designed for server wallets, delegated sessions, and governed execution rather than raw signer access with a nicer wrapper.
Simulation-aware protocol actions
Vault previews, protocol guards, and state-aware preflight checks help stop unsafe DeFi actions before they become writes.
Blockchain-native MCP
Expose onchain tools with typed inputs, normalized errors, and chain-aware control boundaries instead of generic connector sprawl.
Multi-chain adapters
Tezos, Etherlink, Solana, and EVM adapters stay isolated underneath one control surface, so safety logic is not scattered per chain.
🧾
Decision-grade audit trail
Every allowed or blocked action yields machine-readable reasons, which is what operators actually need for trust, review, and debugging.
Tezosstable
Etherlinkstable
Solanastable
EVMstable
Policy and execution in one surface.
# Install npm install @envoy/core @envoy/tezos # policy.yaml version: 1 limits: daily_max_xtz: 500 per_tx_max_xtz: 100 allowlist: - tz1ops... - tz1treasury... audit: true # agent.ts import { TezosAdapter } from '@envoy/tezos' import { PolicyEngine } from '@envoy/core' const agent = new PolicyEngine({ adapter: new TezosAdapter({ rpc: 'https://rpc.tezos.example' }), policy: './policy.yaml' }) await agent.transfer({ to: 'tz1ops...', amount: 100 }) // ✓ allowed await agent.transfer({ to: 'tz1unknown', amount: 50000 }) // ✗ blocked before signing
A policy layer you can reason about.
Envoy’s policy semantics are the right place to invest in formal methods because they are stable, declarative, and central to the product wedge. The current direction assumes Quint-modeled semantics, conformance testing between model and runtime, and a longer-term path to a narrow high-assurance policy kernel.
Quint-modeled semantics
Critical properties such as fail-closed evaluation and non-escalation can be checked explicitly instead of being left as prompt discipline.
Runtime conformance tests
Generated traces are replayed against the implementation so the TypeScript runtime stays aligned with the modeled policy behavior.
Narrower, stronger claim
The promise is verified policy for onchain agents, not a vague claim that every adapter and protocol integration is fully proven.
The claim is narrow on purpose: verified policy, governed execution, and a safer path from agent intent to chain action.
From modeled policy to deeper assurance.
The near-term path is practical: keep the runtime in TypeScript, keep the control plane usable, and harden policy semantics with modeling and conformance tests. The longer-term path is narrower and higher-assurance: move the policy kernel toward a Rust/WASM boundary and explore Lean or Rocq only where theorem-level guarantees are worth the cost.
1
Now
Policy-first wallet control, blockchain-native MCP tooling, and simulation-aware protocol actions.
2
Next
Expand Quint-modeled semantics and trace replay so implementation and spec stay aligned as the surface grows.
3
Later
Move the policy kernel toward Rust/WASM and explore Lean or Rocq for narrower proof-oriented work where stronger guarantees matter.
Interactive Terminal
See the control plane the way an operator would.
The terminal below is not the homepage anymore. It is the interactive product artifact inside the page: blocked actions, allowed actions, policy checks, and guided commands that make the execution model tangible.
envoy@sdk: ~
envoy@sdk:~$
envoy@sdk:~$