SpecfirstMonad ERC-4626 board

All vaults

Partly checked

0xab3CB7b3b28366eD7f6C59DbD2D708890919B289

0xab3CB7b3b28366eD7f6C59DbD2D708890919B289Monad mainnet

16 of 30 properties passed and none failed at block 111,262,020. 14 could not be exercised.

Found by the watcher at its first Deposit event in block 111,101,834, 2026-10-06 17:52 UTC. No factory the watcher follows announced it. It was not on the hand-made list the board started from.

bit 0, asset: pass0bit 1, totalAssets: pass1bit 2, convertToShares: pass2bit 3, convertToAssets: pass3bit 4, maxDeposit: pass4bit 5, previewDeposit: pass5bit 6, deposit: pass6bit 7, maxMint: pass7bit 8, previewMint: pass8bit 9, mint: pass9bit 10, maxWithdraw: pass10bit 11, previewWithdraw: inconclusive11bit 12, withdraw: inconclusive12bit 13, withdraw-zero-allowance: pass13bit 14, maxRedeem: pass14bit 15, previewRedeem: inconclusive15bit 16, redeem: inconclusive16bit 17, redeem-zero-allowance: pass17bit 18, RT-deposit-redeem: inconclusive18bit 19, RT-deposit-withdraw: inconclusive19bit 20, RT-redeem-deposit: inconclusive20bit 21, RT-redeem-mint: inconclusive21bit 22, RT-mint-withdraw: inconclusive22bit 23, RT-mint-redeem: inconclusive23bit 24, RT-withdraw-mint: inconclusive24bit 25, RT-withdraw-deposit: inconclusive25bit 26, sf-maxDeposit-honored: pass26bit 27, sf-maxMint-honored: pass27bit 28, sf-maxWithdraw-honored: inconclusive28bit 29, sf-maxRedeem-honored: inconclusive29a16z/erc4626-testsSpecfirst

Request a re-checkRuns the same 30 properties at the latest block and attests the new report.

What the watcher saw

Every event the watcher recorded for this vault, newest first. Each check is a statement about one block; a re-check with the same outcome is recorded here without a new attestation.

  1. Recovered
    Spec mismatchPartly checked

    14 pass, 2 fail, 14 inconclusive, 0 not applicable before; 16 pass, 0 fail, 14 inconclusive, 0 not applicable now.

    No longer failing: sf-maxDeposit-honored, sf-maxMint-honored

  2. Checked
    Partly checked

    16 pass, 0 fail, 14 inconclusive, 0 not applicable at block 111,262,020, 2 min. Report

    Why: backfill scan.

  3. Queued

    Waiting for a check: backfill scan.

  4. Checked
    Partly checked

    16 pass, 0 fail, 14 inconclusive, 0 not applicable at block 111,224,893, 4 min. Report

    Why: backfill scan.

  5. First result
    Spec mismatch

    14 pass, 2 fail, 14 inconclusive, 0 not applicable.

    Now failing: sf-maxDeposit-honored, sf-maxMint-honored

  6. Checked
    Spec mismatch

    14 pass, 2 fail, 14 inconclusive, 0 not applicable at block 111,196,887, 3 min. Report

    Why: first Deposit event from an unknown address.

  7. Queued

    Waiting for a check: first Deposit event from an unknown address.

  8. Checked
    Spec mismatch

    14 pass, 2 fail, 14 inconclusive, 0 not applicable at block 111,192,258, 3 min. Report

    Why: first Deposit event from an unknown address.

  9. Queued

    Waiting for a check: first Deposit event from an unknown address.

  10. Found

    First Deposit event from an unknown address in block 111,101,834 tx 0xdaae9a...333332

JSON: this vault's history

All 30 properties

In report order. Bit i is the bit the registry's passedBitmap and failedBitmap use for that property.

BitPropertyResultWhat 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)
0assettest_assetEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: asset() does not revert

1totalAssetstest_totalAssetsEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: totalAssets() does not revert

2convertToSharestest_convertToSharesEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: convertToShares gives the same result for any caller

3convertToAssetstest_convertToAssetsEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: convertToAssets gives the same result for any caller

4maxDeposittest_maxDepositEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: maxDeposit does not revert

5previewDeposittest_previewDepositEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: deposit mints at least the shares previewDeposit quoted

6deposittest_depositEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: deposit moves assets from the caller, credits shares to the receiver and spends allowance

7maxMinttest_maxMintEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: maxMint does not revert

8previewMinttest_previewMintEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: mint pulls at most the assets previewMint quoted

9minttest_mintEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: mint moves assets from the caller, credits shares to the receiver and spends allowance

10maxWithdrawtest_maxWithdrawEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: maxWithdraw does not revert

11previewWithdrawtest_previewWithdrawEIP-4626 MUSTInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw burns at most the shares previewWithdraw quoted

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
12withdrawtest_withdrawEIP-4626 MUSTInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2427 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw burns owner shares, pays the receiver and spends share allowance

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2427 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
13withdraw-zero-allowancetest_withdraw_zero_allowanceEIP-4626 SHOULDPass

No counterexample in 16 fuzz runs at this block.

Checks: withdraw on behalf of an owner without allowance reverts

14maxRedeemtest_maxRedeemEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block.

Checks: maxRedeem does not revert

15previewRedeemtest_previewRedeemEIP-4626 MUSTInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem pays at least the assets previewRedeem quoted

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
16redeemtest_redeemEIP-4626 MUSTInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2427 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem burns owner shares, pays the receiver and spends share allowance

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2427 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
17redeem-zero-allowancetest_redeem_zero_allowanceEIP-4626 SHOULDPass

No counterexample in 16 fuzz runs at this block.

Checks: redeem on behalf of an owner without allowance reverts

18RT-deposit-redeemtest_RT_deposit_redeemEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem(deposit(a)) returns no more than a

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
19RT-deposit-withdrawtest_RT_deposit_withdrawEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw(a) burns at least the shares deposit(a) minted

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
20RT-redeem-deposittest_RT_redeem_depositEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: deposit(redeem(s)) mints no more than s

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
21RT-redeem-minttest_RT_redeem_mintEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: mint(s) costs at least the assets redeem(s) paid

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
22RT-mint-withdrawtest_RT_mint_withdrawEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: withdraw(mint(s)) burns at least s shares

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
23RT-mint-redeemtest_RT_mint_redeemEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: redeem(s) pays no more than mint(s) cost

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
24RT-withdraw-minttest_RT_withdraw_mintEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: mint(withdraw(a)) costs at least a

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
25RT-withdraw-deposittest_RT_withdraw_depositEIP-4626 SHOULDInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs. Along the way deposit reverted 2478 times at amounts up to maxDeposit; some of these may be tiny amounts that round to zero shares, which many vaults reject. Those inputs were discarded, as upstream does, so this stays inconclusive; whether deposit honors maxDeposit is judged by sf-maxDeposit-honored.

Checks: deposit(a) mints no more than the shares withdraw(a) burned

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed); deposit reverted below maxDeposit 2478 times (inputs discarded, EIP-4626 says it must not revert)
runs: 0
Specfirst max-honored properties, MIT, each on one EIP-4626 MUST sentence about a max function
26sf-maxDeposit-honoredtest_sf_maxDeposit_honoredEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block. 10 amounts below the bound were refused; the bound itself was accepted.

Checks: deposit goes through up to min(maxDeposit, 1e6 tokens); when a smaller amount is refused the bound must go through, and refusals are counted (EIP-4626: maxDeposit MUST NOT be higher than what deposit accepts)

27sf-maxMint-honoredtest_sf_maxMint_honoredEIP-4626 MUSTPass

No counterexample in 16 fuzz runs at this block. 18 amounts below the bound were refused; the bound itself was accepted.

Checks: mint goes through up to min(maxMint, shares of 1e6 tokens); when a smaller amount is refused the bound must go through, and refusals are counted (EIP-4626: maxMint MUST NOT be higher than what mint accepts)

28sf-maxWithdraw-honoredtest_sf_maxWithdraw_honoredEIP-4626 MUSTInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs.

Checks: withdraw goes through up to maxWithdraw; when a smaller amount is refused maxWithdraw must go through, and refusals are counted (EIP-4626: maxWithdraw MUST NOT be higher than what withdraw accepts, and MUST be 0 when withdrawals are disabled)

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed)
runs: 0
29sf-maxRedeem-honoredtest_sf_maxRedeem_honoredEIP-4626 MUSTInconclusive

Never exercised: the vault rejected nearly every amount the fuzzer tried, and forge gave up after 4096 discarded inputs.

Checks: redeem goes through up to maxRedeem; when a smaller amount is refused maxRedeem must go through, and refusals are counted (EIP-4626: maxRedeem MUST NOT be higher than what redeem accepts, and MUST be 0 when redemptions are disabled)

Raw result
reason: `vm.assume` rejected too many inputs (4096 allowed)
runs: 0