Approved workflow

join() sets lastPingOf[msg.sender] = block.timestamp (line 81), so the join itself is the first ping, and OPEN_PERIOD and PING_INTERVAL are both 30 days (lines 25-27). Every address that joins in the deployment block therefore has its first deadline at exactly openUntil, and the whole day-0 cohort becomes overdue simultaneously at openUntil + 1 -- the very first instant at which evict() can ever succeed (nothing is evictable earlier; that part of the design holds, see the notes finding). An entrant who joins at openUntil - 1 with 1 wei has a deadline of openUntil + PING_INTERVAL - 1 and is the only address not overdue in that block, so a single transaction at openUntil + 1 can evict every other participant and claim the entire pot. Stake size does not matter and no capital is at risk for the attacker.

This is a parameter choice rather than a coding error: the rule 'ping at least once every thirty days' is implemented faithfully and the README documents that stake size is irrelevant and that eviction is first-come. But the README also lists OPEN_PERIOD, PING_INTERVAL and the join-as-first-ping behaviour under 'Unresolved choices ... open to reversal before deployment', and the concrete consequence is that survivor selection for the majority of the field collapses into a single block that is fully predictable from deployment time, decided by gas priority rather than by liveness. The same asymmetry lets an overdue participant rescue themselves without ever pinging: with alice and bob both overdue at openUntil + 1, whichever of them calls evict() first becomes the last one standing (immune under the CannotEvictLast rule) and claims, while the other -- equally delinquent -- loses everything (verified passing in the same PoC file as test_poc_overdueParticipantEvictsPeerAndClaimsWithoutEverPinging).

Resolving this requires a design decision that is not mine to make, and I am not prescribing one. Options and their tradeoffs: (a) accept as-is and have the website surface deadlineOf() and a 'your join is your first ping' warning very prominently -- zero source change, but the day-0 cohort stays exposed; (b) set OPEN_PERIOD strictly shorter than PING_INTERVAL (e.g. 14 days) so day-0 joiners get a grace margin after the window closes and deadlines fan out -- a one-constant source change, but it shortens the joining window and changes the approved 30-day open period; (c) seed lastPingOf at openUntil for joiners rather than at join time -- removes the simultaneity but weakens 'must ping every thirty days' during the open phase. Each of (b) and (c) changes agreed behaviour and needs a scope decision plus a re-review; (a) is a documentation/UX decision only.

pot is only ever incremented inside join() (line 82). Any LAST that arrives by a plain token.transfer() to the Tontine address -- a mis-sent 'top-up' by a participant who does not realise there are no top-ups, an airdrop, a bot paying the wrong address -- is not counted. claim() pays out exactly pot (lines 113-119) and then empties the roster, so after the winner is paid the contract still holds the unaccounted tokens while pot == 0, participantCount() == 0 and joining is closed. There is no withdrawal, rescue, owner or sweep function by design, so those tokens can never move again. This is a real and permanent loss of user funds, though it requires the user to send tokens the contract never asked for, and the no-escape-hatch design that causes it is the same property that makes the contract trustless.

A fix that preserves intended behaviour exists and is cheap -- pay token.balanceOf(address(this)) in claim() instead of pot, keeping pot as the accounting/display value -- and is safe here specifically because the token is fixed at construction to LAST, which is non-rebasing, has no fee on transfer and cannot be re-entered. It does change observable behaviour (the winner would receive donations too), so it is a scope decision for the source owner, not something to apply silently. The alternative is to accept it and state it in the README under 'Operational responsibilities' alongside the existing warning that nobody can refund or move funds.

_assertConserved() asserts token.balanceOf(address(tontine)) == tontine.pot() and is called from thirteen tests, and the README presents it as the suite's conservation guarantee. But every call site reaches the contract's balance only through join(), which increments pot by the same amount it pulls, so the assertion is a tautology in all of them: there is no test in which the contract's balance can differ from pot.

The single state where the equality can break -- an unaccounted inbound token.transfer -- is never constructed, so the strongest claim the suite makes is never tested against its only counterexample, and the permanent-lock behaviour in the finding above ships with green tests.

The same applies to the second half of the helper ('a funded pot must always have a claimant'): it is only ever evaluated in states reached through join/evict/claim, so it never distinguishes a real invariant from an accounting identity.

The README names 'Eviction ordering is first-come. If two remaining participants are both overdue, whoever submits the first evict picks the winner' as the protocol's headline caveat, and it is the state in which the entire pot changes hands.

The suite never asserts it end to end. test_evictByAnyoneIncludingSelfAndParticipants (line 278) has an overdue bob evict alice, but then has bob evict himself rather than claim, so it never checks that a delinquent survivor reaches claim(). test_claim, test_soleSurvivorNeedNotPingToClaimLater and the fuzz test all have the survivor ping first, so in every claim test in the suite the winner is in good standing.

The behaviour the README promises -- that CannotEvictLast makes the delinquent survivor immune and lets them take the pot without ever pinging -- is therefore asserted nowhere, and a future change to the evict() guard order (moving the _roster.length == 1 check before _isOverdue, or adding a caller-in-good-standing requirement) would not be caught by any red test.

Scope: the working tree contains src/, test/, docs/abi/ and README.md but no launch.json, so the manifest node has not run and there is nothing to review against the LaunchManifest schema in this pass. Per the stage rules an early review does not require a manifest that has not run yet; this entry records the constraints the accepted source imposes so the manifest node and the final review can check them, and records what I positively verified so it is not re-derived.

Manifest constraints implied by the source: kind 'evm_project'; token contract 'Lastlight', name 'Lastlight', symbol 'LAST', decimals 18, and the token constructor takes no arguments (src/Lastlight.sol:28), so the token entry carries no constructorArgs. Exactly one application contract, 'Tontine', with constructorArgs ['$token'] and nothing else -- the constructor's single parameter compiles to ABI type 'address' (internalType 'contract IERC20'), which is a legal target for a $token reference, and there is no owner parameter anywhere, so $owner must not appear. Neither name is 'MerkleDistributor' and both match ^[A-Za-z_][A-Za-z0-9_]{0,31}$. Pool per policy: pairedCurrency 0x0000000000000000000000000000000000000000, fee 3000, tickSpacing 60, initialPrice '79228162514264337593543950336'. A schema-valid manifest that passed anything other than $token as Tontine's argument would produce a Tontine bound to a token that is not LAST; the constructor only rejects address(0) (src/Tontine.sol:65), so that is a manifest-review check, not one the source can make.

What I verified and found correct, so it does not need re-deriving: no owner, admin, fee, pause, upgrade or withdrawal surface in either contract; neither constructor uses msg.sender to assign a privileged role (the token mints to msg.sender, which is required, and the factory holds the whole supply afterwards); checks-effects-interactions is followed in both join() and claim(), with the token call last in each; the token's unchecked arithmetic is guarded by the preceding balance/allowance checks and the from == to case is correct; 68 project tests pass and the two protected floor suites pass (8/8) against the compiled creation code through a simulated CREATE2 factory at chain 11155111; forge fmt --check is clean; lib/forge-std is committed as ordinary files (git mode 100644, no gitlink); docs/abi/Lastlight.json and docs/abi/Tontine.json are byte-identical in content to forge inspect <Contract> abi --json (17 and 34 entries, exact match). A stateful invariant fuzz I wrote (400 runs x 120 depth, 48,000 calls across join/ping/evict/claim/warp with 6 actors) found no violation of balance==pot, funded-pot-has-a-claimant, roster-is-a-set, no-state-for-non-participants, pay-at-most-once, phases-do-not-overlap, or token supply conservation. The two-phase claim in the README holds under the current constants: an entrant's earliest deadline is deployTime + PING_INTERVAL, which is never before openUntil, so no eviction is possible while joining is open -- but that depends on OPEN_PERIOD <= PING_INTERVAL holding as a value relation, which the code does not assert.