The contract
32 properties, executed on Robinhood Chain
An eth_call with no to runs creation code on the real evaluator
against real chain state and returns whatever the constructor returns. No testnet, no toolchain, no funded
account, no private key — and nothing is written.
| Sabotage | What was broken | Caught by |
|---|---|---|
no-line | depositWith stops enforcing its floor | P12, P28 |
no-deadline | the deadline is not checked | P14 |
donation-priced | totalAssets reads balanceOf instead of the tracked counters | P6, P7, P24 |
credit-requested | a deposit is credited what was asked for, not what arrived | P5, P30 |
no-mutex | the reentrancy lock is removed | P23 |
line-ignores-weight | the floor is computed from the mark instead of from the share price | P28 |
swing-flat | the ladder becomes one constant tolerance for every sea | P16, P17, P18, P32 |
abandon-marked | the price-free exit starts reading the price | P21, P22 |
ship-no-floor | ship ignores the floor in its own signature | P20 |
redeem-overdraws | redeem stops checking there is cash to pay with | P9 |
allowance-burns-infinity | an infinite allowance is decremented | P3 |
mint-dilutes | mint issues the full shares for a part payment | P30 |
ship-prices-late | ship values the arriving stock at a price read after the transfer | P31 |
unbounded-ratio-reverts | the unbounded ratio reverts instead of being reported | P32 |
line-zero-when-unbounded | an unbounded exposure produces a floor of zero instead of the quote | P32 |
no-offset | the virtual share offset is removed | survives |
owner-drain | an owner-only function that empties the vault is added | survives ABI read |
A suite that bites on everything is a suite nobody has found the floor of, so two sabotages are expected to survive and each says why.
the virtual share offset is removed
tracked accounting already closes the inflation attack the offset defends against — P24 runs the attack with the offset at zero and the victim still recovers everything. Two locks on one door; this is the one with no cost.
an owner-only function that empties the vault is added
no property enumerates the ABI, so no property can see a new function. Caught by a mechanical read of the compiled interface below, and by nothing else — a hand-written list of owner functions tests the list.
And a longer test than the property suite
Each property builds one state and asserts one thing about it.
tools/fuzz.mjs does the opposite: it drives the vault through
3,360 randomised operations from several accounts — deposits, guarded
deposits, redemptions, shipping, abandoning, transfers, and moving the pool's price and its liquidity
underneath — and re-checks 9 invariants after every single one:
30,240 checks in total, on this chain's own EVM. The guarded doors were called
731 times and refused 90, so both directions were exercised
rather than one.
The control is the point. A fuzz harness that has never failed is a harness nobody has tested, so the same runs are repeated against 6 deliberately broken vaults and each break must be caught by a named invariant rather than by something going wrong somewhere.
| What was broken | Must be caught by | Was |
|---|---|---|
| a deposit credits the amount requested rather than the amount that arrived | I1 |
I1 |
| abandon forgets to debit the stock it paid out | I2 |
I2 |
| a deposit mints more shares than it paid for | I6 |
I6 |
| the load line is computed above the quote instead of below it | I7 |
I7 |
| exposure returns more than the swing it is a fraction of | I8 |
I8 |
| maxWithdraw stops being bounded by the cash on hand | I9 |
I9 |
One invariant was worthless and the control found it. The first version of I6 summed every
holder's convertToAssets and compared it against totalAssets — which is an
identity, because a pro‑rata claim on a pool always sums to the pool. It could not fail, and the
over‑minting break walked straight past it. It measures the price per share instead now, which is
where dilution is actually visible, and only a pool move is allowed to lower it.
The app's write path, driven in a browser
A property suite proves the contract; 24 more checks prove the page. There is no key
here, so the harness records every transaction the app tries to send and answers every later read by
replaying that history inside one eth_call, with the replayer's code placed at the user's own
address so msg.sender is right. It covers EIP-6963 discovery, connect, the 4902 add-chain branch, the chain switch, both balances, the CREATE prediction at nonce 0, simulate-before-send, the receipt, adopting the vault, approve, a guarded deposit, and the vault reading its own new state back.
What it does not cover is stated in the same breath: a wallet actually signing, and gas actually being paid. That is the wallet's job and it is the one step between this and a transaction on chain.
It earned itself immediately: the app had no control for ship, so a vault built
through it could only ever hold cash, exposure was zero by construction, and the load line was
always exactly the quote. Nothing else had noticed, because nothing else had ever driven the page.
What a property suite does not prove
It proves the contract behaves as claimed. It does not prove the front end sends the calldata the
contract was proved against, which is a separate execution: tools/verify-app.mjs runs
js/vault.js's own byte strings against real USDG through a state override,
with negative controls, and the app on this site imports that same module.
And none of it is an audit. It is a test suite written by the author of the contract, adversarially reviewed by the same person. What is live, part by part →