7 papers
A formal framework for the economic security of DeFi compositions
Massimo Bartoletti, Riccado Marchesin, Roberto Zunino
Decentralized Finance (DeFi) services are usually constructed by composing a variety of smart contracts. While composability is a key driver of the success of DeFi, it also creates…
Neuroforger: certified violation witnesses for smart contracts verification via LLMs
Massimo Bartoletti, Enrico Lipparini
Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property, suggestin…
KindHML: formal verification of smart contracts based on Hennessy-Milner logic
Massimo Bartoletti, Angelo Ferrando, Enrico Lipparini +1
Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks of…
A Formal Approach to AMM Fee Mechanisms with Lean 4
Marco Dessalvi, Massimo Bartoletti, Alberto Lluch-Lafuente
Decentralized Finance (DeFi) has revolutionized financial markets by enabling complex asset-exchange protocols without trusted intermediaries. Automated Market Makers (AMMs) are a…
LLMs as verification oracles for Solidity
Massimo Bartoletti, Enrico Lipparini, Livio Pompianu
Ensuring the correctness of smart contracts is critical, as even subtle flaws can lead to severe financial losses. While bug detection tools able to spot common vulnerability patte…
A theory of Lending Protocols in DeFi
Massimo Bartoletti, Enrico Lipparini
Lending protocols are one of the main applications of Decentralized Finance (DeFi), enabling crypto-assets loan markets with a total value estimated in the tens of billions of doll…