Formal Analysis of Lending Pools in Decentralized Finance

TL;DR

This paper presents a formal analysis tool for DeFi Lending Pools, enabling safety verification and risk assessment through model checking and statistical analysis to identify parameters minimizing unrecoverable loans.

Contribution

The paper introduces a novel formal analysis tool for DeFi Lending Pools, integrating Maude and MultiVeStA for comprehensive safety and risk evaluation.

Findings

Identified parameter thresholds reducing unrecoverable loan risks

Demonstrated the tool's capability for reachability and LTL model checking

Provided insights into Lending Pool safety through statistical analysis

Abstract

Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi applications is essential to assess their safety. We have developed a tool for the formal analysis of one of the most widespread DeFi applications: Lending Pools (LP). This was achieved by leveraging an existing formal model for LPs, the Maude verification environment and the MultiVeStA statistical analyser. The tool supports several analyses including reachability analysis, LTL model checking and statistical model checking. In this paper we show how the tool can be used to analyse several parameters of LPs that are fundamental to assess and predict their behaviour. In particular, we use statistical analysis to search for threshold and reward parameters that minimize the risk of unrecoverable loans.