Verification¶
A venue moves real money, so on top of the unit suites the module is checked against invariants over random command streams. Each invariant below was added because it caught a class of defect the previous one missed.
Run it all:
cd build && ctest # unit suites + fuzzes
../venue/scripts/run_sanitizers.sh # ASAN/UBSAN over parsers and fuzzes, TSAN over concurrency
Differential fuzz¶
test_venue_differential_fuzz drives the map-reference MatchingBook and the
O(1) LadderBook in lockstep over a random stream of limits, markets, IOC,
post-only, cancels, modifies and pegs. After every command:
- both engines must have emitted an identical event stream (compared as a rolling hash), and
- neither book may be crossed.
The reference book is the oracle: any ladder divergence fails with the command
index. Depth is CI-friendly by default; set FLOX_FUZZ_OPS for a deep run
(2M commands verified).
Conservation fuzz¶
test_venue_conservation_fuzz asserts money properties over a random stream
across five scenarios: spot, perp, perp with ADL, cross-margin, and multi-asset
collateral.
- Conservation of total. Each asset's total across accounts plus the venue account never changes.
- The reserved invariant. After the book is drained, every account's
reservedmust be zero.
What each property catches¶
Each of these defects passed the check above it in the table, and each round of hardening added the property that would have caught it:
| Property | Catches | Example defect it caught |
|---|---|---|
| conservation of total | money created or destroyed in aggregate | ADL crediting a winner while the deficit vanished |
reserved invariant (drain, then reserved == 0) |
buying power frozen: total is fine, the funds are stuck | residual reservations kept on IOC/FOK/reject paths |
| per-order reservation consistency | one order over-releasing, masked by other orders in the same account's aggregate | iceberg modify releasing against the displayed peak instead of the full size |
| per-account equity + insurance payout | mis-socialization: right total, wrong recipient | insurance paying out to an account that was solvent on total equity |
| insertion-order independence | a replica making a different choice from the same logical state | ADL victim chosen by hash iteration order |
| made-whole on non-fill | funds frozen when a fill does not happen | last-look reject stranding both sides' reservations |
| positive-obligation netting | a debit balance masking a real custody shortfall | segregation reporting a short custody balance as fully backed |
Several of these compound: funding driving a wallet negative while a position kept the account alive made states reachable that the ADL and segregation defects then exploited. Finding one exposed the next.
Sanitizers¶
venue/scripts/run_sanitizers.sh builds and runs:
- ASAN + UBSAN over the parsers (hostile network input), both fuzzes, the venue harnesses, and the recovery/journal paths. UBSAN halts on the first diagnostic; it caught a signed overflow in the LULD band computation on a high-priced instrument.
- TSAN over the sequenced single-writer core and the multi-threaded gateways.
CI also runs the whole project, venue included, under all three sanitizers.
Determinism gates¶
test_venue_enginereplays a journal into a fresh engine and requires an identical event-stream hash and ledger.test_venue_venuedoes the same for a stream containing anAdminCmdauction uncross, which is why auctions are sequenced commands.- Tie-breaks are asserted directly: equal-score ADL candidates must resolve to the same victim under a reversed insertion order, and mass-cancel must emit in ascending order id regardless of insertion order.
Book agreement¶
Market-data depth is compared against the engine's book over 300k commands, periodically at full depth. The full-depth comparison is what surfaced an iceberg's hidden reserve leaking into the public feed on a partial peak fill; top-of-book checks had passed.