Reserve Protocol enables a class of token called RToken: self-issued tokens backed by a rebalancing set of collateral. This engagement focused on the Fixed.sol library for fixed-point arithmetic that provides safe conversions and common operations.

During the verification process, the Certora team discovered issues in the Solidity library code which are detailed in the full report along with subsequent fixes. The Certora Prover demonstrated that the implementation of the Fixed.sol library was correct with respect to formal rules written by the Certora team.