Runtime Verification audits Gyroscope Protocol’s Mathematical Model Implementation

Runtime Verification is pleased to announce the audit completion of Gyroscope Protocol’s mathematical model implementation.

Gyroscope, built on Ethereum, is a fully-backed stablecoin with all-weather reserves and autonomous price bounding. The Gyroscope stablecoin aims at a long-term reserve ratio of 100%, where every unit of stablecoin is backed by 1 USD worth of collateral. This collateral is held in a reserve, a basket of protocol-controlled assets that jointly collateralize the issued stablecoin. The reserve aims to diversify all risks in DeFi to the greatest extent possible.

Runtime Verification conducted a code review of the Gyroscope contracts, with a primary focus on their mathematical model implementation. Over a period of 6 weeks, auditors conducted multiple reviews on the contract’s core functionalities. The audited functions include - 

• The PAMM mathematical model implementation - The Gyroscope primary algorithmic market maker (P-AMM) provides a redemption price curve for the Gyro token. 
• The CEMM mathematical model implementation - The constant-ellipse market maker (CEMM) is an automated market maker where the price curve is an ellipse
• The mathematical model implementation of LP Share Pricing- The LP share price of the underlying pools is used to compute the Gyroscope reserve value and the amount of proceeds for mint and redemption.

The audit covered only the Solidity source code contracts and excluded any deployment and upgrade scripts, off-chain codebase, and client-side portions of the codebase.

All analysis of the above protocol components was conducted assuming the correct and secure implementation of the other parts of the system and their integration with the core math implementation.

A central part of the audit has been to perform deep numerical error analysis on the implementation of the main algorithms of the protocol. This precision analysis aims to quantify the numerical differences (so-called errors) between the theoretical results produced by the algorithms and the actual results produced by their implementation in the code. This analysis shed important insights regarding which part of the code could be most optimized, which led to significant improvements in the precision of the implemented algorithms.

The audit identified and highlighted some issues along with a number of informative findings. Users interested in a more detailed and technical explanation of the findings can go over the full report  in our GitHub repository.

About Gyroscope

Gyroscope's mission is to build robust public infrastructure for DeFi. The central piece is a fully-backed stablecoin with all-weather reserves and autonomous price bounding:

• A fully backed stablecoin: the Gyroscope stablecoin aims at a long-term reserve ratio of 100%, where every unit of stablecoin is backed by 1 USD worth of collateral. 
• An all-weather reserve: the reserve is a basket of protocol-controlled assets that jointly collateralize the issued stablecoin. Initially most assets will be other stablecoins. The reserve aims to diversify all risks in DeFi to the greatest extent possible. It considers more than just price risk, but also censorship, regulatory, counterparty, oracle and governance risks. 
• Autonomous price bounding: Prices for minting and redeeming stablecoins are set autonomously to balance the goal of maintaining a tight peg with the goal of long-term viability of the project in the face of short-term crises.

About Runtime Verification

Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.