Run on the chain, then deliberately broken
There is no testnet here, no toolchain, no funded account and no private key. An eth_call with no to executes creation code on the real EVM of Robinhood Chain and returns whatever the constructor returns, so each property below is a real execution against the real evaluator, costs nothing, and leaves nothing behind. Last run at block 56,798,152.
All 24, and what each one does
| # | Property | Result |
|---|---|---|
| P1 | A first deposit mints against its own assets | executed · pass |
| P2 | The ERC-4626 inflation attack does not work | executed · pass |
| P3 | A donation does not move the share price | executed · pass |
| P4 | The protocol cut cannot exceed the hard cap | executed · pass |
| P5 | sweep() cannot reach principal | executed · pass |
| P6 | openPostern refuses an unlimited allowance, as unlimited | executed · pass |
| P7 | openPostern refuses an over-large allowance, as inexact | executed · pass |
| P8 | openPostern refuses an under-size allowance, as inexact | executed · pass |
| P9 | After openPostern, nothing is left standing | executed · pass |
| P10 | After the ordinary deposit, everything approved is still standing | executed · pass |
| P11 | residual() predicts the real post-state | executed · pass |
| P12 | exposure() is the lesser of allowance and balance | executed · pass |
| P13 | A token that does not decrement is refused, and nothing is kept | executed · pass |
| P14 | A fee-on-transfer token is credited what arrived, not what was asked | executed · pass |
| P15 | A reentrant deposit cannot credit itself twice | executed · pass |
| P16 | previewDeposit agrees with deposit | executed · pass |
| P17 | previewRedeem agrees with redeem | executed · pass |
| P18 | A round trip never returns more than went in | executed · pass |
| P19 | Redeeming somebody else’s shares needs their allowance | executed · pass |
| P20 | Transferring the share transfers the claim | executed · pass |
| P21 | harvest takes its cut from the gain, never principal | executed · pass |
| P22 | harvest cannot book income the vault does not hold | executed · pass |
| P23 | Both doors price the same deposit the same way | executed · pass |
| P24 | Only the front door leaves a key behind | executed · pass |
A suite nobody has shown to fail is a suite nobody has tested
Each row is the contract recompiled with one deliberate defect and run again. The defect is applied to a string in memory, never to a file, so an interrupted run cannot leave a broken Postern.sol in the repository — and every anchor carries the number of times it must match, so a search-and-replace that silently stopped matching throws instead of quietly testing nothing.
| Defect | What it does | Caught by |
|---|---|---|
| donation-priced | read assets from balanceOf instead of the storage counter | P3 |
| no-offset | remove the virtual share offset from both conversions | nothing — expected |
| cap-removed | let the owner set the protocol cut above the hard cap | P4 |
| sweep-principal | let the owner sweep the whole balance, principal included | P5 |
| no-share-allowance | let anyone redeem anyone else’s shares | P19 |
| price-after-assets | price a deposit after its own assets have landed | P2, P5, P16, P21 |
| credit-requested | credit what was requested rather than what arrived | P14 |
| no-mutex | remove the reentrancy guard the arrived-balance measurement requires | P15 |
| unlimited-accepted | let openPostern take an unlimited allowance | P6 |
| inexact-accepted | let openPostern take more allowance than the deposit needs | P7 |
| no-readback | trust the token to have consumed the allowance instead of reading it back | P13 |
| residual-lies | have residual() always answer zero | P11 |
| extra-owner-hatch | add an owner-only rescue() that no property forbids | the ABI surface (rescue) |
rescue() breaks no invariant any property states, and is seen only by a mechanical read of the compiled ABI. If nothing in this list were expected to survive, "caught by everything" would read as strength rather than as a suite whose edges nobody has probed.Three of these were missed on the first run, and the reasons are worth having. Two guard properties only asked whether openPostern reverted — so removing the unlimited-allowance check changed nothing they could see, because the very next line still said no, for a different reason. They check the revert selector now. The third was worse: the reentrancy exploit never fired at all. The hook re-entered the vault as the token, the token had approved nothing, and the inner deposit died on allowance before it could do any damage — so the property passed against a vault with its guard removed. An attack that never fires is not a passing test, and the property now fails unless the hook records that it ran.