Depositor maintenance (_activeDepositorSwitch) reverts with AlreadyLapsed when block.timestamp >= lastPing + period; claim reverts with NotLapsed when block.timestamp < lastPing + period. The two predicates are exact complements, so at every timestamp exactly one party can act and transaction ordering inside a block cannot change the outcome. setPeriod cannot shorten the deadline below now because MIN_PERIOD is 1 day.

Verified with the shipped tests (test_pingOneSecondBeforeLapseResetsDeadlineAndDefeatsOldClaim, test_atExactLapseAllDepositorMutationsRevertAndBeneficiaryClaims) and with a 256-run fuzz over arbitrary non-round start timestamps and periods.

reclaim requires block.timestamp >= lastPing + period + 365 days and msg.sender == depositor; claim remains valid for the beneficiary. Both routes call _close, which zeroes balance and sets closed, so the second transaction reverts with ClosedSwitch(id) and nothing is paid twice. The recovery deadline is computed from the latest lastPing and period, so a depositor cannot shorten it retroactively.

A beneficiary front-running reclaim at the boundary is the documented behaviour, not a bypass.

All seven mutating functions plus create share one nonReentrant guard (_guard 1->2). withdraw decrements balance and resets lastPing before _send; claim/reclaim call _close (balance=0, closed=true) before _send. A receiver that re-enters any mutator, on the same or another switch, gets ReentrantCall; views inside the callback already observe the settled state, so there is no stale-read window.

If the receiver reverts, the whole outer call reverts and the guard resets to 1, so a rejecting recipient cannot lock the contract.

ping, deposit, withdraw, setBeneficiary and setPeriod all pass through _activeDepositorSwitch, which reverts UnauthorizedDepositor for any msg.sender other than the recorded depositor, so nobody else can reset lastPing (including by depositing ETH). claim checks msg.sender == beneficiary and reclaim checks msg.sender == depositor.

There is no receive or fallback, so plain ETH cannot be pushed in to affect state, and a forced balance increase (SELFDESTRUCT from elsewhere) is not credited to any switch and never raises a payout.

withdraw is bounded by the per-id balance (amount > info.balance reverts InvalidAmount) and claim/reclaim pay exactly the per-id balance read before zeroing it. Balances are only credited by create and deposit with msg.value, so the contract balance always equals the sum of open balances under supported operations.

The invariant suite tracks per-id inflows/outflows independently across four actors and 24 switches with fail_on_revert, then reclaims every open switch and asserts a zero contract balance.

DeadMansSwitch declares constructor() {} (nonpayable, no parameters) and the manifest lists constructorArgs []. There is no $owner, $token or $contract reference and the source has no owner, admin, pause, upgrade, initializer, delegatecall or selfdestruct path, so no argument can confer a privileged role.

The token entry names LaunchToken with name Heartbeat, symbol BEAT and 18 decimals, matching the source constants; LaunchToken has no constructor arguments and mints exactly 10^27 to msg.sender. Pool fields (zero paired currency, fee 3000, tickSpacing 60, initialPrice 2^96) match the canonical guidance and initialPrice is below 2^256. Committed docs/abi/*.json are byte-equivalent to forge inspect output for both contracts.

The suite never calls claim/reclaim with to == address(this). Because the contract has no receive or fallback, the value call reverts, _send raises EtherTransferFailed, and the switch stays open and retryable. This is correct behaviour and only noted so the edge is on record; recipients that are precompiles behave the same way and are the caller's choice.