Massimo Bartoletti
3 indexed papers
Publications per year
Top categories
Frequent co-authors
Research Timeline
The paper introduces KindHML, an automated formal verification approach that uses Hennessy-Milner Logic and the Kind 2 model checker to verify complex temporal properties of smart contracts, detecting vulnerabilities beyond current tools.
The paper introduces Neuroforger, a system that combines a new formal specification language with LLMs and type checking to reliably generate and validate concrete violation witnesses (counterexamples) for smart contract verification.
The paper introduces MEV non-interference, a formal security notion, to ensure that composing new smart contracts in DeFi does not increase the maximal extractable value, thereby providing a formal foundation for economic security.
Papers
A formal framework for the economic security of DeFi compositions
The paper introduces MEV non-interference, a formal security notion, to ensure that composing new smart contracts in DeFi does not increase the maximal extractable value, thereby providing a formal fo…