The contract
Executed, not described
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 fork, no funded account,
no private key. One property per call, so a revert can only have come from the property in that call.
What the vault is
An ordinary ERC-4626 vault with tracked accounting, a virtual share offset, a reentrancy guard and the
full standard surface. No strategy address, no upgrade path, no owner who can move the assets, no fee.
Assets sit in the contract; income arrives by somebody transferring the asset in, which is how a fee
router or a keeper actually pays a vault, and settle() is permissionless because it can only
ever move the share price up and only by exactly what arrived.
report() is the single trusted entry point, bounded in size and cadence, and unavailable
outright when steward is the zero address — which is what the app deploys.
The ABI surface is read mechanically out of the compiled artefact and checked against the declared interface: nothing outside it. A hand-written list of "owner functions to look for" tests the list.
Properties
29 of them, on chain
| # | Verdict | What it reports |
|---|---|---|
| P1 | holds | 4 layers for 4 mutations, none for the no-op |
| P2 | holds | refolded from totalAssets/totalSupply and it matches |
| P3 | holds | 5 layers, refolded in order, reproduce chronology() exactly |
| P4 | holds | a dropped layer changes the accumulator; the full one still matches |
| P5 | holds | order is committed to, not just membership |
| P6 | holds | price 1000000 -> 1099999 on 10000000 booked |
| P7 | holds | marked down 5, price 1000000 -> 950000 |
| P8 | holds | price from the layer alone: 1062096 |
| P9 | holds | in 1234567, out 1234567 |
| P10 | holds | all four previews match their calls at a non-round price |
| P11 | holds | deposit rounds down, withdraw rounds up |
| P12 | holds | 600 held, 100 booked, until somebody calls settle() |
| P13 | holds | offset 0, victim recovered 10000 bps of 10000 |
| P14 | holds | asked 1000, arrived 990, booked 990 |
| P15 | holds | the hook fired and the reentrant deposit reverted |
| P16 | holds | share decimals 9, one share = 1000000 |
| P17 | holds | withdrew maxWithdraw of 1016999999 in one call |
| P18 | holds | finite allowance spent, infinite one left alone |
| P19 | holds | refused with no steward, accepted with one, everything else identical |
| P20 | holds | 1% cap binds at 10, 9 accepted, 11 refused, stranger refused |
| P21 | holds | refused at gap 5, accepted at gap 0, same block and same amount |
| P22 | holds | zero refused, and a non-zero deposit that would mint nothing refused too |
| P23 | holds | a stranger changed neither the holdings nor the supply |
| P24 | holds | approve, transfer, donate and five views all left both alone |
| P25 | holds | the share is an ordinary ERC-20 and carries the claim with it |
| P26 | holds | supply 0, assets 1 after the last holder left |
| P27 | holds | the series starts at assets 0, supply 0 |
| P28 | holds | four kinds, distinguishable, and an empty settle is not one |
| P29 | holds | markdown stands, settle books 0, real income still books 7 |
Sabotages
Every defect, and who caught it
The contract is recompiled with one deliberate defect at a time. Each must be caught by a specific, related property, or declared a survivor with a reason. A missing anchor throws rather than reporting "not caught", because a sabotage that broke nothing looks identical to a hole in the suite.
| Defect | What it does | Caught by |
|---|---|---|
| accrue-writes-no-layer | settle() books income without writing a layer — the exact hole the site is about | P1, P3, P4, P5 |
| chronology-frozen | the layer is emitted but the accumulator is never updated | P2, P3, P4, P5, P27 |
| chronology-forgets-history | the accumulator commits to the latest layer only, not to the chain of them | P2, P3, P4, P5 |
| layer-records-pre-state | the layer is written before the mutation it describes | P2, P3, P4, P5 |
| empty-settle-writes-a-layer | settle() writes a layer even when nothing arrived, filling the record with nothings | P1 |
| no-genesis-layer | the constructor writes no starting point, so a reader has to infer one | P1, P2, P3, P4, P5, P22, P27 |
| markdown-writes-no-layer | a loss is applied silently — which is exactly what every other vault does | P7 |
| total-assets-is-balance-of | totalAssets reads the token balance, so a stranger can move the share price | P7, P12, P20, P21 |
| credits-what-was-asked-for | deposit credits the amount requested rather than the amount that arrived | P14 |
| no-reentrancy-guard | the mutex is removed from deposit, which the balance-either-side read makes exploitable | P15 |
| share-decimals-lose-resolution | the share token is not finer than the asset, so every price view returns 1 | P16 |
| stewardless-vault-can-be-marked | the zero-steward check is dropped, so anyone can mark a vault that has no trusted party | P19 |
| report-cap-removed | a steward may mark the vault by any amount at all | P20 |
| report-gap-removed | a steward may mark the vault as often as they like | P21 |
| zero-shares-guard-removed | a non-zero deposit at a coarse price mints zero shares and the assets go to everyone else | P22 |
| allowance-never-spent | a third party redeeming on your behalf does not spend their allowance | P18 |
| deposit-rounds-up | deposit mints on a round-up, so a round trip makes money | P10, P22 |
| withdraw-rounds-down | withdraw burns on a round-down, so the last holder pays for everyone else | P10, P11 |
| settle-undoes-a-markdown | settle re-books the surplus a markdown leaves behind, reversing a loss the holders already took | P29 |
| layer-index-dropped-from-the-fold | the layer index is dropped from the accumulator, on both sides | survives |
| owner-only-rescue-added | an owner-only rescue() is added that can move every asset out | survives ABI read |
layer-index-dropped-from-the-fold
the layer index is dropped from the accumulator, on both sides
REDUNDANT, NOT MISSING — and the first version of this sabotage was WRONG. It dropped `n` from the internal accumulator only, leaving the external `fold()` a reader uses still taking it, so four properties caught a disagreement between the two rather than the thing being tested. Dropped from both, it survives, and that is the honest result: the accumulator takes the previous value as its first argument, so position is already committed to by construction. The counter is kept because it makes a mis-indexed replay fail loudly rather than silently, and the suite says plainly that no property can tell the difference.
owner-only-rescue-added
an owner-only rescue() is added that can move every asset out
NO PROPERTY CAN SEE THIS. It adds a function rather than changing one, and every property tests behaviour that still holds. It is caught by the mechanical read of the compiled ABI below, and by nothing else — which is the argument for doing that read at all.
A property that is red on the correct contract appears in every sabotage's caught-by list and proves nothing, so the runner fails the build if any property is caught by every real sabotage.
Randomised runs
And then nobody chooses the order
A property builds one state and asserts one thing about it. The fuzzer drives the vault through 2,208 arbitrary calls from three accounts — deposits, mints, withdrawals, redemptions, share transfers, income, markdowns — and re-checks eight invariants after every single one, on this chain's own EVM.
It found a real one
A markdown lowers what the vault claims while the tokens stay physically in
it — so the surplus it leaves looked exactly like income nobody had booked yet, and
settle() is permissionless. Anyone could call it and silently reverse a loss the holders had
already taken.
No property saw it, and the reason is structural: it needs a markdown
followed by a settle, and each property builds one state and asserts one thing. A randomised run
of forty operations did it twice in four seeds. The fix is a writtenOff floor that
settle() will not book below; P29 is the regression test and
settle-undoes-a-markdown is now a deliberate break in both suites.
The harness had the matching bug: its conservation invariant fed on
settle()'s own return value, so a vault booking income nobody sent balanced perfectly
against its own lie. It counts what the harness actually transferred now.
Read it
The Solidity ships with the site. Nothing here is deployed by this repository.