The vault

24 properties, run on this chain

There is no toolchain here, no testnet and no funded account. An eth_call may carry a state override, so the compiled suite is placed at a scratch address and a public Robinhood Chain node executes the whole thing — constructors, reverts, transfers and all — for free, on the same EVM the app deploys to. Last run at block 55,462,976.

24properties, every one executed and held
11deliberate defects introduced, each one confirmed caught
1of those that no property can see — only the ABI surface can
7,961bytes of creation code, from the compile that proved it

Every property

#PropertyResult
P1the first deposit mints, and redeeming it all returns exactly what went inheld
P2rounding never favours the holder, at every sizeheld
P3a stray transfer moves no price at allheld
P4the donation attack is closed by the accounting, with the offset switched off entirelyheld
P5deposit mints exactly previewDeposit, and redeem pays exactly previewRedeemheld
P6mint costs exactly previewMint, and withdraw burns exactly previewWithdrawheld
P7totalAssets tracks the accounting rather than the token balanceheld
P8a cut above the cap reverts — from the owner and from the constructor — and one at the cap is acceptedheld
P9a stranger reaches none of the three owner-only functionsheld
P10harvest charges exactly the cut on the income and no moreheld
P11accrued cut sits outside every holder's claim and survives a full exitheld
P12collect cannot move a wei more than has been accrued, and never touches principalheld
P13another holder arriving or leaving moves the share price by nothingheld
P14transferring a share moves the claim and moves no priceheld
P15a zero deposit, a zero redemption and the zero address all revertheld
P16allowance is respected, and an infinite one does not decayheld
P17everybody leaving empties the supply and strands no principalheld
P18THE FOLD IS EXACT: dust() mints zero, and one wei more mints oneheld
P19THE STEP IS EXACT: both ends of step() mint the same shares, and one wei outside each does notheld
P20foldLoss() matches a real deposit followed by a real redemption, to the weiheld
P21a larger offset strictly NARROWS the dead zoneheld
P22an offset outside the bound reverts rather than being clampedheld
P23a fee-on-transfer token credits only what actually arrivedheld
P24the ERC-4626 view surface is complete and its limits are honouredheld

Sabotage

A suite that passes is evidence of nothing until you have watched it bite

11 copies of the contract are compiled with one deliberate defect each and put through the same properties. Each must come back with a hole, and the runner names which property found it. One is expected to survive every property, and is in the file for exactly that reason: without it, a suite with one permanently-red property would appear to catch everything.

caught

totalAssets is read from the token balance

the classic donation vector, and the reason the accounting is tracked at all.

Found by P1, P3, P4, P7, P10(revert), P11(revert), P12(revert), P13, P17, P18(revert), P19(revert), P20(revert), P21(revert), P23.

caught

previewDeposit rounds up instead of down

the direction of a single floor is the whole of who absorbs the remainder. Rounded up, the depositor is issued shares worth more than they paid, and the wei comes out of everybody already in the vault.

Found by P18, P19, P20.

caught

previewRedeem rounds up instead of down

the same wei, taken on the way out. A round trip then returns more than it cost, which is a slow drain rather than a theft, and is invisible per trade.

Found by P20.

caught

dust() is off by one

the site's headline number. Off by one it is not a dead zone but a claim that the first share is free, and only a real deposit can tell the difference.

Found by P18.

caught

step() reports a half-open interval as a closed one

the missing −1 makes `hi` the first size that mints one share MORE, so the app would tell a depositor they are getting a share they are not.

Found by P19.

caught

the cut cap is removed from setCut

the cap is the only thing standing between a holder and a 100% fee on income. The constructor still checks, so a reader auditing deployment sees a capped vault.

Found by P8.

caught

collect saturates instead of reverting

asking for more than has accrued silently takes everything accrued and pushes the requested amount, which reaches principal. A revert and a clamp look the same from outside until the amount is wrong.

Found by P12.

caught

the offset bound is removed from the constructor

the app lets a deployer choose the offset. Unbounded, a large one pushes the conversion multiplications toward overflow and makes the vault unusable in a way that only shows up at size.

Found by P22.

caught

the accounting credits what was asked for, not what arrived

a fee-on-transfer token delivers less than the request. Crediting the request mints shares against assets the vault never received, and the shortfall is paid silently by everyone already in it.

Found by P23.

caught

maxRedeem reports more than the holder owns

a limit that does not match what the vault will actually do is worse than no limit: an integrator sizes a redemption on it and the transaction reverts.

Found by P24.

survives

an owner-only rescue() is added

it breaks NO property. Every invariant in the suite still holds, and the owner can take the principal. Only a mechanical read of the compiled ABI against the written-down surface can see a function that was added rather than changed.

Found by no property at all and by the ABI surface check.

The attack, four times

The offset is a second lock on a door the accounting already shut

The textbook ERC-4626 inflation attack: the attacker takes the first share for one wei, transfers a large amount straight to the vault, and the victim deposits afterwards — deliberately less than the donation. Run against Cusp and against a vault identical to it except that totalAssets() reads balanceOf, at two offsets.

AccountingOffsetVictim put inVictim can take outKept
Tracked in storage Cusp0500 tokens500.0000 tokens100.0000%
Tracked in storage Cusp6500 tokens500.0000 tokens100.0000%
Read from balanceOf0500 tokens0.0000 tokens0.0000%
Read from balanceOf6500 tokens499.9997 tokens99.9999%

The comparison vault is not a straw man built to lose: it is Cusp's arithmetic with one function changed, and its source is in contracts/Attack.sol next to the result. What the run says is that either defence alone is sufficient, and that the one with a cost — the fold — is the one that is optional.

The written-down surface

The only check that can see a function that was added

Every state-changing function the vault is allowed to expose is written down; the check is that the compiled ABI contains no others. A hand-written list of "functions the owner can call" would test the list. This is what catches an owner-only rescue(), which breaks no invariant that exists and hands the owner the principal.

  • deposit(uint256,address)
  • mint(uint256,address)
  • redeem(uint256,address,address)
  • withdraw(uint256,address,address)
  • harvest(uint256)
  • setCut(uint16)
  • collect(address,uint256)
  • transfer(address,uint256)
  • transferFrom(address,address,uint256)
  • approve(address,uint256)

Unexpected on the last run: none.

Where it runs

And what is not deployed

contract

Compiled and executed

Cusp.sol compiles with solc 0.8.26 and its properties run on Robinhood Chain's own EVM through an eth_call state override on every build. It is not deployed to a fixed address and has not been audited.

app

Deploys from your wallet

The app deploys the contract from your own address. Every write is an ordinary signed transaction; no key is handled anywhere in this repo.

measurement

Read from chain

Asset list, decimals and prices are read from Robinhood Chain with no API key and no proxy. The fold figures are computed from those.

token

Does not exist

There is no Cusp token and no contract address to copy.