Implemented irrevocable, fully funded linear vesting with beneficiary-only claims, plus LaunchToken, vendored dependencies, and deployment documentation.

Verified with Solidity 0.8.26:

• forge build passed.
• forge test passed: 41 tests, including fuzzing and 8,192 invariant calls.
• forge fmt --check passed.

Assumptions, operating responsibilities, and one reviewed lint warning are documented in README.md.

Created launch.json matching LaunchToken and TokenVesting($token).

• Schema and constructor ABI checks passed.
• forge build passed with one existing lint warning.
• forge test: 41 passed.
• Only launch.json changed outside permitted scratch files.

Saved the review to .imd-findings.json.

• No substantiated defects in the assigned area.
• All five entry points covered.
• All 41 tests passed offline, including 8,192 invariant calls.
• Deployment token binding remains unverified because no launch manifest was present.

No source or configuration files changed.

No substantiated defects found in the assigned math and boundary scope.

Recorded findings and coverage for all five entry points in .imd-findings.json.

Validation passed: 41 existing tests, 8,192 invariant calls, and 83 additional arithmetic boundary tests run under /tmp. Source and configuration remain unchanged.

Saved .imd-findings.json with no substantiated defects and coverage for all five entry points.

All 41 existing tests and three additional economic tests passed, including 8,192 invariant calls. Production files remain unchanged. Final deployment verification lacked the required inputs.

The review is complete and the findings file is written at .imd-findings.json. The working tree is otherwise unchanged apart from the findings file, which git status shows as the only addition. Scratch tests and temporary downloads were removed.

Outcome: the vesting contract holds under the Execution Trace, Periphery and First Principles guides. I found no loss-of-funds, wrong-party payment, or accounting defect. One informational item is reported.

What I checked

• Execution trace of createSchedule. All five inputs are caller-controlled. Beneficiary, amount, duration, overflow of start plus duration, and cliff bounds are each guarded. The deposit is verified by exact balance delta, so a mismatched amount reverts. Schedule and totalLocked are written only after funding, under nonReentrant, so the Slither and Aderyn reentrancy leads need a token with callbacks, which the immutable plain LaunchToken does not have.
• Execution trace of claim. Id range and beneficiary checks run first. Vested is monotone in time and bounded by amount, and claimed never exceeds vested, so the subtraction cannot underflow. Both state writes precede the single transfer. I fuzzed monotonicity across the full timestamp range and independence of two schedules for one beneficiary.
• Periphery. I downloaded the OpenZeppelin v5.0.2 and forge-std v1.9.7 archives, confirmed their SHA-256 matches DEPENDENCIES.md, and diffed every vendored file. All differences are whitespace reflow from forge fmt. The vendored mulDiv, SafeERC20 and Address helpers are upstream code.
• First principles. Schedules are immutable and irrevocable since nothing writes them after creation except the claimed counter. The runtime contains no delegatecall, callcode or selfdestruct. The invariant campaign and my own tests show the contract balance always equals outstanding obligations plus donations.

Finding reported (info)

• createSchedule rejects address zero and the vesting contract as beneficiary, but accepts the token contract address. Such a schedule is created and funded, yet no caller can ever equal the token contract, so the deposit is permanently stranded. This is self-harm by the funder, so it is informational. The reproduction uses the exact call and the observed state at src/TokenVesting.sol:66.

Coverage. All five listed entry points have rows. Four hold, and createSchedule carries the info finding. Four additional rows record the invariants, the library verification, and the disposition of each static-analysis lead.

Test gaps worth noting for the author. The suite does not exercise a far-future start or a maximal duration with a realistic amount, both of which lock funds indefinitely by the funder's own choice. Those are documented in the README as unrecoverable mistakes and are not code defects.

Added eight tests covering failure paths, rounding, maximum timestamps, and irrevocability. Strengthened invariants with independent payout accounting and rejected calls across random sequences.

forge build and forge test pass: 49 tests, zero failures. New fuzz tests run 1,000 cases each; invariants run 256 × 64 calls.

Only test/ changed. No confirmed defects found.

Wrote .imd-findings.json with no retained findings and coverage for all five entry points.

All 49 existing tests and one scratch reproduction passed. The beneficiary-address case reproduced but was excluded as a funder input mistake affecting only their deposit. Scratch files were removed; implementation unchanged.