The review is complete and the findings file is written. No tracked file was changed.

Outcome: no reproducible defect found in the run-7 code. The findings file holds one informational entry recording coverage, the verified run-7 behaviours, and the trust assumptions.

What was read in full: all nine contracts under src/ plus the interfaces. Each was checked against the Pashov checklist and the launch's forbidden list. There is no post-launch minting, pausing, blacklisting or seizing, no delegatecall or selfdestruct, and no proxy or initializer.

Run-7 items confirmed in code:

• Letters pay no auto-sell fee; only a plea without the BY_LETTER flag does, and the 0.70 IMD floor holds for both paths.
• Over-long letters revert with LetterTooLong(bytes, 280).
• Seat multiplier is score times 1.2 floored, read through a gas-capped staticcall that cannot block a record.
• Owner fee 0.75% with 2.0% total, cap decay 15 days, distributor Ownable2Step with renounce blocked before the root.
• Fact-score bands, PASS_MARK 71, letter share 15%, and every Tribunal number match the brief.

Checks run:

Not reached: the live Sepolia Intake, Stacker, TestIMD, oracle-fee token and seat NFT are external code the contracts trust. The fork suites need RPC URLs, and the full-profile invariant and adversarial suites were not re-run within the time budget.

I found no defects I could reproduce. .imd-findings.json is written with an empty findings list and one coverage row for each of the 56 entry points, plus two invariant rows. I changed no other files and wrote no scratch tests, since there was nothing to prove.

Coverage: 54 entry points are marked holds and 2 unreached:

• unreached: PleaHook.rebalance() and the rebalance branch of PleaHook.unlockCallback. I didn't trace them within the time.
• Hook swap callbacks: beforeSwap and afterSwap are marked holds for control flow only: how the trader and fee are passed between them, sells allowed only from the gate, exact-output buys refused while the Cabal lives, and when the hourly price snapshot is taken. I did not re-check the fee and cap arithmetic; that belongs to the math and economics reviewers.

What I traced in depth (Execution Trace, Periphery, First Principles):

• Plea, appeal and sale flow: pleas and appeals in the gate are scored before the fee swap, so the fee sale can't move the balance or buy record being scored. Callbacks are accepted only from the Intake and only for a pending request. A sale's status is updated before its swap, and a gate swap callback runs only when the gate expects one.
• Letterbox: each escrow is closed before any payout. Letters pay no 0.35 IMD auto-sell fee, the site's auto-sell box does, and the 0.70 IMD floor applies to both. An over-long letter is refused with LetterTooLong, and appeal amounts are clamped to the original's share of the balance.
• Tribunal and Seasons:
  • The 1-hour grace before a season can close covers the 20-minute objection window plus a 20-minute pending objection.
  • An overruled stake is booked to the plea's own season.
  • The recorded score is the lowest any panel gave, and a sustained objection blocks the points.
  • A caller can't use a tight gas limit to make the Tribunal, launcher or seat-NFT read fail and still finish the record. Too little gas would be left for the rest of it.
• Accounting: the prize pot's balance never falls below what Seasons has booked. The PLEA bonus burns are bounded by what Seasons holds.
• Periphery: the gate's hand-written number and address formatting and its text escaping are correct. The distributor's leaves are 84 bytes, so they can't be confused with the tree's 64-byte inner nodes. The launcher's address hashing has a single variable-length input, so the static-analysis "hash collision" warning doesn't apply.
• Launch wiring: registration with PLEA, the committed-code checks for the hook, Letterbox and Tribunal, and seed's rule that the current PLEA owner may open trading early.

Static-analysis leads I rejected:

• The "uninitialized" storage maps and local variables are mappings and counters that start at zero on purpose.
• The "weak PRNG" warnings are the hourly price ring's % RING indexing, not randomness.
• The "reentrancy" warnings involve trusted contracts (PoolManager, Intake, IMD, PLEA) or paths that are already guarded.

One lead I left unreported: Seasons._standing treats a Tribunal standing() call that reverts as "not held" with no lowest score. That call can only revert if the external Intake's requests() reverts while an objection is pending, and I couldn't make that happen with the Intake as it is.

The review is complete. No tracked file changed, and the findings file is in place with an empty findings list and a coverage row for all 56 entry points plus 4 invariants.

Outcome: no reproducible economic defect in the run-7 tree. I audited the Economic Security, Invariant and Flow Gap failure modes against every value flow and found each guarded, either by code or by a documented and accepted limit in the threat model. The file at .imd-findings.json holds {"findings":[]} and sixty coverage rows, every one holds with a one-line reason.

What I traced and confirmed

• Season pot accounting. The accounted pot always equals open season fees plus rollover and never exceeds what Seasons holds. Checkpoint, objection checkpoint, close and flush all preserve it, and no IMD leaves Seasons unaccounted.
• Objection stakes are conserved. Each stake leaves the Tribunal exactly once, to the objector or to the plea's season pot. A verdict after a season's end belongs to the next season, so the 40-minute hold always ends inside its season's one-hour close grace.
• Trade fees. The hook charges 2.0% on the fill with the agreed split and burns 0.25% of the PLEA leg. Exact-input and exact-output formulas give the same share. Payout decisions key on the pool's own IMD, not the PoolManager balance.
• Letterbox custody. It holds exactly its open escrows' PLEA plus one tip each. Letters pay no auto-sell fee, the site's box pays at most the sale, and every escrow ends once.
• Launch manifest. Constructor arguments match each constructor in order, both code hashes match this tree, and the manifest test confirms the gas fit.

Verification runs on this tree

Not reached in depth. The attestation signature and replay logic in OracleAttestation.sol was outside my area and I did not read it. The two oracle callbacks are marked holds for their economic effects only, and the rows say so.

Leads I checked and dropped. The seat flash-rental at record time, the two-wallet objection shield, the min-of-panels re-roll, and the trend pump across an hour boundary are all explicitly accepted in the threat model or in OBJECTIONS.md Known limits, so none opens a revision. The static analysis lines in my area (strict equalities, reentrancy orderings in Seasons and the Letterbox) were all behind guards or trusted tokens and produced no failing input.

Findings file is complete and valid. Final recap:

Scope covered. I audited the arithmetic of all nine contracts against the Pashov Math Precision, Boundary and Numerical Gap guides: fee splits and their rounding at dust sizes, the fact-score bands and need, the Letterbox's escrow, fee-cap and floor clamps, the Seasons prize and bonus shares, the cap ratchet and wall-guard remainder math, the hourly ring, and the Tribunal's margin rule. Where reading left doubt I swept the numbers in Python and ran Foundry scratch tests under test/scratch/ (nothing there is kept).

Result: one Low, no Medium or higher.

• Low, src/Letterbox.sol:396. The delivery floor is 95% of the escrow's gross snapshot value, but the gate compares it with the sale net of the hook's 2% fees and the price impact. At spot equal to the snapshot a delivery pays 97.84% of the snapshot value, so the floor tolerates only a ~2.8% intra-hour dip. The ledger's R3-A2-3 note says 5%. A 3.2% dip makes deliver and SELL revert SlippageExceeded, and the approval then lapses with the oracle fee spent and a 4-hour cooldown. A fix that keeps the 95% number is to measure the floor against the gross pool fill, or to document the effective tolerance.

What held. The hook's IMD fee always covers cashback, owner and prize shares for every fill size at every launch rate (swept exact-in and exact-out fills of 1 to 200,000 wei). The 25 prize shares sum to exactly 10,000 bps on the 450-to-350 line. Every timing boundary (> versus <=) is consistent between the gate, the Letterbox, the Tribunal and Seasons. The season accounting cannot underflow, late fees after the death land in the last season, and the letter fee cap still admits a letter with the snapshot 8.5% above spot on the Sepolia path.

Coverage. All 57 listed entry points have a row, 55 holds, 2 finding (the delivery path), plus three invariant rows. Not reached in depth: the fork and invariant suites under the full profile, and the mainnet fee path beyond the existing round tests.

The review is complete. The findings file is written and valid, and the working tree has no other changes.

Result: no reproducible defect in the permissions area. The findings file at .imd-findings.json holds an empty findings list and a coverage record with one row for each of the 56 listed entry points plus four invariant rows, all holds with a one-line reason.

What I covered, per the three guides:

• Access Control. I mapped every role (PLEA owner, launch owner, distributor owner, launcher, Letterbox, Tribunal, Intake, PoolManager) and traced every state-changing entry point to its guard. Every privileged write has exactly one writer path. The launcher, hook, Letterbox and Tribunal registrations are one-shot with committed code. The two Ownable2Step contracts behave as intended, and the distributor cannot be renounced before its root.
• Asymmetry. I diffed the paired surfaces: submitSell against submitFor, appeal against appealFor, executeSell against executeSellFor, record against the close's batch record, object against standing, onOracleResult against onPleaFailure, plead against letters, and the gate's and the Tribunal's text validators. The only differences are the agreed ones, such as letters paying no auto-sell fee. The missing pendingOf check in executeSellFor is not exploitable because an Approved plea is always its seller's pendingOf.
• Trust Gap. The allowlist cannot reach the PoolManager, the gate or the Letterbox, so it cannot bypass the sell gate. The hook's fee beneficiary is immutable, so a PLEA ownership handover cannot un-exclude the team. The fail-open Tribunal and seat reads cannot be starved by a caller's gas choice, since the 63/64 rule leaves the outer record call too little gas to finish.

Verification run. The source tree builds under via_ir, and the eight LaunchManifest tests pass on this tree, confirming the launch.json code hashes, argument encoding and gas fit.

Not reached. I did not re-derive the hook's economic payouts or the pool math beyond their access paths, which belong to the other three specialists. Points already accepted in the findings ledger, such as the Intake's requestId binding and the record-time seat read, were not re-reported.

Added failure-path tests and randomized invariants for distributor ownership, seat accounting, and objections.

Validation with the supplied seed: build passed, 621 default tests passed, and 129 full-profile tests passed. Two fork checks skipped without RPC URLs.

Reported one confirmed low-severity Tribunal standing bug with a failing proof in .imd-findings.json.

The findings file is written and the scratch test removed. Final recap:

Verdict: two low findings, no critical, high or medium. The file .imd-findings.json holds both findings and a coverage row for all 56 listed entry points plus one for the Tribunal.standing view.

Finding 1 (low, Tribunal.standing, merged from the tester's finding). The pending-objection branch returns held=true before the seller's exclusion is checked. I ran the tester's proof on this tree and it fails at the final assertion as described: after the seller accepts PLEA ownership mid-objection, status() says the seller is excluded while standing() still holds the plea. Impact is a public read only. Seasons rejects the excluded seller before consulting standing, so no points or funds move. A fix changes the Tribunal's creation code, so the manifest's 13th PleaLaunch argument and the manifest test must follow it.

Finding 2 (low, Letterbox._deliver, merged from the math specialist). The 95% floor is taken on the gross snapshot value but compared with the gate's output, which is already net of the 2% fees and impact. The arithmetic gives about a 3% tolerance inside the hour, not the 5% recorded in the audit log. A deep enough dip lapses the plea with the oracle fee spent and a cooldown. The agreed 95% number stays. Either compare against the gross fill or document the effective tolerance.

What I verified myself.

• The two entry points the flow specialist could not verify, PleaHook.rebalance and PleaHook.unlockCallback, hold: PoolManager-only behind a one-shot flag, and a rebalance that does no work reverts.
• test/LaunchManifest.t.sol passes on this tree, so launch.json commits to the committed Letterbox and Tribunal code, the notes fit the cap and the launch fits the gas cap. The manifest has the right kind, 1/7/4/2/13 arguments in declaration order, and even-length hex throughout.
• Every runtime is within EIP-170 (CabalGate 23,742, PleaHook 24,358, Letterbox 23,229, Tribunal 20,116, Seasons 12,473 bytes).
• The run-7 numbers match the brief: owner 75 bps, cap decay 15 days, letters 15%, PASS_MARK 71 with the stated fact table, seat multiplier 1.2 via a gas-capped read, distributor Ownable2Step with the renounce guard, objection window 20 minutes, stake 0.35, margin 2, two rulings.
• Static-analysis leads (weak-prng, uninitialized-state, incorrect-equality, the aderyn casts and encodePacked) are false positives on inspection: ring indexing, mapping declarations, exact-match comparisons, and a fixed-layout init code hash.

Not done. I did not re-run the full 759-test suite or the full profile suites; the verifier runs those, and nothing I read contradicts their state.