How does Provely guard an MCP server that nobody compiled?

Provely guards any MCP server on the day you connect it. A call that no person confirmed never reaches the provider. A guarded call still proves no outcome: an uncompiled provider answers UNVERIFIABLE, and only a compiled integration reaches VERIFIED.

Read the two facts together. The first fact says what you get with no compiler run. The second fact says what a compiler run adds. A page that stated one of them alone would sell a permission control as a proof of an outcome.

The SDK reads the tool declarations of the server. It derives a permission envelope from those declarations and from the input that a person confirmed. A call that the confirmed plan does not name is refused before the provider is reached.

What does Provely guard on the day you connect a server?

Every call that passes through the wrapped client. The Model Context Protocol answers a tool catalogue under tools/list. Provely reads that catalogue, and it derives the envelope from it. The derivation runs on connection, for any server.

• No compiler run happens. The envelope needs no signed skill.
• No language model call happens. The derivation reads no prose.
• Every bound comes from a declaration that the server published.
• A value bound comes from an input that a person confirmed.
• Provely closes every derived schema with additionalProperties: false.
• The envelope records the hash of the declarations and the hash of the confirmed input.

A published tool schema usually states no additionalProperties. An extra member then passes a plain check, and a compromised server smuggles a payload in a member that no person read. The closed schema refuses that member.

A confirmed plan is an allow list, not a checklist. A checklist asks whether the authorised steps happened. An allow list also refuses every other call. A skill that does the authorised work and one extra call is stopped at the extra call.

Which calls does the envelope refuse?

Provely compares the call with the envelope before it reaches the server. The comparison is an operator over two documents. It reads no text as an instruction, and it asks no language model. A schema that the checker cannot evaluate refuses the call, so the check fails closed.

A refusal happens before the provider call, and never after it. A verdict after the fact is honest, and the money has already moved.

Why is a guarded call not a verified outcome?

A tool declaration states the shape of a call. It never states what "done" means. The declaration says that a call takes an object and answers an object. It says nothing about the state of the money.

That semantic comes from provider documents, and a conformance run proves it. A contract derived from a tool schema could assert only "the tool answered". That claim is an E1 acknowledgement. Safety rule 5 forbids an acknowledgement as terminal success, so Provely refuses to write such a contract.

An uncompiled provider answers UNVERIFIABLE, with the reason outcome_not_compiled. That answer is safety rule 2 working, and it is not a gap. Read the UNVERIFIABLE definition and what each verdict obliges an agent to do.

Provely publishes 16 compiled integrations today. Each one states its completion levels, its certification, and its last conformance run. Read the compiled integrations.

A guarded call never answers VERIFIED. Never present the guarded answer as a completed business outcome.

Why does the verifier not read the provider through your MCP server?

An MCP server is a transport. It is not an evidence channel. A verifier that reads a provider through the server that the agent used is no longer independent of the action path.

The evidence hierarchy rests on that independence. E2 means a provider readback that the verifier made itself. A reading that the action path returns is E1 at best. A compromised server that reports a success it never performed would then also supply the evidence for it, and the verdict would be a false VERIFIED.

1. You give the verifier its own connection to the provider.
2. Make that credential read only, where the provider permits it.
3. The verifier calls the provider directly, and never through the server of the agent.
4. A provider that offers the verifier no direct read has no E2 channel, and the answer is UNVERIFIABLE.

Never give an MCP server the credentials of the verifier. A hop on the action path is never new evidence. Read the evidence level definition.

What does the envelope not cover?

Three limits. Read each one before you trust the control, because none of them is small.

Provely contains the consequence of an attack. It does not read a prompt, and it does not judge the reason for an action. The contract states what a person authorised, and the evidence states what happened.

How do you wrap a server?

import { createToolGuard, deriveEnvelope, guardMcpClient, Provely } from '@provely/sdk';

const provely = new Provely();

// The declarations of the server. Provely reads them, and it reads no prose.
const declared = await client.listTools();

const envelope = deriveEnvelope({
  source: 'payments-mcp',
  tools: declared.tools,
  // The input that the person confirmed. Each name bounds the argument of that name.
  confirmed: { charge: 'ch_1001', amount: 500 },
});

// Every argument that no confirmed value bounds. A person reads each one.
for (const part of envelope.review) console.log(part.reason);

const guard = createToolGuard(provely, { policy: envelope.policy });
// The same client, with the one member replaced. The agent code does not change.
const guarded = guardMcpClient(guard, client);

The wrapper reads the tool name from each call. One guard therefore covers every tool of the server, including a tool that the server added after the process started.

Provely also publishes its own MCP server, with the four tools begin, verify, status, and receipt. That server is not the subject of this page. Read the Provely MCP server documentation.