Skip to main content
Glama

x402_verify_vault_rounding

Formally verify ERC-4626, Euler, and Meteora vault share rounding, donation attacks, and zero-share inflation by analyzing deposit and redeem functions with Z3.

Instructions

Paid tool (20000 Base USDC atomic): Formal Z3 verification of ERC-4626 / Euler / Meteora vault share rounding, donation attacks, and zero-share inflation vulnerabilities.

Input Schema

NameRequiredDescriptionDefault
max_assetsNo
max_sharesNo
paymentHeaderNox402 Base64 or JSON payment authorization string (if not in _meta.x402Payment)
redeem_fn_codeYesPython snippet or AST defining preview_redeem(shares, total_assets, total_shares)
deposit_fn_codeYesPython snippet or AST defining preview_deposit(deposit, total_assets, total_shares)
check_zero_share_mintNo

Schema Changelog

Changes observed during successful MCP inspections.

  1. First observedv1.0.0

TDQS

C2.8/5.0
Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries the full disclosure burden, and it does add one valuable fact: this is a paid tool costing 20000 Base USDC atomic units, plus that verification is formal (Z3). It omits critical behavior – whether payment failure blocks execution, whether the operation is read-only, how long verification takes, and whether the tool ever mutates anything.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness4/5

Is the description appropriately sized, front-loaded, and free of redundancy?

A single tight sentence with the cost front-loaded and the subject matter immediately following. No filler or redundant restatement of the name, though it is arguably too terse for the tool's complexity.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness3/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

For a paid formal-verification tool with no output schema and no annotations, the definition leaves the agent uncertain about the shape of the result (verdict? counterexample?), payment-failure behavior, and the semantics of the bound parameters. The price disclosure and named vulnerability classes cover the essentials of what the tool does but not enough to call it confidently.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters2/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is only 50%: max_assets, max_shares, and check_zero_share_mint have no schema descriptions, and the description does not explain that they act as search bounds or that check_zero_share_mint toggles the zero-share inflation check it names. Only the zero-share vulnerability mention loosely hints at one undocumented parameter.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description names a specific verb and resource ('Formal Z3 verification of vault share rounding') and scopes it to ERC-4626 / Euler / Meteora plus class of vulnerability (donation attacks, zero-share inflation). That makes it clearly distinguishable from the sibling verifiers (polymarket basket, zk_or_bitvec, differential_spec) by topic, though it never explicitly contrasts itself with them.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

There is no statement of when to call this versus the other x402_verify_* tools, no prerequisites beyond price, and no guidance on the required Python/AST inputs being valid preview_deposit/preview_redeem definitions. The agent must infer usage entirely from the topic sentence.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.