This document describes the specification and verification of Protofire's ve8020-Launchpad using the Certora Prover and manual code review findings. The work was undertaken from 27th November 2023 to 15th December 2023. The latest commit that was reviewed is [d1e79a2].

The following contracts list is included in the scope:

• RewardDistributor.sol
• RewardFaucet.sol
• VotingEscrow.vy
• Launchpad.vy

The contracts were verified against the Solidity versions:

• RewardDistributor.sol : solc 7.6
• RewardFaucet: solc 8.18
• OpenZeppelin ERC20 instances: solc 8.18

The Certora Prover demonstrated that 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 Solidity contracts. During the verification process and the manual audit, the Certora Prover discovered bugs in the Solidity contracts code, as listed below.