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
| Name | Required | Description | Default |
|---|---|---|---|
| max_assets | No | ||
| max_shares | No | ||
| paymentHeader | No | x402 Base64 or JSON payment authorization string (if not in _meta.x402Payment) | |
| redeem_fn_code | Yes | Python snippet or AST defining preview_redeem(shares, total_assets, total_shares) | |
| deposit_fn_code | Yes | Python snippet or AST defining preview_deposit(deposit, total_assets, total_shares) | |
| check_zero_share_mint | No |