Testing and verification

The levels

The economic invariants

These are the equalities that must always hold:

1. The four shares sum to exactly the tax charged, 500 basis points by default, with no wei lost
2. Nobody can withdraw a vault's assets to an address of their choosing; the only possible decreases are conversion, the airdrop to holders, and the owner's emergency transfer
3. A basket's weights sum to 100 % and never change
4. Both positions are deposited at creation and can only be removed by the end mode, 30 days after it is announced
5. Liquidity is locked; its only exit is the end mode, which the owner announces 30 days ahead
6. The $STOCKFUN buyback cannot send bought tokens anywhere but the burn
7. Creator supply is zero on every market
8. A vault can only buy its basket's assets
9. A vault only acquires ETH, USDC, USDG and its basket's stocks, plus USDon refunds on the optional Ondo rail
10. An airdrop cycle never pays out more than it holds, stock by stock, and no holder receives more than their pro-rata share; what the airdrop contract owes, across cycles and held-aside stocks, never exceeds its balance — required since 2026-09-27, tested since 2026-10-04 by a stateful invariant. Since 2026-10-05, through emergencies too, what backs those books is always made of tokens the contract actually holds, never of tokens not credited yet, tested by a second stateful invariant
11. Only the liquidity lock adds liquidity to a StockFun pool
12. A trade pays nobody but the market's vault; the other shares wait on the hook until claimed. Since 2026-10-05 a vault that refuses its share is owed it on the hook, and the trade goes on
13. Each basket stock spends only the cash reserved for it

They are checked on the current implementations; an upgrade replaces the code they are checked on.

The size constraint

The EIP-170 limit is 24,576 bytes of runtime code. It is enforced by a test that fails the test suite, not by manual inspection.

It is a real constraint here: the factory had to be split. Until 2026-10-02 the vault deployer, which embedded a TreasuryVault's creation code, was the contract closest to the ceiling, and every line added to the vault was charged against that headroom. Removing the creator buyback on 2026-09-28 took it from 23,055 to 14,965 bytes; the fixes of 2026-10-01, which reserve the cash stock by stock, brought it to 15,954. Since 2026-10-02 it deploys a proxy, and what must fit under the limit is each module's implementation.

On 2026-10-05 the airdrop contract became the closest. The fourth audit loop's claims took it over the limit; making some of its views private and dropping its emergency transfers charged to one cycle brought it back to 24,432 bytes, 144 under the ceiling.

After the 2026-09-29 audit

Each finding fixed after the security audit of 2026-09-29 has regression tests that fail on the audited code; most are the audit's proofs of concept, inverted to check the fixed behaviour.

The security pipeline of 2026-10-01

A second audit round, by two independent auditors, then every check again on the fixed code. Each of its fixes to the contracts and the keeper has regression tests. On 2026-10-01, after those fixes:

• Foundry. The 421 tests outside the fork suites pass, and so does the deep profile: 20,000 fuzz runs, invariants at 512 runs of depth 128. The fork suites did not run: no RPC URL was available.
• Mutation testing. slither-mutate ran on five contracts: the fee distributor, the holding record, the treasury vault, the Robinhood Chain stock router and the remote hub. It made 1,301 mutants, small deliberate changes to the code, and the tests caught 1,118. Of the 183 that survived, 107 are equivalent to the original code: no input can tell them apart. The other 76 showed checks the tests did not make; the tests now cover all of them. No mutant revealed a bug.
• Formal verification. Every Certora job was re-run on the prover, on the fixed code (certora-cli 8.8.1, basic sanity checks). No rule was violated. Seven LiquidityLock rules remain undecided on one method, lockProtocolLiquidity: they ran out of time, and a re-run with a longer limit ended without a verdict. They hold on every other method; that one is owner-only, runs once, for $STOCKFUN, and Foundry tests cover its access, its single use and the shape of its lock. The other results not verified are known vacuity cases: a rule run on every method, for a method that can never succeed in the verified setup. The first TreasuryVault run's failures came from two artefacts of the specification, none a bug; the specification was fixed.
• Fuzzing and symbolic execution. Medusa ran five properties of the holding record for ten minutes with no failure. Its first run found that on a chain whose clock starts in hour 0, a test chain, the recorded supply's first hourly mark was missing; no real chain was affected, and the token now records that mark at deployment. Halmos passes three symbolic checks for every input in bounds: the fee split is exact, the recorded supply follows any two transfers, and its integral at the next hour is right. Mythril cannot explore the protocol contracts outside a deployment, about 14 % coverage; on the self-contained holding record it reached 31 % in 15 minutes and reported nothing.
• Static analysis. Slither, Aderyn and Solhint found nothing new.
• On a fresh local chain. A full deployment, a real keeper cycle and ten use cases pass. The deployment rehearsal, the production scripts run in the runbook's order, passes after one script fix: the mock rail's script minted its seeding funds to forge's default sender instead of the deploying key.

That run also verified 11 rules of TeamVesting, a contract deleted with its specification on 2026-10-05. The prover does not cover the Robinhood Chain side: the remote hub, the mirror vaults and the stock router.

The upgradeable redesign of 2026-10-02

The redesign that made the modules upgradeable came after every check above. On 2026-10-02, on the new code:

• Foundry. The 458 tests outside the fork suites pass. New suites cover the upgrades, on Ethereum and on Robinhood Chain — who may upgrade, the authority and the PoolManager a new implementation must keep, the vaults one by one — and the end mode. The holding record's suite moved with the record, to the holding recorder.
• Storage layouts. Every upgradeable module's storage layout is recorded in contracts/storage-layouts/, and contracts/script/check-storage-layouts.sh fails on any change but an append. It is meant to run before every upgrade. Since 2026-10-05 it checks every depth of every struct: see Deployment.
• On a fresh local chain. The LocalRun script passes.
• Formal verification. The Certora specifications are being updated for the new code. Their last full prover run, on 2026-10-01, predates the redesign: the table above describes that run.

The deep profile, the mutation testing, the fuzzing and symbolic execution and the static analysis described above ran on 2026-10-01, on the code before the redesign.

The airdrop of 2026-10-04

The airdrop contract and the two sendToAirdrop paths, coded on 2026-10-04, not deployed. On that day, on the new code:

• Foundry. The 514 tests outside the fork suites pass, against 459 before the airdrop. Three new suites: AirdropDistributorTest, 38 tests; AirdropCrossChainTest, 15, with LayerZero mocked; AirdropInvariantsTest, 2, around a stateful invariant: conservation and solvency across two markets under random sends, claims, placings, openings, and changes of exclusions and cycle hour, 128 runs of 64 calls. A fuzz of the share computation runs 512 times.
• Gas. A claim of a cycle of two or three stocks costs roughly 120,000 to 210,000 gas as measured in the tests, which run with warm storage: a real transaction costs somewhat more. A delivery from Robinhood Chain costs about 85,000 to 1,016,000 gas on Ethereum, measured cold: see Deployment.
• On a local chain. On Anvil, LocalRun then LocalAirdrop: two holders, stocks held aside before 13:00 UTC, then placed and claimed after. Each claim is the exact floor of its share, with 1 wei of dust per stock.
• Formal verification. The five Certora specifications touching the changed contracts typecheck. The prover was not run, and no specification covers the airdrop contract.
• Offchain. The keeper's 93 tests, the shared package's 43, the back end's 9 and the worker's 58 pass.
• Reviews. Codex (gpt-6-astra) reviewed the design, then the code: one Medium, on the timing of held-aside stocks, and one Low, on the local script, both fixed. A re-review of the fixes found one Medium, on the timing of exclusion edits, and one Low, on the order of the local script, both fixed: a window is measured against the exclusion list in force when it closed, and the script places held-aside stocks first. A final check of those two fixes found no bug, under the stated guarantee: held-aside stocks go to the first window with eligible holdings whoever calls and whenever, as long as the cycle hour does not change and the token's holding recorder is not replaced in between. The reports are in projet/docs/audit-2026-10-04/.

The changes of 2026-10-05

No team allocation, an immediate emergency mode and every number an owner setting, coded on 2026-10-05, not deployed. On that day, on the new code:

• Foundry. The suite passes, 520 tests. Two new suites, Settings and SettingsCrossChain, cover each setting: who may set it, the values it refuses, and the next operation after a change — among them the tax and the anti-snipe, the launch shape, each pool keeping its key, and the shares of what the locked positions collect. The fee properties, fuzzed and symbolic, hold for any accepted settings. The emergency tests follow the immediate transfer, and the vesting contract's tests went with it.
• Gas. Reading the tax settings costs a swap about 1,200 more gas, warm.
• Formal verification. The specifications of the fees, the hook, the lock, the factory, the tokens and the oracle follow the settings and typecheck locally. The prover was not run.

The audit loops of 2026-10-05

The same day, five review loops went over the code, not deployed; from the fourth, a breach of the founder's rule that one failure never blocks the rest counts as a defect (see Architecture). Each fix has a regression test. On the code of each loop:

• Foundry. 602 tests pass after the fourth loop and 613 after the fifth; at the end of the day, 614 pass, three fork suites skipped without an RPC. Every contract fits under EIP-170, and the storage layouts only grew where a fix appended state.
• Invariants. The airdrop's invariants pass 512 runs of depth 128 under the deep profile, after the third loop. A second stateful invariant drives the airdrop through emergencies: deliveries whose last step runs late, stray tokens, transfers out, restores, write-downs and pauses, and, since the fifth loop, stocks frozen by their issuer and claimMany.
• Formal verification. The loops added rules on the hook (its debts to the vaults, its strays), on the lock (the shares it keeps, its rescues), on the burner and the tokens (their rescues), and a rule that only the protocol owner rescues on the routers, the oracle and the factory: 213 rules and invariants in 11 specifications after the fourth loop, one more on the tokens' rescues after the fifth. Every touched specification typechecks locally; nothing was sent to the prover, whose last run is still that of 2026-10-01.
• Offchain. After the keeper's airdrop step, the dapp's claim screen and the offchain pass of the fourth loop: the keeper's 191 tests, the shared package's 51, the back end's 9 and the worker's 90 pass, and the app passes its typecheck and lint.
• On a local chain. On Anvil, LocalRun, then the keeper, the worker's engine and the app's claim preparation: in the window of the deployment the keeper sent nothing; in the next it opened two cycles and sent two vaults' stocks, and one claimMany paid five stocks over the two cycles, at about 421,000 gas, after which claimable read zero.

The fifth loop's offchain pass, 2026-10-06

The fifth loop's review of the keeper, the worker, the app and the scripts found three medium-severity and sixteen low-severity issues, each fixed with a regression test, not deployed. Run on 2026-10-06:

• Foundry. 619 tests pass on that day's code, three fork suites skipped without an RPC: the Lens's new fields, the five-stock basket cap and the resumed $STOCKFUN launch have their tests. The storage layouts did not change.
• Offchain. The keeper's 210 tests, the shared package's 51, the back end's 9 and the worker's 111 pass; each keeper fix's tests fail when the fix is removed. The app passes its typecheck and lint; it has no test runner, and its claim preparation moved into the worker's engine, whose tests cover it.
• On a local chain. A rehearsal on a private Anvil passed its six scenarios: LocalRun, whose dry run writes no deployment file; the keeper over two windows, converting each vault's ETH once per window, then placing, opening and sending the airdrop once, every claim exact to the wei; a vault refusing ETH, its debts on the hook and the lock paid once it was restored; kills mid-flight with the state file and its lock, nothing sent twice, a replaced and a dropped transaction handled; the rescues and a daily LP-fee collection. The bridge rail, the app and the worker were not part of it.

After the rehearsal, 2026-10-06

The rehearsal's findings were fixed the same day, not deployed. The keeper places the stocks the airdrop contract holds aside for a market even when its vault has nothing new to send, and records a vault found under the threshold by the window it was checked for, never by its own clock; it counts a send held aside apart, leaves alone the few units of USDC a vault's last purchase leg can never spend, and shows pool ids in its log. The sixth review loop's first area found nothing in the contracts and one low-severity issue in a local script, fixed: the local deployment file is checked against the chain before the keeper, the app or the worker use it. On that code:

• Foundry. 620 tests pass, three fork suites skipped without an RPC: one more, a resumed $STOCKFUN launch refused a vault that holds another basket's stocks
• Offchain. The keeper's 218 tests, the shared package's 51, the back end's 9 and the worker's 111 pass; each keeper fix's tests fail on the keeper before it. The local deployment file's check has no automated test: it was run by hand on a private Anvil, where it passed a fresh deployment and refused a file with two contracts' roles swapped

After the sixth and seventh audit loops, 2026-10-06

The sixth loop's keeper and worker fixes and the seventh loop's were made the same day, not deployed; no contract's code changed in either, one comment of a contract being corrected. Run on 2026-10-06, on commit 415dcae (the contracts from a clean copy of that commit, since other contract work was under way):

• Foundry. 620 tests pass: 615 outside the fork files, and the five of the Robinhood Chain fork suite against its public RPC; the three Ethereum fork suites are skipped without an RPC. The same count as after the rehearsal: no contract test changed
• Offchain. The keeper's 277 tests, the shared package's 51, the back end's 9 and the worker's 137, in 11 files, pass. Each proof of concept of the seventh loop is a regression test, and each fix's new tests fail on the code before it, except the few that pin what the old code already did (a send the keeper cannot value goes as before; an old state file loads) and the chart's, whose functions are new. A state file written by the keeper before the sixth loop is kept as a test fixture and loads under the new keeper
• The app. It passes its typecheck, its lint and its build, and its pre-rendered demo chart spans the plot; it has no test runner, and no browser test was run. The chart's placement runs code from the worker's engine, which the worker's tests cover

The price-feed protections and the eighth audit loop, 2026-10-06

The oracle's two price-feed protections for Robinhood Chain were written on 2026-10-06, and the eighth loop's keeper, worker and app fixes the same day, not deployed. The contracts changed with the protections, not with the loop. Run on 2026-10-06, on commit 6586d40 (the contracts from a clean copy of that commit, since other contract work was under way):

• Foundry. 640 tests pass: 633 outside the fork files, in 82 suites, and the seven of the Robinhood Chain fork file against its public RPC; the three Ethereum fork suites are skipped without an RPC. The protections added 18 tests outside the fork files: 16 on the oracle alone, with mock feeds and tokens (each guard off, then on, every way a feed or a token can fail to answer, every answer that counts as paused, a read starved of gas, the owner's settings and the deployment script's refusals), and 2 on the cross-chain rail (a paused stock's leg fails alone and buys once unpaused; a sequencer outage stops every leg until its grace period ends). The two new fork tests read the real stock tokens: each of the twenty answers the pause signal as the oracle reads it, the most one read took being 13,288 gas, and a token paused where its real code keeps the flag holds back its own price alone
• Storage and specifications. The storage layouts of the 17 upgradeable modules are unchanged but for the oracle's append; the oracle's formal specification, 25 rules and invariants, typechecks, with no prover run
• Offchain. The keeper's 306 tests, the shared package's 51, the back end's 9 and the worker's 155, in 12 files, pass. Each proof of concept of the eighth loop is a regression test, and each fix's new tests fail on the code before it, except those of functions that are new
• The app. It passes its typecheck, its lint, its engine check and its build; it has no test runner, and no browser test was run. Its launch form's basket check and its trade panel's tax run code from the worker's engine, which the worker's tests cover

The ninth audit loop, Glamsterdam and the LayerZero testnet run, 2026-10-06

The ninth loop's fixes, the airdrop delivery's gas under Ethereum's Glamsterdam upgrade and the keeper's re-execution of a stuck delivery were made on 2026-10-06, not deployed on mainnet. One contract change (the remote hub's gas policies and the mirror vault's three-argument send and quote) came with them, tested by nine new tests of the cross-chain rail (the defaults against the measurements, the clamping at both ends, the send's options and the quote that matches them, the one-argument shapes, the setters' refusals, a delivery heavier than the gas its OFT enforces, a hub without policies keeping the stocks home, the options byte for byte) and four of the deployment script. The stock OFT mock now adds the gas options up and leaves a delivery short of gas waiting for a run with more, as LayerZero's endpoint does. Since this loop a second agent reviews each fix's change before it is pushed (the verifier gate), and its findings are fixed and tested the same way. Run on 2026-10-06, on commit 92a1904 (the contracts from a clean copy of that commit, since other work was under way):

• Foundry. 653 tests pass: 646 outside the fork files, in 83 suites, and the seven of the Robinhood Chain fork file against its public RPC; the three Ethereum fork suites are skipped without an RPC. Foundry runs the Cancun gas schedule: its gas figures are the old prices, and the new ones come from Sepolia
• Storage. The storage layouts of the 17 upgradeable modules are unchanged but for the remote hub's append (its gas policies, slots 21 to 23)
• Offchain. The keeper's 370 tests, the shared package's 51, the back end's 9 and the worker's 189, in 14 files, pass (the keeper's 372 at e1dd5f6, after the gate's last fix, the others unchanged); the keeper and the worker pass their typecheck. Each fix's new tests fail on the code before it, except those of functions that are new. The app's new gas limit per write runs code from the worker's engine, which the worker's tests cover
• The app. It passes its typecheck, its lint and its engine check; it has no test runner. Its two other fixes, the pot marked as an estimate and the approval that could not be read, were checked by running its own code in a scratch copy
• On Sepolia, after Glamsterdam. Every fixed gas number of the contracts and the scripts was measured again on the live chain: all hold, with room, but the airdrop delivery's two, fixed by the gas policies. The tenth audit loop found two more: the deployment scripts' own gas, which forge takes from its own simulation at the old prices (every broadcast now takes the node's estimate), and the bridge compose's, sized for one market and not for a batch. The keeper's preflight, run read-only on the LayerZero testnet run's deployment, passes its 68 checks
• The LayerZero testnet run. The protocol ran end to end on Sepolia and Robinhood Chain's testnet over LayerZero's real testnet endpoints, DVN and executor, seven hourly windows and six airdrop cycles, every claim exactly the share computed from the holding recorder: see The Robinhood rail. Its last window ran on the ninth loop's keeper, with the delivery gas chosen from its simulations

The tenth audit loop, 2026-10-06

The tenth loop's fixes were made on 2026-10-06, not deployed on mainnet, each reviewed by a second agent before it was merged. One contract changed, the USDG bridge adapter: a bridge batch's last step on Robinhood Chain now gets a base plus a part per market, and a batch carries at most 17 markets. Nine new tests cover it: four new five-stock markets, a full batch of 17 and thirty markets sent as two batches, each run cold at exactly its gas; 18 markets refused for their message's size; the fee growing with the batch; a batch above the cap refused whole while the next goes; an adapter set up before the new settings bridging nothing until they are set; and the settings' bounds. The mock of the USDG token's bridge now refuses a message above LayerZero's size limit and prices the gas, as LayerZero does. The deployment procedure has no test: its change was played on Sepolia, where a creation sent with the deployment tool's own gas ran out of it and the same creations sent with the node's estimate went through. Run on 2026-10-07, on commit 5ea8bf0 (the contracts from a clean copy of it):

• Foundry. 662 tests pass: 655 outside the fork files, in 84 suites, and the seven of the Robinhood Chain fork file against its public RPC; the three Ethereum fork suites are skipped without an RPC. The LayerZero testnet project's 2 tests pass, on LayerZero's own contracts
• Storage. The storage layouts of the 17 upgradeable modules are unchanged but for the bridge adapter's append (its two batch settings)
• Offchain. The keeper's 400 tests, the shared package's 51, the back end's 9 and the worker's 210, in 15 files, pass; the keeper and the worker pass their typecheck. Each reviewer's proof of concept is a regression test, and each fix's new tests fail on the code before it, except those of functions that are new. The app's follow of a transaction the wallet cancels or replaces, and its reads at no earlier than its own last transaction's block, run code from the worker's engine, which the worker's tests cover
• The app. It passes its typecheck, its lint and its engine check; it has no test runner
• On the testnets. The bridge adapter of the LayerZero testnet run was upgraded on Sepolia on 2026-10-06, and its next batch, one market, was delivered and composed by LayerZero's executor at its new gas, 600,000, of which 115,990 were used

What the tests do not prove

This matters and the project's own reports state it plainly.

Local tests simulate cross-chain delivery. They do not prove a real LayerZero delivery. The airdrop's cross-chain tests run against mocks of LayerZero and of the stock adapters, which are not in the repository for mainnet. Fork suites were excluded from at least one run because the public endpoints returned HTTP errors — and that report says so rather than presenting the suites as passing.

The LayerZero testnet run of 2026-10-06 carried real LayerZero messages between two testnets, with test stocks, test adapters, a test USDG and mock feeds: it proves StockFun's code over LayerZero's transport, not Paxos's USDG pair, Robinhood's stocks and their adapters, real feeds and liquidity, or mainnet's gas, fees and finality.

No run proves: LayerZero transport on mainnet, an external review, or a formal proof covering the current rail. The testnet run signed with real wallets, three of its claims through the app.

Locally

The full scenario runs in four terminals: the chain, the deployment and simulation, the price service, the dapp. Then the keeper and the browser harness.

The exact procedure is in projet/docs/LOCAL_TESTING.md.