This report describes the specification and verification of the Integrated Liquidity Market (ILM) using the Certora Prover and manual code review findings. The main work was undertaken from January 28th 2024 to February 29th 2024, with an additional 3 days (March 25-28) for fix review.

In the table above, the original code submitted for review is commit hash 697b389. The first round of code fixes is commit hash f480d90 from February 21. The second and final round of fixes reviewed in this engagement is commit hash f480d90 from March 20. The file structure remained the same throughout the three versions of the code base. The following Solidity files are included in our scope:

src/LoopStrategy.sol
src/swap/adapter/WrappedTokenAdapter.sol
src/swap/adapter/AerodromeAdapter.sol
src/swap/adapter/SwapAdapterBase.sol
src/swap/Swapper.sol
src/libraries/LoanLogic.sol
src/libraries/math/RebalanceMath.sol
src/libraries/math/ConversionMath.sol

src/libraries/math/USDWadRayMath.sol
src/libraries/RebalanceLogic.sol
src/storage/AerodromeAdapterStorage.sol
src/storage/LoopStrategyStorage.sol
src/storage/SwapAdapterBaseStorage.sol
src/storage/SwapperStorage.sol
src/storage/WrappedTokenAdapterStorage.sol
src/tokens/WrappedCbETH.sol
src/types/DataTypes.sol

The Certora Prover demonstrated the implementation of the Solidity contracts above is correct with respect to the formal rules written by the Certora team. In addition, the team performed a manual audit of all the Solidity contracts . During the verification process and the manual audit, the Certora Prover discovered bugs in the Solidity contracts code, as listed in the report below.