### View Halmos Counterexample Output

Source: https://www.soliditytestingbook.com/symbolic-testing

Example output from Halmos showing a failed test case with symbolic input values.

```text
Running 1 tests for test/symbolic/MiniPopsicleTest.t.sol:MiniPopsicleTest
Counterexample:
    p_depOld_uint64 = 0x4000000000000000
    p_depNew_uint64 = 0x4000000000000000
    p_feesPerShareIncrement_uint64 = 0x8000000000000000
    p_transferAmount_uint64 = 0x4000000000000000
[FAIL] check_transferDoesNotIncreaseTotalWorth(uint64,uint64,uint64,uint64) (paths: 13, time: 0.90s, bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 0.92s
```

--------------------------------

### Fuzz Test Example

Source: https://www.soliditytestingbook.com/advanced/invariant-tests

Demonstrates a stateless fuzz test targeting a single deposit function with randomized input.

```solidity
function testFuzz_Deposit(uint256 amount) public {
    vm.assume(amount > 0 && amount <= token.balanceOf(user));
    vm.prank(user);
    pool.deposit(amount);
    assertEq(pool.balanceOf(user), amount);
}
```

--------------------------------

### Observe symbolic testing output

Source: https://www.soliditytestingbook.com/symbolic-testing

Example output from a symbolic engine identifying the specific counterexample that triggers the assertion failure.

```text
Counterexample: 
    p_x_uint256_a611e6e_00 = 0x188e9f07e00f74
[FAIL] check_property(uint256) (paths: 3, time: 0.13s, bounds: [])
Symbolic test result: 0 passed; 1 failed; time: 0.15s
```

--------------------------------

### Vesting Contract Implementation

Source: https://www.soliditytestingbook.com/advanced/mutation-tests

Core functions for initializing, starting, pausing, and unpausing the vesting contract.

```solidity
// Vesting.sol
    function initialize(
        address _beneficiary,
        uint256 _vestingDuration
    ) external onlyOwner onlyInState(VestingState.Uninitialized) {
        // Validate input parameters
        if (_beneficiary == address(0)) {
            revert ZeroAddress();
        }
        if (_vestingDuration == 0) {
            revert ZeroDuration();
        }
        
        beneficiary = _beneficiary;
        vestingDuration = _vestingDuration;
        state = VestingState.Initialized;
        
        emit VestingInitialized(_beneficiary, _vestingDuration);
    }
    
    
    function startVesting() 
        external 
        onlyOwner 
        onlyInState(VestingState.Funded) 
    {
        vestingStart = block.timestamp;
        state = VestingState.Vesting;
    }
    
 ...
    
    function pause() external onlyOwner {
        if (paused) {
            revert AlreadyPaused();
        }
        paused = true;
        emit VestingPaused();
    }
    
    function unpause() external onlyOwner {
        if (!paused) {
            revert NotPaused();
        }
        paused = false;
        emit VestingUnpaused();
    }
```

--------------------------------

### Documenting Scenario Test Logic

Source: https://www.soliditytestingbook.com/advanced/scenario-tests

Example of using comments to explain complex state transitions and recovery paths in scenario tests.

```solidity
// Although the values here don't revert, if they were a bit higher, they would in the `getNextPaymentBreakdown` function.
// Currently, the way out of the situation would be to either:
// 1. Refinance using a custom fixedTermRefinancer that can manually alter the storage of the interest rate.
// 2. Close the loan, paying only the closing interest.
 
close(loan1);
 
// TotalAssets went down due to the loan closure.
assertEq(poolManager.totalAssets(), 4_000_000e6 + 90_000e6);  // 1% of 1_000_000e6, removing management fees
 
// Loan Manager should be in a coherent state
assertFixedTermLoanManager({
    loanManager:       loanManager,
    accruedInterest:   0,
    accountedInterest: 0,
    principalOut:      0,
    issuanceRate:      0,
    domainStart:       start + 800_000,
    domainEnd:         start + 800_000,
    unrealizedLosses:  0
});
```

--------------------------------

### Vulnerable createFund Implementation

Source: https://www.soliditytestingbook.com/formal-verification

Example of a contract function missing a critical security check.

```solidity
function createFund(uint256 fundId) public {
    require(msg.sender != address(0));
    require(funds[fundId].currentManager == address(0));
    // BUG: Missing this check!
    // require(!isActiveManager(msg.sender));
    funds[fundId].currentManager = msg.sender;
    _isActiveManager[msg.sender] = true;
}
```

--------------------------------

### Mutation Testing Report Output

Source: https://www.soliditytestingbook.com/advanced/mutation-tests

Example output showing surviving mutants in the contract code.

```text
Mutation testing report:
Number of mutations:    15
Killed:                12 (80.00%)
Survived:              2 (20.00%)
Runtime:               8.12 seconds
Mutations:
 
 
[+] Survivors
 * Mutation:
    File: /solidity-testing-book/examples/src/Vesting.sol
    Line nr: 163
    Result: Lived
    Original line:
             function pause() external onlyOwner {
 
    Mutated line:
             function pause() external  {
 
Mutation:
    File: /solidity-testing-book/examples/src/Vesting.sol
    Line nr: 171
    Result: Lived
    Original line:
             function unpause() external onlyOwner {
 
    Mutated line:
             function unpause() external  {
```

--------------------------------

### Symbolic Execution Example Function

Source: https://www.soliditytestingbook.com/symbolic-testing

A simple function used to demonstrate how symbolic execution explores branches and identifies counterexamples.

```solidity
function foobar(int a, int b) public pure {
    int x = 1;
    int y = 0;
    if (a != 0) {
        y = 3 + x;      // y = 4
        if (b == 0) {
            x = 2 * (a + b);
        }
    }
    assert(x - y != 0);
}
```

--------------------------------

### Invariant Test Example

Source: https://www.soliditytestingbook.com/advanced/invariant-tests

Demonstrates a stateful invariant test verifying that the total supply matches the sum of all user balances.

```solidity
function invariant_totalSupplyEqualsSumOfBalances() public {
    uint256 totalSupply = token.totalSupply();
    uint256 sumOfBalances = 0;
    for (uint256 i = 0; i < users.length; i++) {
        sumOfBalances += token.balanceOf(users[i]);
    }
    assertEq(totalSupply, sumOfBalances);
}
```

--------------------------------

### Example of Invalid Implementation

Source: https://www.soliditytestingbook.com/basic/unit-tests

A dummy implementation of a setter that would pass the basic test despite not performing the intended logic.

```solidity
uint256 public number = 10
function setNumber(uint256 value) public {}
```

--------------------------------

### Fetch RPC URL with mesc and Configure Forks

Source: https://www.soliditytestingbook.com/basic/fork-tests

Utility function to retrieve RPC URLs via the mesc CLI tool and a setup function demonstrating multi-chain fork selection.

```solidity
   function fetchRpcUrlFromMesc(string memory networkName) internal returns (string memory url) {
       string[] memory inputs = new string[](3);
       inputs[0] = "mesc";
       inputs[1] = "url";
       inputs[2] = networkName;
 
       bytes memory res = vm.ffi(inputs);
       url = string(res);
   }
 
   function setUp() public {
       string memory network = "avax-c-chain";
       uint256 cchainForkId = vm.createSelectFork(fetchRpcUrlFromMesc(network), 41022344);
       network = "eth-mainnet";
       uint256 mainnetForkId = vm.createSelectFork(fetchRpcUrlFromMesc(network), 19120056);
       // Do something
    }
```

--------------------------------

### Traditional Solidity test functions

Source: https://www.soliditytestingbook.com/advanced/scenario-test-runner

Standard Foundry test functions demonstrating repetitive setup and action patterns.

```solidity
function test_Scenario_MultipleUsersCompetingForLiquidity() public {
    // Setup initial state
    vm.startPrank(user1);
    token.approve(address(lending), 500 ether);
    lending.deposit(500 ether);
    vm.stopPrank();
 
    vm.startPrank(user2);
    token.approve(address(lending), 300 ether);
    lending.deposit(300 ether);
    vm.stopPrank();
 
    // More actions...
}
 
function test_Scenario_CascadingLiquidations() public {
    // Different but similar setup
    vm.startPrank(user1);
    token.approve(address(lending), 500 ether);
    lending.deposit(500 ether);
    vm.stopPrank();
 
    // More actions...
}
```

--------------------------------

### Observe fuzzer output

Source: https://www.soliditytestingbook.com/symbolic-testing

Example output from a fuzzer showing a passing result despite the presence of an unreachable assertion.

```text
[PASS] testFuzz_check(uint256) (runs: 256, μ: 9204, ~: 9204)
Suite result: ok. 1 passed; 0 failed; 0 skipped; finished in 14.26ms (9.85ms CPU time)
```

--------------------------------

### View Revert Trace in Foundry

Source: https://www.soliditytestingbook.com/basic/fork-tests

Example of a failed transaction trace showing an ERC20 transfer revert during a fork test.

```text
    │   │   ├─ [8384] 0xA0b86991c6218b36c1d19D4a2e9Eb0cE3606eB48::transferFrom(LiquidityAdder: [0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f], 0xB4e16d0168e52d35CaCD2c6185b44281Ec28C9Dc, 1000000000 [1e9])
    │   │   │   ├─ [7573] 0x43506849D7C04F9138D1A2050bbF3A0c054402dd::transferFrom(LiquidityAdder: [0x5615dEB798BB3E4dFa0139dFa1b3D433Cc23b72f], 0xB4e16d0168e52d35CaCD2c6185b44281Ec28C9Dc, 1000000000 [1e9]) [delegatecall]
    │   │   │   │   └─ ← [Revert] revert: ERC20: transfer amount exceeds allowance
    │   │   │   └─ ← [Revert] revert: ERC20: transfer amount exceeds allowance
    │   │   └─ ← [Revert] revert: TransferHelper: TRANSFER_FROM_FAILED
    │   └─ ← [Revert] revert: TransferHelper: TRANSFER_FROM_FAILED
    └─ ← [Revert] revert: TransferHelper: TRANSFER_FROM_FAILED
```

--------------------------------

### Define Scenario Test Cases in JSON

Source: https://www.soliditytestingbook.com/advanced/scenario-test-runner

Examples of JSON structures used to define test scenarios, including market stress tests and bug reproduction steps.

```json
{
  "description": "Market stress test - Multiple users competing for liquidity",
  "actions": [
    {
      "action": "deposit",
      "caller": "user1",
      "params": { "amount": "500000000000000000000" }
    },
    // ... more actions ...
  ]
}
```

```json
{
  "description": "Bug #123 - Liquidation during price recovery",
  "actions": [
    // Steps to reproduce the bug
  ],
  "expectedFinalState": {
    // The correct state after fix
  }
}
```

--------------------------------

### Implement SampleLending and MockToken contracts

Source: https://www.soliditytestingbook.com/basic/fuzz-tests

A simplified lending protocol and a mock ERC20 token used to demonstrate interest calculation and repayment logic.

```solidity
contract SampleLending {
    uint256 public constant FEE_PERCENTAGE = 1000; // 10%
    address public feeReceiver;
 
    constructor(address _feeReceiver) {
        feeReceiver = _feeReceiver;
    }
 
    function calculateInterest(uint256 principal, uint256 rate, uint256 time) public pure returns (uint256 interest, uint256 fees) {
        interest = (rate * principal * time) / 10000 / 365 days;
        fees = (FEE_PERCENTAGE * interest) / 10000;
        interest -= fees;
    }
 
    function repay(address token, uint256 principal, uint256 rate, uint256 time) external {
        (uint256 interest, uint256 fees) = calculateInterest(principal, rate, time);
        IERC20(token).transferFrom(msg.sender, feeReceiver, fees);
    }
}
 
contract MockToken {
    mapping(address => uint256) private _balances;
    mapping(address => mapping(address => uint256)) private _allowances;
 
    function mint(address account, uint256 amount) external {
        _balances[account] += amount;
    }
 
    function transferFrom(address sender, address recipient, uint256 amount) external returns (bool) {
        require(amount > 0, "Cannot transfer zero tokens");
        require(_balances[sender] >= amount, "Insufficient balance");
        require(_allowances[sender][msg.sender] >= amount, "Insufficient allowance");
 
        _balances[sender] -= amount;
        _balances[recipient] += amount;
        _allowances[sender][msg.sender] -= amount;
        return true;
    }
 }
```

--------------------------------

### Initiate Certora Run

Source: https://www.soliditytestingbook.com/formal-verification

Command to execute the verification process using a configuration file.

```bash
certoraRun ManagerBug1.conf
```

--------------------------------

### Implement LendingProtocol Contract

Source: https://www.soliditytestingbook.com/advanced/invariant-tests

A basic lending protocol contract allowing users to deposit tokens and borrow against them with an 80% collateral factor.

```solidity
contract LendingProtocol {
    mapping(address => uint256) public deposits;
    mapping(address => uint256) public borrows;
    IERC20 public token;
    uint256 public constant COLLATERAL_FACTOR = 80; // 80% collateral factor
    uint256 public totalDeposits;
    uint256 public totalBorrows;
 
    constructor(address _token) {
        token = IERC20(_token);
    }
 
    function deposit(uint256 amount) external {
        require(token.transferFrom(msg.sender, address(this), amount), "Transfer failed");
        deposits[msg.sender] += amount;
        totalDeposits += amount;
    }
 
    function borrow(uint256 amount) external {
        uint256 maxBorrow = (deposits[msg.sender] * COLLATERAL_FACTOR) / 100;
        require(borrows[msg.sender] + amount <= maxBorrow, "Exceeds borrow limit");
        borrows[msg.sender] += amount;
        totalBorrows += amount;
        require(token.transfer(msg.sender, amount), "Transfer failed");
    }
 
    function repay(uint256 amount) external {
        require(token.transferFrom(msg.sender, address(this), amount), "Transfer failed");
        uint256 actualRepayment = amount > borrows[msg.sender] ? borrows[msg.sender] : amount;
        borrows[msg.sender] -= actualRepayment;
        totalBorrows -= actualRepayment;
        if (amount > actualRepayment) {
            uint256 excess = amount - actualRepayment;
            deposits[msg.sender] += excess;
            totalDeposits += excess;
        }
    }
 
    function withdraw(uint256 amount) external {
        require(deposits[msg.sender] > 0, "No deposits");
        uint256 requiredCollateral = (borrows[msg.sender] * 100) / COLLATERAL_FACTOR;
        require(deposits[msg.sender] >= requiredCollateral, "insufficient collateral");
        
        uint256 availableToWithdraw = deposits[msg.sender] - requiredCollateral;
        uint256 actualWithdrawal = amount > availableToWithdraw ? availableToWithdraw : amount;
        
        require(actualWithdrawal > 0, "insufficient funds");
        
        deposits[msg.sender] -= actualWithdrawal;
        totalDeposits -= actualWithdrawal;
        require(token.transfer(msg.sender, actualWithdrawal), "Transfer failed");
    }
}
```

--------------------------------

### Implement Realistic Market Scenarios

Source: https://www.soliditytestingbook.com/advanced/scenario-tests

Avoid setting unrealistic price values; instead, simulate gradual market movements to test system behavior.

```solidity
// WRONG: Oversimplified market crash scenario
lending.setPrice(0 ether);  // Unrealistic
 
// RIGHT: Realistic market movement
lending.setPrice(0.8 ether);  // 20% drop
// Test system behavior
lending.setPrice(0.6 ether);  // Further 20% drop
// Test system behavior again
```

--------------------------------

### LiquidityAdder Contract Implementation

Source: https://www.soliditytestingbook.com/basic/fork-tests

A simple contract that interacts with the Uniswap V2 router to add liquidity.

```solidity
contract LiquidityAdder {
    IUniswapV2Router02 public uniswapRouter;
 
    constructor(address _uniswapRouter) {
        uniswapRouter = IUniswapV2Router02(_uniswapRouter);
    }
 
    function addLiquidity(
        address tokenA,
        address tokenB,
        uint amountADesired,
        uint amountBDesired
    ) external returns (uint amountA, uint amountB, uint liquidity) {
        IERC20(tokenA).transferFrom(msg.sender, address(this), amountADesired);
        IERC20(tokenB).transferFrom(msg.sender, address(this), amountBDesired);
 
        IERC20(tokenA).approve(address(uniswapRouter), amountADesired);
        IERC20(tokenB).approve(address(uniswapRouter), amountBDesired);
 
        return uniswapRouter.addLiquidity(
            tokenA,
            tokenB,
            amountADesired,
            amountBDesired,
            0,
            0,
            msg.sender,
            block.timestamp
        );
    }
}
```

--------------------------------

### Unit Test with Mocks

Source: https://www.soliditytestingbook.com/basic/fork-tests

A unit test for LiquidityAdder that uses vm.mockCall to simulate external contract interactions.

```solidity
contract LiquidityAdderTest is Test {
    LiquidityAdder liquidityAdder;
    address constant UNISWAP_ROUTER = address(0xdeadbeef);
 
    function setUp() public {
        liquidityAdder = new LiquidityAdder(UNISWAP_ROUTER);
    }
 
    function testAddLiquidityMock() public {
        address tokenA = address(0x1);
        address tokenB = address(0x2);
        
        // Mock token transfers
        vm.mockCall(
            tokenA,
            abi.encodeWithSelector(IERC20.transferFrom.selector),
            abi.encode(true)
        );
        vm.mockCall(
            tokenB,
            abi.encodeWithSelector(IERC20.transferFrom.selector),
            abi.encode(true)
        );

        // Mock the addLiquidity function call
        vm.mockCall(
            UNISWAP_ROUTER,
            abi.encodeWithSelector(IUniswapV2Router02.addLiquidity.selector),
            abi.encode(1000, 1000, 1000)
        );
        
        (uint amountA, uint amountB, uint liquidity) = liquidityAdder.addLiquidity(tokenA, tokenB, 1000, 1000);
        
        assertEq(amountA, 1000);
        assertEq(amountB, 1000);
        assertEq(liquidity, 1000);
    }
}
```

--------------------------------

### Generate Scenarios Programmatically

Source: https://www.soliditytestingbook.com/advanced/scenario-test-runner

Demonstrates how to iterate through data sets to generate multiple test scenarios dynamically.

```solidity
function generateStressScenarios() public {
    uint256[] memory prices = [1e18, 0.9e18, 0.8e18, 0.7e18];
    for(uint i = 0; i < prices.length; i++) {
        generateScenario(prices[i]);
    }
}
```

--------------------------------

### Validating State Transitions with Helpers

Source: https://www.soliditytestingbook.com/advanced/scenario-tests

Helper function pattern for verifying user positions and system state during scenario tests.

```solidity
// Create helper functions to verify system state
function verifyUserPosition(
    address user,
    uint256 expectedDeposit,
    uint256 expectedBorrow
) internal {
    assertEq(lending.deposits(user), expectedDeposit);
    assertEq(lending.borrows(user), expectedBorrow);
    // Add other relevant checks
}
```

--------------------------------

### Invariant Test Failure Output

Source: https://www.soliditytestingbook.com/advanced/invariant-tests

Example of a failed invariant test log showing the sequence of calls and the specific error encountered.

```text
[FAIL: <empty revert data>]
	 [Sequence]
        sender=0x00000000000000000000002eA38b54cE5a819AF6 addr=[test/invariant/Invariant.t.sol:Handler]0xF62849F9A0B5Bf2913b396098F7c7019b51A820a calldata=deposit(uint256) args=[268086407878502856564320633721989845494868808503440654 [2.68e53]]
        sender=0x00000000000000000000002eA38b54cE5a819AF6 addr=[test/invariant/Invariant.t.sol:Handler]0xF62849F9A0B5Bf2913b396098F7c7019b51A820a calldata=borrow(uint256) args=[1083181390655043523035 [1.083e21]
        sender=0x0000000000000000000000000000000000657374 addr=[test/invariant/Invariant.t.sol:Handler]0xF62849F9A0B5Bf2913b396098F7c7019b51A820a calldata=deposit(uint256) args=[149284093665934295474410336178711275202335643493951105 [1.492e53]]
        sender=0x00000000000000000000002eA38b54cE5a819AF6 addr=[test/invariant/Invariant.t.sol:Handler]0xF62849F9A0B5Bf2913b396098F7c7019b51A820a calldata=withdraw(uint256) args=[2442579456253310227425442841 [2.442e27]]
 invariant_userCollateralAlwaysSufficient() (runs: 1, calls: 1, reverts: 1)
Logs:
  Error: INVARIANT_INSUFFICIENT_COLLATERAL
  Error: a >= b not satisfied [uint]
    Value a: 262567983659900320649
    Value b: 508481869510300963140
```

--------------------------------

### Fuzz Test Failure Output

Source: https://www.soliditytestingbook.com/basic/fuzz-tests

Example of a console output showing a failed fuzz test due to a zero-value transfer revert.

```text
[FAIL. Reason: revert: Cannot transfer zero tokens; counterexample: calldata=0x92d09fa000000000000000000000000000000000000000000000000000000000000003b1000000000000000000000000000000000000000000000000000000000000028f0000000000000000000000000000000000000000000000000000000000001613 args=[945, 655, 5651]] testFuzz_Repayment(uint256,uint256,uint256) (runs: 0, μ: 0, ~: 0)
Logs:
  Principal: 945
  Rate: 655
  Time: 5651
  Fees: 0
  Interest: 0
```

--------------------------------

### Run Vertigo Mutation Tests

Source: https://www.soliditytestingbook.com/advanced/mutation-tests

Command to execute the mutation testing suite.

```bash
vertigo run
```

--------------------------------

### Avoid Redundant Overflow Testing

Source: https://www.soliditytestingbook.com/basic/unit-tests

Example of a test that attempts to trigger overflow, which is unnecessary due to Solidity's default compiler protections.

```solidity
   function testFail_setNumber() public {
        cut.setNumber(type(uint256).max + 1);
    }
```

--------------------------------

### Invariant Test for uniqueManagers

Source: https://www.soliditytestingbook.com/formal-verification

An example of an invariant test structure that struggles to verify uniqueness due to the lack of knowledge regarding existing fund IDs.

```solidity
function invariant_uniqueManagers() public {
    // How do you even express this?
    // You'd need to iterate all funds and check uniqueness
    // But you don't know which fundIds exist
}
```

--------------------------------

### Run Verification with Invariant

Source: https://www.soliditytestingbook.com/formal-verification

Command to run the prover against the updated specification.

```bash
certoraRun Manager.v2.conf
```

--------------------------------

### Certora Configuration File

Source: https://www.soliditytestingbook.com/formal-verification

Defines the verification parameters for the Certora prover.

```JSON
{
    "files": [
        "ManagerBug.sol"
    ],
    "verify": "Manager:Manager.v1.spec",
    "wait_for_results": "all",
    "rule_sanity": "basic",
    "msg": "Funds managers verification"
}
```

--------------------------------

### Implement Time-Aware Lifecycle Tests

Source: https://www.soliditytestingbook.com/advanced/lifecycle-tests

Use vm.warp to simulate time progression and verify time-sensitive contract logic.

```solidity
contract TimeAwareLifecycleTest is Test {
    // Define time constants clearly
    uint256 constant DAY = 1 days;
    uint256 constant YEAR = 365 days;
 
    function test_TimeProgression() public {
        // Start from a known timestamp
        vm.warp(1672531200); // Jan 1, 2023
 
        // Use relative time movements
        vm.warp(block.timestamp + 180 days);
 
        // Check time-sensitive calculations
        assertEq(
            vesting.vestedAmount(),
            expectedAmount,
            "Incorrect vesting calculation"
        );
    }
 
    // Test time boundaries
    function test_TimeBoundaries() public {
        // Test at exact boundaries
        vm.warp(vestingStart);
        vm.warp(vestingStart + vestingDuration - 1);
        vm.warp(vestingStart + vestingDuration);
    }
}
```

--------------------------------

### Implement Vesting Contract Lifecycle

Source: https://www.soliditytestingbook.com/advanced/lifecycle-tests

A state-machine based vesting contract that tracks progress through five distinct phases from initialization to completion.

```solidity
contract Vesting is Ownable {
 
    // Core storage variables
    IERC20 public token;
    address public beneficiary;
    uint256 public vestingStart;
    uint256 public vestingDuration;
    uint256 public totalAmount;
    uint256 public releasedAmount;
    VestingState public state;
    bool public paused;
 
     enum VestingState {
        Uninitialized,
        Initialized,
        Funded,
        Vesting,
        Completed
    }
 
    // Modifiers for common state checks
    modifier onlyInState(VestingState requiredState) {
        if (state != requiredState) {
            revert InvalidState(state, requiredState);
        }
        _;
    }
 
    function initialize(
        address _beneficiary,
        uint256 _vestingDuration
    ) external onlyOwner onlyInState(VestingState.Uninitialized) {
        // Validate input parameters
        if (_beneficiary == address(0)) {
            revert ZeroAddress();
        }
        if (_vestingDuration == 0) {
            revert ZeroDuration();
        }

        beneficiary = _beneficiary;
        vestingDuration = _vestingDuration;
        state = VestingState.Initialized;

        emit VestingInitialized(_beneficiary, _vestingDuration);
    }

    function fund(
        IERC20 _token,
        uint256 _amount
    ) external onlyOwner onlyInState(VestingState.Initialized) {
        if (_amount == 0) {
            revert ZeroAmount();
        }

        token = _token;
        totalAmount = _amount;

        // Attempt token transfer
        bool success = token.transferFrom(msg.sender, address(this), _amount);
        if (!success) {
            revert TransferFailed();
        }

        state = VestingState.Funded;
        emit VestingFunded(_amount);
    }

    function startVesting()
        external
        onlyOwner
        onlyInState(VestingState.Funded)
    {
        vestingStart = block.timestamp;
        state = VestingState.Vesting;
    }

    function vestedAmount() public view returns (uint256) {
        if (state != VestingState.Vesting) {
            return 0;
        }

        if (block.timestamp >= vestingStart + vestingDuration) {
            return totalAmount;
        }

        return (totalAmount * (block.timestamp - vestingStart)) / vestingDuration;
    }

    function claim() external whenNotPaused onlyBeneficiary {
        if (state != VestingState.Vesting) {
            revert InvalidState(state, VestingState.Vesting);
        }

        if (block.timestamp <= vestingStart) {
            revert VestingNotStarted();
        }

        uint256 vested = vestedAmount();
        uint256 claimable = vested - releasedAmount;

        if (claimable == 0) {
            revert NoTokensAvailable();
        }

        releasedAmount += claimable;
        bool success = token.transfer(beneficiary, claimable);
        if (!success) {
            revert TransferFailed();
        }

        emit TokensReleased(claimable);

        // Check if vesting is complete
        if (releasedAmount == totalAmount) {
            state = VestingState.Completed;
            emit VestingCompleted();
        }
    }
...
}
```

--------------------------------

### Test getNumber method

Source: https://www.soliditytestingbook.com/basic/unit-tests

Demonstrates simple and robust approaches to testing a getter method in Solidity.

```solidity
   function test_getNumber_Simple() public {
        getterSetter.setNumber(10);
        assertEq(getterSetter.getNumber(), 10);
    }
```

```solidity
    function test_getNumber_Robust() public {
        getterSetter.setNumber(322e26);
        assertEq(getterSetter.getNumber(), 322e26);
        assertEq(getterSetter.getNumber(), getterSetter.number());
 
        getterSetter.setNumber(0);
        assertEq(getterSetter.getNumber(), 0);
        assertEq(getterSetter.getNumber(), getterSetter.number());
    }
```

--------------------------------

### Perform Complete State Verification

Source: https://www.soliditytestingbook.com/advanced/scenario-tests

Verify the entire system state after scenario execution rather than checking only a single variable.

```solidity
// WRONG: Partial verification
function test_Scenario() public {
    // Execute scenario
    assertEq(lending.borrows(user), expectedBorrow);
}
 
// RIGHT: Complete verification
function test_Scenario() public {
    // Execute scenario
    verifySystemState({
        userBorrow: expectedBorrow,
        totalBorrows: expectedTotalBorrows,
        userDeposit: expectedDeposit,
        totalDeposits: expectedTotalDeposits
    });
}
```

--------------------------------

### Lending Contract Scenario Tests

Source: https://www.soliditytestingbook.com/advanced/scenario-tests

A comprehensive test suite using Foundry to validate lending contract behavior under various market and user conditions.

```Solidity
contract LendingScenarioTest is Test {
    LendingWithLiquidation public lending;
    MockERC20 public token;
    address public user1;
    address public user2;
    address public liquidator;
 
    function setUp() public {
        token = new MockERC20("Mock Token", "MTK");
        lending = new LendingWithLiquidation(address(token));
        user1 = address(0x1);
        user2 = address(0x2);
        liquidator = address(0x3);
        
        // Initial setup for all users
        token.mint(user1, 1000 ether);
        token.mint(user2, 1000 ether);
        token.mint(liquidator, 1000 ether);
    }
 
    function test_Scenario_MultipleUsersCompetingForLiquidity() public {
        // Scenario: Two users deposit and try to borrow when there's limited liquidity
        
        // User1 deposits
        vm.startPrank(user1);
        token.approve(address(lending), 500 ether);
        lending.deposit(500 ether);
        vm.stopPrank();
 
        // User2 deposits
        vm.startPrank(user2);
        token.approve(address(lending), 300 ether);
        lending.deposit(300 ether);
        vm.stopPrank();
 
        // User1 borrows first
        vm.prank(user1);
        lending.borrow(400 ether);
 
        // User2 attempts to borrow
        vm.startPrank(user2);
        lending.borrow(240 ether);  // Should succeed (80% of 300)
        
        // Try to borrow more - should fail
        vm.expectRevert("Exceeds borrow limit");
        lending.borrow(1 ether);
        vm.stopPrank();
 
        assertEq(lending.borrows(user1), 400 ether);
        assertEq(lending.borrows(user2), 240 ether);
    }
 
    function test_Scenario_CascadingLiquidations() public {
        // Scenario: Multiple positions become liquidatable due to rapid price decline
        
        // Setup initial positions
        vm.startPrank(user1);
        token.approve(address(lending), 500 ether);
        lending.deposit(500 ether);
        lending.borrow(350 ether);  // 70% utilization
        vm.stopPrank();
 
        vm.startPrank(user2);
        token.approve(address(lending), 300 ether);
        lending.deposit(300 ether);
        lending.borrow(210 ether);  // 70% utilization
        vm.stopPrank();
 
        // Simulate market crash
        lending.setPrice(0.7 ether);  // 30% price drop
 
        // Liquidator starts liquidating positions
        vm.startPrank(liquidator);
        token.approve(address(lending), 1000 ether);
        
        uint256 liquidatorInitialBalance = token.balanceOf(liquidator);
        
        lending.liquidate(user1, 100 ether);
        lending.liquidate(user2, 60 ether);
        vm.stopPrank();
 
        // Verify liquidations
        assertLt(lending.borrows(user1), 350 ether);
        assertLt(lending.borrows(user2), 210 ether);
        assertGt(token.balanceOf(liquidator), liquidatorInitialBalance);
    }
 
    function test_Scenario_RepayDuringLiquidation() public {
        // Scenario: User attempts to repay while being liquidated
        
        // Setup user's position
        vm.startPrank(user1);
        token.approve(address(lending), 1000 ether);
        lending.deposit(1000 ether);
        lending.borrow(700 ether);  // 70% utilization
        vm.stopPrank();
 
        // Make position liquidatable
        lending.setPrice(0.75 ether);
 
        // Start liquidation
        vm.startPrank(liquidator);
        token.approve(address(lending), 300 ether);
        lending.liquidate(user1, 300 ether);
        vm.stopPrank();
 
        // User attempts to repay during liquidation
        vm.startPrank(user1);
        token.approve(address(lending), 200 ether);
        lending.repay(200 ether);
        vm.stopPrank();
 
        // Verify final state
        uint256 finalBorrow = lending.borrows(user1);
        assertLt(finalBorrow, 700 ether);
        assertGt(finalBorrow, 0);
    }
 
    function test_Scenario_MarketRecovery() public {
        // Scenario: Price recovers after partial liquidation
        
        // Setup initial position
        vm.startPrank(user1);
        token.approve(address(lending), 1000 ether);
        lending.deposit(1000 ether);
        lending.borrow(700 ether);
        vm.stopPrank();
 
        // Price drops and liquidation occurs
        lending.setPrice(0.75 ether);
        
        vm.startPrank(liquidator);
        token.approve(address(lending), 200 ether);
        lending.liquidate(user1, 200 ether);
        vm.stopPrank();
 
        // Price recovers
        lending.setPrice(1 ether);
 
        // User should be able to borrow again
        vm.startPrank(user1);
        uint256 borrowBefore = lending.borrows(user1);
        lending.borrow(100 ether);
        assertEq(lending.borrows(user1), borrowBefore + 100 ether);
        vm.stopPrank();
    }
}
```

--------------------------------

### Constrain inputs for symbolic testing

Source: https://www.soliditytestingbook.com/symbolic-testing

Use vm.assume to enforce logical preconditions and prevent overflows during symbolic execution.

```solidity
function check_withdrawal(uint256 amount, uint256 userBalance) public {
    // Prevent expected reverts
    vm.assume(amount > 0);
    vm.assume(userBalance > 0);
    
    // Prevent overflow in calculations
    vm.assume(amount < type(uint128).max);
    vm.assume(userBalance < type(uint128).max);
    
    // Logical preconditions
    vm.assume(amount <= userBalance);
    
    // assert
    vault.withdraw(amount);
    assert(vault.totalSupply() >= 0);
}
```

--------------------------------

### Implement an Action Handler in Solidity

Source: https://www.soliditytestingbook.com/advanced/scenario-test-runner

Defines a function to handle specific actions like deposits by interacting with the address book and performing token operations.

```solidity
function handleDeposit(string memory caller, uint256 amount) internal {
    address callerAddr = addressBook[caller];
    
    // Handle token approval and deposit
    vm.startPrank(callerAddr);
    token.approve(address(lending), amount);
    lending.deposit(amount);
    vm.stopPrank();
    
    console.log("Deposit processed:", amount);
}
```

--------------------------------

### Token Vesting Lifecycle Test Structure

Source: https://www.soliditytestingbook.com/advanced/lifecycle-tests

A template for structuring lifecycle tests in Solidity, emphasizing documentation of phases and assumptions.

```solidity
/// @title Token Vesting Lifecycle Tests
/// @notice Comprehensive tests for token vesting lifecycle
/// @dev These tests verify the complete contract lifecycle
contract TokenVestingLifecycleTest is Test {
 
    /// @dev This test progresses through all contract phases
    function test_DetailedLifecycle() public {
        // PHASE 1: Initialization
        /* Detailed explanation of what's being tested and why */
 
        // PHASE 2: Funding
        /* Clear documentation of test progression */
 
        // Clearly document assumptions
        // Document edge cases and why they matter
    }
}
```

--------------------------------

### Time Manipulation Best Practices

Source: https://www.soliditytestingbook.com/advanced/lifecycle-tests

Avoid hardcoded timestamps in favor of relative time manipulation to ensure test portability.

```solidity
// WRONG: Hardcoded timestamps
vm.warp(1672531200);
 
// RIGHT: Relative time manipulation
vm.warp(block.timestamp + YEAR);
```

--------------------------------

### Execute unit test for repayment

Source: https://www.soliditytestingbook.com/basic/fuzz-tests

A standard unit test verifying the happy path for the repayment function.

```solidity
function testRepayment() public {
    uint256 principal = 1000 ether;
    uint256 rate = 1000; // 10% APR
    uint256 time = 30 days;
 
    (uint256 interest, uint256 fees) = protocol.calculateInterest(principal, rate, time);
    assertGt(fees, 0, "Fees should be greater than zero");
 
    vm.startPrank(address(this));
    token.mint(address(this), fees);
    token.approve(address(protocol), type(uint256).max);
    protocol.repay(address(token), principal, rate, time);
    vm.stopPrank();
}
```

--------------------------------

### Define a BTT specification

Source: https://www.soliditytestingbook.com/branching-tree-technique

A .tree file defines the hierarchical structure of test cases, representing conditions and expected outcomes.

```text
FooTest
└── When stuff is called
    └── When a condition is met
        └── It should revert.
            └── Because we shouldn't allow it.
```

--------------------------------

### Structure Complex Lifecycle Tests

Source: https://www.soliditytestingbook.com/advanced/lifecycle-tests

Organize tests by breaking down scenarios, using modifiers for prerequisites, and parameterizing inputs.

```solidity
contract ComplexLifecycleTest is Test {
    // Break down complex scenarios into smaller, focused tests
    function test_VestingSchedule_LinearVesting() public {
        // Test basic linear vesting
    }
 
    function test_VestingSchedule_WithCliff() public {
        // Test vesting with cliff period
    }
 
    // Use modifiers to enforce test prerequisites
    modifier withFundedContract() {
        _setupFundedState();
        _;
    }
 
    // Parameterize tests for different scenarios
    function test_VestingCalculation(uint256 timeElapsed) public {
        vm.assume(timeElapsed <= vestingDuration);
        // Test calculation with different time periods
    }
}
```

--------------------------------

### Simulate a Buggy Function Implementation

Source: https://www.soliditytestingbook.com/formal-verification

Demonstrates a faulty implementation where a function incorrectly modifies the current manager state instead of the pending manager.

```Solidity
// Buggy setPendingManager
function setPendingManager(uint256 fundId, address pending) public {
    require(funds[fundId].currentManager == msg.sender);
    // BUG: Accidentally setting currentManager instead of pendingManager
    funds[fundId].currentManager = pending;  
    funds[fundId].pendingManager = pending;
}
```

--------------------------------

### Mocking external calls in unit tests

Source: https://www.soliditytestingbook.com/basic/unit-tests

Shows how to isolate contract logic by mocking external ERC20 transfers using vm.mockCall.

```solidity
function deposit(uint256 _amount) external {
        require(token.transferFrom(msg.sender, address(this), _amount), "Transfer failed");
        balances[msg.sender] += _amount;
    }
```

```solidity
// Vault.t.sol
contract VaultTest is Test {
...
address tokenA = makeAddr("TokenA");
...
 
function test_deposit() external {
    vm.mockCall(address(tokenA), abi.encodeWithSelector(IERC20.transferFrom.selector), abi.encode(true));
    vault.deposit(10);
    assert(vault.balances(address(this))== 10);
  }
}
```

--------------------------------

### Original Repayment Function

Source: https://www.soliditytestingbook.com/basic/fuzz-tests

The vulnerable implementation that attempts to transfer fees even when they are zero.

```solidity
function repay(address token, uint256 principal, uint256 rate, uint256 time) external {
    (uint256 interest, uint256 fees) = calculateInterest(principal, rate, time);
    IERC20(token).transferFrom(msg.sender, feeReceiver, fees);
}
```

--------------------------------

### Lending Protocol Lifecycle Test in Foundry

Source: https://www.soliditytestingbook.com/advanced/lifecycle-tests

A comprehensive test function that simulates a full user journey through a lending protocol, including edge cases like failed borrows and liquidations.

```solidity
    function testLendingLifecycle() public {
      console.log("Step 1: User deposits tokens");
      vm.startPrank(user);
      token.approve(address(lending), 1000 ether);
      lending.deposit(1000 ether);
      vm.stopPrank();
 
      assertEq(lending.deposits(user), 1000 ether);
      assertEq(lending.totalDeposits(), 1000 ether);
 
      console.log("Step 2: User borrows against collateral");
      vm.prank(user);
      lending.borrow(700 ether);
 
      assertEq(lending.borrows(user), 700 ether);
      assertEq(lending.totalBorrows(), 700 ether);
 
      console.log("Step 3: Attempt to borrow more than allowed");
      vm.expectRevert("Exceeds borrow limit");
      vm.startPrank(user);
      lending.borrow(150 ether);
      vm.stopPrank();
 
      console.log("Step 4: Partial repayment");
      vm.startPrank(user);
      token.approve(address(lending), 200 ether);
      lending.repay(200 ether);
      vm.stopPrank();
 
      assertEq(lending.borrows(user), 500 ether);
      assertEq(lending.totalBorrows(), 500 ether);
 
      console.log("Step 5: Withdraw some funds");
      vm.prank(user);
      lending.withdraw(100 ether);
 
      assertEq(lending.deposits(user), 900 ether);
      assertEq(lending.totalDeposits(), 900 ether);
 
      console.log("Step 6: Set up for liquidation");
      vm.prank(user);
      lending.borrow(200 ether);
 
      assertEq(lending.borrows(user), 700 ether);
 
      console.log("Step 7: Price drop, making the position liquidatable");
      lending.setPrice(0.8 ether); // 20% price drop
 
      console.log("Step 8: Liquidator attempts to liquidate");
      uint256 liquidatorBalanceBefore = token.balanceOf(liquidator);
      vm.startPrank(liquidator);
      token.approve(address(lending), 300 ether);
      lending.liquidate(user, 300 ether);
      vm.stopPrank();
      uint256 liquidatorBalanceAfter = token.balanceOf(liquidator);
 
      assertLt(lending.borrows(user), 700 ether);
      assertLt(lending.deposits(user), 900 ether);
      assertGt(liquidatorBalanceAfter, liquidatorBalanceBefore);
      console.log("Liquidator balance before:", liquidatorBalanceBefore);
      console.log("Liquidator balance after:", liquidatorBalanceAfter);
      console.log(
          "Collateral received by liquidator:",
          liquidatorBalanceAfter - liquidatorBalanceBefore
      );
 
      console.log("Step 9: User repays remaining debt");
      uint256 remainingDebt = lending.borrows(user);
      vm.startPrank(user);
      token.approve(address(lending), remainingDebt);
      lending.repay(remainingDebt);
      vm.stopPrank();
 
      assertEq(lending.borrows(user), 0);
 
      console.log("Step 10: User withdraws remaining collateral");
      uint256 remainingDeposit = lending.deposits(user);
      vm.prank(user);
      lending.withdraw(remainingDeposit);
 
      assertEq(lending.deposits(user), 0);
 
      assertEq(lending.totalBorrows(), 0);
      assertEq(lending.totalDeposits(), 0);
      assertLt(token.balanceOf(user), INITIAL_BALANCE);
      assertGt(token.balanceOf(liquidator), INITIAL_BALANCE);
  }
```

--------------------------------

### Implement Governance Integration Test

Source: https://www.soliditytestingbook.com/basic/integration-tests

A test case verifying that the Governance contract correctly updates the reward rate in the Vault contract.

```solidity
contract GovernanceIntegrationTest is Test {
    Vault vault;
    Governance governance;
 
    function setUp() public {
        governance = new Governance();
        vault = new Vault(address(governance));
    }
 
    function testGovernanceUpdatesRewardRate() public {
        uint256 newRewardRate = 100;
        governance.setRewardRate(address(vault), newRewardRate);
 
        assertEq(vault.rewardRate(), newRewardRate, "Vault's rewardRate should be updated to 100");
    }
}
```

--------------------------------

### Vesting Unit Test Suite

Source: https://www.soliditytestingbook.com/advanced/mutation-tests

Initial unit tests for the vesting contract functionality.

```solidity
// Vesting.t.sol
contract Vesting_UnitTest is Test {
    Vesting public vesting;
    MockERC20 public token;
    address public owner;
    address public beneficiary;
    uint256 public vestingDuration;
    uint256 public totalAmount;
 
    function setUp() public {
        owner = address(this);
        beneficiary = address(0x1);
        vestingDuration = 365 days;
        totalAmount = 1000 ether;
 
        vesting = new Vesting();
        token = new MockERC20("MockToken", "MTN");
        token.mint(owner, totalAmount);
    }
 
    function testStartVesting() public {
        vesting.initialize(beneficiary, vestingDuration);
        token.approve(address(vesting), totalAmount);
        vesting.fund(IERC20(address(token)), totalAmount);
        vesting.startVesting();
 
        assertEq(uint256(vesting.state()), uint256(Vesting.VestingState.Vesting));
        assertEq(vesting.vestingStart(), block.timestamp);
    }
}
```