Invariants and testing

Implemented

The properties asserted across randomised action sequences, and what they rule out.

#Results

text

contracts (forge)     93 passed   (8 suites, 0 failed)
@vaults/shared        75 passed
@vaults/fomoscan      22 passed
@vaults/sdk           13 passed
playwright  desktop   45 passed
playwright  mobile    45 passed

#Invariants

These run against randomised action sequences — arbitrary interleavings of deposits, redemptions, source buys and sells, epoch settlements, time warps and syncs. Each is checked after every step.

Invariant	Rules out
`sharesAreAlwaysBackedByAssets`	Shares existing without backing
`individualClaimsNeverExceedSupply`	A claim larger than the pool it draws on
`executionRouterNeverHoldsValue`	Value stranded in the routing layer
`noStandingApprovalsExist`	An adapter holding a live allowance between transactions
`sourceAccountNeverHoldsVaultShares`	The source acquiring a stake in what it signals
`privilegedRolesNeverAccrueClaims`	A role quietly accumulating a claim on depositor assets
`keepersNeverAccumulatePositions`	A keeper extracting position value through its bounty
`reservedClaimsAreAlwaysCovered`	Promising a redemption the vault cannot pay
`trackedAssetSetStaysBounded`	Unbounded growth making a sync ungasable
`vaultHoldsNoNativeBalance`	Native value arriving where accounting does not track it

The fifth is the one the whole design rests on. It is not asserted in prose; it is checked after every step of every randomised sequence.

#Property tests worth naming

The oracle blackout test. Force every price feed to fail. Assert totalAssets() reverts. Assert the in-kind exit still succeeds. This is the central promise, tested directly.
The airdrop test. Send an unapproved token to a source. Assert it is recorded as divergence, never purchased, and does not move the sizing denominator.
Divergence reporting. Assert the reported divergence uses the immutable desired size, not a value already reduced by a cap — the bug that made whichever cap bound last report zero.

#Interface tests

45 Playwright tests run across a desktop and a mobile viewport. They assert product properties rather than pixels, so they survive legitimate copy changes:

unavailable never renders as a zero
the four verification facts never merge into one tick, and the X badge never carries a check
an ineligible source is listed and labelled, not hidden
both exits sit alongside deposit
the deposit drawer traps focus, closes on Escape and on backdrop, and restores focus
no route can be scrolled sideways, and nothing is painted outside the viewport
the hero returns to its exact geometry after ten scroll round trips

Note. That last group is a regression suite for a real defect: an earlier hero tied its transform to scroll position and drifted on the way back up. The test scrolls to the bottom and back ten times, asserts the page is genuinely at the top first, then compares bounding boxes to a 1px tolerance.

#What is not tested

There is no mainnet deployment, no external audit, and no fuzzing campaign against a live venue's real liquidity. The execution adapter has not been proven against the real venue — that is production gate 3.