0xB4641064f64E2F3aAffc1b4b4A66BE75c1C81408
Rounding favors the caller: 2 round-trip properties fail EIP-4626's SHOULD guidance (Security Considerations) at block 111,263,642, by at most 14,626 base units, <0.01% of the amount; no MUST sentence failed.
Known to the watcher from a backfill scan in block 111,041,054, 2026-10-06 12:43 UTC. First deposit seen in block 110,391,946. It was not on the hand-made list the board started from.
Request a re-checkRuns the same 30 properties at the latest block and attests the new report.
What failed
- RT-redeem-depositEIP-4626 SHOULD
Forge found a counterexample: the round trip ended 14,626 base units in the caller's favor (144,907,523,788,424,795 against 144,907,523,788,410,169).
EIP-4626, Security Considerations: rounding should favor the Vault over its users. That is a SHOULD, not a MUST.
Counterexample:
test_RT_redeem_deposit(([0xb81AEf6fd0631D46eb2febFB061e28079968217b, 0x42047e2bc46C9B21026dC1b7f1bcAfCF3d3C99AB, 0x3fD3C599cB6FAa8fc9457204Ef893BF4fe6b98Be, 0x7E70E65b65D7b49E56f543fc8A31dA5c9B87c9c8], [2, 1369157656841231102401257108935390574257794187020225218071974, 144560500807202019203179602574849247868030344220393522583604737, 41910795479], [6254005027521821681153520687112290221130091716374014238787741697417431949, 30191631338, 25238745865040887575332761391163240387629431405940905293927847, 138924220326931133773093813917949229112272586832910858070047], 215578705186788578543004377382873), 50288063115144969489) - RT-withdraw-depositEIP-4626 SHOULD
Forge found a counterexample: the round trip ended 5,209 base units in the caller's favor (56,500,900 against 56,495,691).
EIP-4626, Security Considerations: rounding should favor the Vault over its users. That is a SHOULD, not a MUST.
Counterexample:
test_RT_withdraw_deposit(([0x00000000000000000000000000000000000020ae, 0x00000000000000000000000000000000000051EC, 0x0000000000000000000000000000000000003889, 0x0000000000000000000000000000000000004313], [143, 3, 143, 10143], [4921, 65535, 2837, 65535], 6611), 801644042)
Each round trip shown went in the caller's favor by the amount in its counterexample, against EIP-4626's guidance that rounding should favor the vault. That guidance is a SHOULD; no MUST sentence failed, and it is not a claim that funds are at risk.
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.
- RegressedSpec mismatchRounding favors caller
27 pass, 3 fail, 0 inconclusive, 0 not applicable before; 28 pass, 2 fail, 0 inconclusive, 0 not applicable now.
Now failing: RT-redeem-deposit
No longer failing: sf-maxDeposit-honored, sf-maxMint-honored
- Attested
Attestation #24 on Monad testnet tx 0x4719bd...54a2ba
- CheckedRounding favors caller
28 pass, 2 fail, 0 inconclusive, 0 not applicable at block 111,263,642, 1 min. Report
Why: backfill scan.
- Queued
Waiting for a check: backfill scan.
- CheckedRounding favors caller
28 pass, 2 fail, 0 inconclusive, 0 not applicable at block 111,262,847, 1 min. Report
Why: backfill scan.
- Queued
Waiting for a check: backfill scan.
- CheckedRounding favors caller
27 pass, 3 fail, 0 inconclusive, 0 not applicable at block 111,224,893, 2 min. Report
Why: backfill scan.
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.
| 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 | Fail | Forge found a counterexample: the round trip ended 14,626 base units in the caller's favor (144,907,523,788,424,795 against 144,907,523,788,410,169). EIP-4626, Security Considerations: rounding should favor the Vault over its users. That is a SHOULD, not a MUST. Checks: deposit(redeem(s)) mints no more than s Raw resultreason: Error: a <=~ b not satisfied [uint]; deposit reverted below maxDeposit 2 times (inputs discarded, EIP-4626 says it must not revert) runs: 9 call: test_RT_redeem_deposit(([0xb81AEf6fd0631D46eb2febFB061e28079968217b, 0x42047e2bc46C9B21026dC1b7f1bcAfCF3d3C99AB, 0x3fD3C599cB6FAa8fc9457204Ef893BF4fe6b98Be, 0x7E70E65b65D7b49E56f543fc8A31dA5c9B87c9c8], [2, 1369157656841231102401257108935390574257794187020225218071974, 144560500807202019203179602574849247868030344220393522583604737, 41910795479], [6254005027521821681153520687112290221130091716374014238787741697417431949, 30191631338, 25238745865040887575332761391163240387629431405940905293927847, 138924220326931133773093813917949229112272586832910858070047], 215578705186788578543004377382873), 50288063115144969489) calldata: 0x37bad155000000000000000000000000b81aef6fd0631d46eb2febfb061e28079968217b00000000000000000000000042047e2bc46c9b21026dc1b7f1bcafcf3d3c99ab0000000000000000000000003fd3c599cb6faa8fc9457204ef893bf4fe6b98be0000000000000000000000007e70e65b65d7b49e56f543fc8a31da5c9b87c9c8000000000000000000000000000000000000000000000000000000000000000200000000000000da1e90ebc1fcc07e17195cf497a99c924680fc24b142b7cda600000000000059f5d102e6be7182e6017fe7431a441e681c6effc73ab9848e0100000000000000000000000000000000000000000000000000000009c213fcd700038a25f06bd0de5ec9da8a431161fafc5f665fd2a3f52cc82a4369130c4b8d00000000000000000000000000000000000000000000000000000007078fbbea0000000000000fb4c3a1db110d51fd63f6c17369915193272242ce0db75455a7000000000000001621c489778664490c3ea09f95709b5b09afae5561e774281f0000000000000000000000000000000000000aa0fc5d68e869b9bc3708437fd9000000000000000000000000000000000000000000000002b9e316f734a3bd11 log: Error: a <=~ b not satisfied [uint] log: Value a: 144907523788424795 log: Value b: 144907523788410169 log: Max Delta: 0 log: Delta: 14626 |
| 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 | Fail | Forge found a counterexample: the round trip ended 5,209 base units in the caller's favor (56,500,900 against 56,495,691). EIP-4626, Security Considerations: rounding should favor the Vault over its users. That is a SHOULD, not a MUST. Checks: deposit(a) mints no more than the shares withdraw(a) burned Raw resultreason: Error: a <=~ b not satisfied [uint]; deposit reverted below maxDeposit 1 times (inputs discarded, EIP-4626 says it must not revert) runs: 4 call: test_RT_withdraw_deposit(([0x00000000000000000000000000000000000020ae, 0x00000000000000000000000000000000000051EC, 0x0000000000000000000000000000000000003889, 0x0000000000000000000000000000000000004313], [143, 3, 143, 10143], [4921, 65535, 2837, 65535], 6611), 801644042) calldata: 0xfbdc418900000000000000000000000000000000000000000000000000000000000020ae00000000000000000000000000000000000000000000000000000000000051ec00000000000000000000000000000000000000000000000000000000000038890000000000000000000000000000000000000000000000000000000000004313000000000000000000000000000000000000000000000000000000000000008f0000000000000000000000000000000000000000000000000000000000000003000000000000000000000000000000000000000000000000000000000000008f000000000000000000000000000000000000000000000000000000000000279f0000000000000000000000000000000000000000000000000000000000001339000000000000000000000000000000000000000000000000000000000000ffff0000000000000000000000000000000000000000000000000000000000000b15000000000000000000000000000000000000000000000000000000000000ffff00000000000000000000000000000000000000000000000000000000000019d3000000000000000000000000000000000000000000000000000000002fc81e0a log: Error: a <=~ b not satisfied [uint] log: Value a: 56500900 log: Value b: 56495691 log: Max Delta: 0 log: Delta: 5209 |
| 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. 1 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) |
| 27 | sf-maxMint-honoredtest_sf_maxMint_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. 19 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) |
| 28 | sf-maxWithdraw-honoredtest_sf_maxWithdraw_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. 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) |
| 29 | sf-maxRedeem-honoredtest_sf_maxRedeem_honoredEIP-4626 MUST | Pass | No counterexample in 16 fuzz runs at this block. 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) |