Formal Analysis of Lending Pools in Decentralized Finance

Massimo Bartoletti, James Chiang, Tommi Junttila, Alberto Lluch Lafuente*, Massimiliano Mirelli, Andrea Vandin

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

26 Downloads (Pure)


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.

Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning.
EditorsTiziana Margaria, Bernhard Steffen
Publication date2022
ISBN (Print)9783031197581
Publication statusPublished - 2022
Event11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Alila Resort & Spa, Rhodes, Greece
Duration: 22 Oct 202230 Oct 2022
Conference number: 11


Conference11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
LocationAlila Resort & Spa
Internet address
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13703 LNCS


Dive into the research topics of 'Formal Analysis of Lending Pools in Decentralized Finance'. Together they form a unique fingerprint.

Cite this