This document describes the specification and verification of Compound's Comet protocol using the Certora Prover. The work was undertaken from Feb 1st to March 24th, 2022, while the code was still in development. The latest commit reviewed and run through the Certora Prover was 4d1c1a42fc31b4b26129fe79e3d97ef637da9520.

The scope of this verification is Compound's Comet protocol which includes the following contracts:

Comet.sol

CometExt.sol

And their parent contracts:

CometConfiguration.sol

CometCore.sol

CometFactory.sol

CometMath.sol

CometStorage.sol

The Certora Prover proved that the implementation of Compound's Comet is correct with respect to formal specifications written by the Compound and Certora teams. Certora also performed a manual audit of these contracts. During this verification process, the Certora Prover discovered bugs in the code which are listed in the tables below. All issues were promptly corrected by Compound, and the fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The Certora development team is currently handling these limitations. All the rules and specification files are publicly available and can be found in Compound's Comet repository.