Method, limits, and why we say spec mismatch

Properties nobody wrote for themselves

A certificate built on the deployer's own spec proves only that the code agrees with its author. This board uses properties that neither the vault teams nor Specfirst chose for the occasion. 26 come from a16z/erc4626-tests, pinned to one commit and fetched at run time. They cover the view functions, the preview functions against the real calls, allowances and round trips such as redeem after deposit.

Specfirst adds 4 properties of its own, one EIP-4626 sentence each. For maxDeposit, maxMint, maxWithdraw and maxRedeem the standard says the value MUST be the most the matching call accepts without reverting, and MUST be 0 while the action is disabled. The upstream suite discards any input whose call reverts, so a vault whose withdraw always reverts never fails there; it only runs out of inputs. The max-honored properties call deposit, mint, withdraw or redeem directly with an amount at or below the advertised max, then at the bound itself (the max, or one million whole tokens for deposit and mint when the max is larger). They fail when the call at the bound reverts; refusals of smaller amounts are counted beside the verdict. Their source is in the Specfirst repository and its hash is in every report.

How a check runs

• Each vault is forked at one block, 109,195,820 for this board. forge runs with a recorded seed and a fresh random sender, so a vault cannot recognise forge's default address.
• Test users come from a pool of 16 addresses derived from the seed. The seed changes per run, so a vault cannot special-case them in advance.
• Amounts are bounded by the smaller of the vault's maxDeposit and one million whole tokens. No synthetic yield is added: the vault's own share price at the block is what gets tested.
• Balances are written with forge-std's deal, with a packed-slot fallback for tokens such as Monad's AUSD. When no slot can be written, the property is inconclusive.
• forge gives up on a property after 4,096 rejected inputs. A property that never got a usable input is inconclusive, never a pass.
• Positive control: the same harness runs against BrokenVault, whose previewDeposit promises 1% more shares than deposit mints. previewDeposit fails there and the other 25 upstream properties pass. A harness that could not catch it would make every pass on this board meaningless.
• Vaults that share an implementation key ran the same code: the implementation behind a proxy when there is one, compared with compiler metadata and with immutables masked. They count once in the implementation total.

What each result means

• Pass: no counterexample in the recorded number of fuzz runs, at that block, for that suite.
• Fail: forge found a concrete input that breaks the property. The report keeps the failing call.
• Inconclusive: the property could not be exercised, because the vault rejected the amounts, test users could not be funded, the RPC failed, or every input needed a Monad precompile the fork does not have. Only a pass counts as verified, so imitating one of these messages gains a vault nothing.
• Not applicable: the suite cannot run on this contract. ERC-7575 vaults keep shares in a separate token, ERC-7535 vaults hold the native coin, some assets only move between allowlisted parties, and a max of 0 for every user leaves nothing to honor.

Limits

• One point in time. State, parameters and proxy implementations change after the block; a later check can come out differently.
• A pass is not an audit and not a safety guarantee. Bugs that need larger amounts, more users, a price change or a specific address are out of reach.
• Masking every PUSH32 immediate also masks real constants, so two contracts that differ only in such a constant are grouped as one implementation.
• forge pranks test users, which changes msg.sender but not tx.origin. A vault that branches on tx.origin can behave differently under the harness.
• Public RPCs rate-limit. Properties that ended on an RPC error say nothing about the vault and should be rerun.
• forge has none of Monad's own precompiles (staking at 0x1000, the reserve balance check at 0x1001, P256 at 0x0100). An input whose vault call reaches one of them and reverts, such as a deposit into a liquid staking vault that stakes it, is not judged, since the fork cannot tell whether the revert needed the precompile's answer. A property with such an input never passes: it fails when another input failed, otherwise it is inconclusive. Calls that reach a precompile and go through are judged as usual.

Why we call them spec mismatches

A failed max-honored property shows a vault whose own numbers disagree with its own behavior: maxWithdraw reports a balance and withdraw reverts, or withdrawals are paused while the max is not 0. EIP-4626 is explicit that this is not allowed. That is what the board reports, and it stops there.

It is not a vulnerability claim. The vault may be working exactly as its authors intend, for example with exits that go through a request queue instead of withdraw. No loss of funds follows from the mismatch itself. What breaks is the promise other software relies on: aggregators, routers and wallets that read maxWithdraw before building a transaction get a revert the standard says cannot happen.

MUST and SHOULD

Not every property checks a MUST. The eight round trips of the upstream suite check EIP-4626's rounding guidance in Security Considerations: rounding should favor the vault over its users. That is a SHOULD. When every failure of a vault is a round trip off by at most 2 base units or 1 basis point of the amount, often a base unit in the caller's favor through a wrapped asset, the board shows "Rounding favors caller" instead of a spec mismatch. A round trip off by more, or by an amount the report does not give, is still a SHOULD but keeps the spec mismatch chip and says by how much: that is a conversion that is wrong, not rounding.

Withdraw and redeem only SHOULD check that the caller may spend the owner's shares, so the two zero-allowance properties are SHOULDs. A failure of the withdraw or redeem property itself counts as a MUST whatever its reason says, because the reason text can come from the vault; a vault that only skips the allowance check shows up in the zero-allowance properties. A round trip is judged by every pair of values in its logs, so values a vault writes there can only make the verdict stricter. Allowance failures keep the spec mismatch chip, because the sentence names what went through. Every failure is shown with its level, and any failed MUST makes the vault a spec mismatch.

Onchain attestations

Results are recorded on Monad testnet in CheckAttestationRegistry 0x3754918bBB8481D046D80718a9efe434e353daF7, keyed by chain, vault and standard (standardId 0x45f39c8c7e3105201fd8b1288ac068347728af9cfd16f3f08e97171ef955c9ab, keccak256 of "erc4626"). An attestation stores the block, the implementation key, the code hash, the suite hash, the report hash, the four counts and one bitmap each for passes and fails.

isCompliant is true only when the latest attestation is valid, has at least one pass and no fail, inconclusive or not applicable result. It repeats the check result; it does not make the vault safe, it says nothing about another block, and the registry cannot read Monad mainnet, so the code hash and implementation key are the issuer's statement until someone repeats the check.

Check it yourself

Every vault page lists the exact command with the recorded block, runs and seed, and links the report file. Its reportHash is keccak256 of the report's RFC 8785 canonical JSON; recompute it and compare with the attestation. Python's json.dumps needs ensure_ascii=False to match.