Kavli Affiliate: James Chiang
| First 5 Authors: Massimo Bartoletti, James Chiang, Tommi Junttila, Alberto Lluch Lafuente, Massimiliano Mirelli
| Summary:
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.
| Search Query: ArXiv Query: search_query=au:”James Chiang”&id_list=&start=0&max_results=3