2 papers
cs.PL2026
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…
cs.CR2026
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…