All vaults / Euler EVK (eVault)
EVK Vault eWMON-9
All 30 properties passed at block 109,195,820. No counterexample was found; that is evidence, not a safety guarantee.
Known to the watcher from a backfill scan in block 109,195,820, 2026-09-30 09:50 UTC.
Request a re-checkRuns the same 30 properties at the latest block and attests the new report.
All 30 properties
In report order. Bit i is the bit the registry's passedBitmap and failedBitmap use for that property.
| Bit | Property | Result | What was found |
|---|---|---|---|
| a16z/erc4626-tests at ac48546, 26 properties: 16 on EIP-4626 MUST sentences, 10 on SHOULD guidance (the round trips and the allowance checks) | |||
| 0 | assettest_assetEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: asset() does not revert |
| 1 | totalAssetstest_totalAssetsEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: totalAssets() does not revert |
| 2 | convertToSharestest_convertToSharesEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: convertToShares gives the same result for any caller |
| 3 | convertToAssetstest_convertToAssetsEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: convertToAssets gives the same result for any caller |
| 4 | maxDeposittest_maxDepositEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: maxDeposit does not revert |
| 5 | previewDeposittest_previewDepositEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: deposit mints at least the shares previewDeposit quoted |
| 6 | deposittest_depositEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: deposit moves assets from the caller, credits shares to the receiver and spends allowance |
| 7 | maxMinttest_maxMintEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: maxMint does not revert |
| 8 | previewMinttest_previewMintEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: mint pulls at most the assets previewMint quoted |
| 9 | minttest_mintEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: mint moves assets from the caller, credits shares to the receiver and spends allowance |
| 10 | maxWithdrawtest_maxWithdrawEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: maxWithdraw does not revert |
| 11 | previewWithdrawtest_previewWithdrawEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: withdraw burns at most the shares previewWithdraw quoted |
| 12 | withdrawtest_withdrawEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: withdraw burns owner shares, pays the receiver and spends share allowance |
| 13 | withdraw-zero-allowancetest_withdraw_zero_allowanceEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: withdraw on behalf of an owner without allowance reverts |
| 14 | maxRedeemtest_maxRedeemEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: maxRedeem does not revert |
| 15 | previewRedeemtest_previewRedeemEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: redeem pays at least the assets previewRedeem quoted |
| 16 | redeemtest_redeemEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: redeem burns owner shares, pays the receiver and spends share allowance |
| 17 | redeem-zero-allowancetest_redeem_zero_allowanceEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: redeem on behalf of an owner without allowance reverts |
| 18 | RT-deposit-redeemtest_RT_deposit_redeemEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: redeem(deposit(a)) returns no more than a |
| 19 | RT-deposit-withdrawtest_RT_deposit_withdrawEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: withdraw(a) burns at least the shares deposit(a) minted |
| 20 | RT-redeem-deposittest_RT_redeem_depositEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: deposit(redeem(s)) mints no more than s |
| 21 | RT-redeem-minttest_RT_redeem_mintEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: mint(s) costs at least the assets redeem(s) paid |
| 22 | RT-mint-withdrawtest_RT_mint_withdrawEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: withdraw(mint(s)) burns at least s shares |
| 23 | RT-mint-redeemtest_RT_mint_redeemEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: redeem(s) pays no more than mint(s) cost |
| 24 | RT-withdraw-minttest_RT_withdraw_mintEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: mint(withdraw(a)) costs at least a |
| 25 | RT-withdraw-deposittest_RT_withdraw_depositEIP-4626 SHOULD | Pass | No counterexample in 16 fuzz runs at this block. Checks: deposit(a) mints no more than the shares withdraw(a) burned |
| Specfirst max-honored properties, MIT, each on one EIP-4626 MUST sentence about a max function | |||
| 26 | sf-maxDeposit-honoredtest_sf_maxDeposit_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: deposit does not revert for amounts up to maxDeposit (EIP-4626: maxDeposit is the most deposit accepts without reverting) |
| 27 | sf-maxMint-honoredtest_sf_maxMint_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: mint does not revert for shares up to maxMint (EIP-4626: maxMint is the most mint accepts without reverting) |
| 28 | sf-maxWithdraw-honoredtest_sf_maxWithdraw_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: withdraw does not revert for assets up to maxWithdraw (EIP-4626: maxWithdraw MUST return 0 when withdrawals are disabled) |
| 29 | sf-maxRedeem-honoredtest_sf_maxRedeem_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. Checks: redeem does not revert for shares up to maxRedeem (EIP-4626: maxRedeem MUST return 0 when redemptions are disabled) |