This document describes the specification and verification of Rocket Joe system using the Certora Prover. We undertook the work from January 13, 2022 to March 4, 2022. The latest commit that was reviewed and ran through the Certora Prover was ef2ef302.

The scope of this verification is Rocket Joe system, particularly the following contracts:

LaunchEvent.sol

RocketJoeFactory.sol

RocketJoeStaking.sol

RocketJoeToken.sol

The Certora Prover proved the implementation of the distribution system is correct with respect to formal specifications written by the Certora team. The team also performed a manual audit of these contracts. The formal specifications focus on validating the system's correct behavior as described by the Trader Joe team. The rules verify valid states of a system, proper transitions between states and the solvency of the system. The formal specifications have been submitted as a pull request against TraderJoe's public git repository.