arXiv subjects

Enrico Lipparini

Publications and source records attributed to Enrico Lipparini.

At least 19 recordsLinked to original sources

arXiv2026

MCSAT Modulo Transcendental Arithmetics

We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally build a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our prototype outperforms state-of-the-art solvers on both SAT and UNSAT instances.

cs.LO↗

arXiv2026

Neuroforger: certified violation witnesses for smart contracts verification via LLMs

Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property, suggesting a complementary approach to traditional formal-methods-based techniques for smart contract verification. However, the application of LLMs in such context has two major issues: 1) properties expressed in natural language are intrinsically ambiguous, and 2) answers returned by LLMs have no guarantee of correctness. In this paper, we address both issues simultaneously by: 1) introducing a new formal specification language that extends Solidity with abstract types, and 2) designing a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses (i.e., counterexamples). The key idea is to represent a specification as a Solidity test with (existentially quantified) variables of abstract type; finding an instantiation of these variables to concrete values (of the correct type) concretizes the test into an executable counterexample (PoC) for the target property. We implemented our procedure in the tool Neuroforger, experimentally evaluating it on a smart-contract verification dataset drawn from literature, obtaining promising results that demonstrate its potential applicability in the wild.

cs.PL↗

arXiv2026

KindHML: formal verification of smart contracts based on Hennessy-Milner logic

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 often exploit flaws in the business logic of contracts that unfold across multiple transactions, such as liquidity or front-running attacks. Detecting these attacks requires reasoning about expressive temporal properties beyond the capabilities of existing analysis tools. In this paper, we present an automated approach to the formal verification of smart contracts, enabling the specification and verification of complex temporal properties. Our approach provides a fully automated encoding into Lustre -- the specification language supported by the Kind 2 model checker -- of an expressive subset of Solidity contracts and temporal specifications based on first-order Hennessy-Milner Logic. This encoding allows us to leverage Kind 2 to determine whether the contract respects the specification or not. We implement our approach in a toolchain that integrates the translation and verification steps, and we evaluate its effectiveness and performance on a benchmark of smart contracts and temporal properties capturing complex attack scenarios. Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts and detect violations that are beyond the reach of existing analysis tools.

cs.CR↗

arXiv2025

LLMs as verification oracles for Solidity

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 patterns can serve as a first line of defense, most real-world exploits and losses stem from errors in the contract business logic. Formal verification tools such as SolCMC and the Certora Prover address this challenge, but their impact remains limited by steep learning curves and restricted specification languages. Recent works have begun to explore the use of large language models (LLMs) for security-related tasks such as vulnerability detection and test generation. Yet, a fundamental question remains open: can LLMs aid in assessing the validity of arbitrary contract-specific properties? In this paper, we provide the first systematic empirical evaluation of GPT-5, a state-of-the-art reasoning LLM, in this role. We benchmark its performance on a large dataset of verification tasks, compare its outputs against those of established formal verification tools, and assess its practical effectiveness in real-world auditing scenarios. Our study combines quantitative metrics with qualitative analysis, and shows that recent reasoning-oriented LLMs - although lacking soundness guarantees - can be surprisingly effective at predicting the (in)validity of complex properties, suggesting a new frontier in the convergence of AI and formal methods for secure smart contract development and auditing.

cs.CR↗

arXiv2025

A theory of Lending Protocols in DeFi

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 dollars. Unlike traditional lending systems, these protocols operate without relying on trusted authorities or off-chain enforcement mechanisms. To achieve key economic goals such as stability of the loan market, they devise instead trustless on-chain mechanisms, such as rewarding liquidators who repay the loans of under-collateralized borrowers by awarding them part of the borrower's collateral. The complexity of these incentive mechanisms, combined with their entanglement in low-level implementation details, makes it challenging to precisely assess the structural and economic properties of lending protocols, as well as to analyze user strategies and attacks. Crucially, since participation is open to anyone, any weaknesses in the incentive mechanism may give rise to unintended emergent behaviours, or even enable adversarial strategies aimed at making profits to the detriment of legit users, or at undermining the stability of the protocol. In this work, we propose a formal model of lending protocols that captures the essential features of mainstream platforms, enabling us to identify and prove key properties related to their economic and strategic dynamics.

cs.GT↗

arXiv2025

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search

The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by incrementally constructing a model by assigning concrete values to theory variables and performing theory-level reasoning to learn lemmas when conflicts arise. Therefore, the selection of values can significantly impact the search process and the solver's performance. In this work, we propose guiding the MCSat search by utilizing assignment values discovered through local search. First, we present a theory-agnostic framework to seamlessly integrate local search techniques within the MCSat framework. Then, we highlight how to use the framework to design a search procedure for (quantifier-free) Nonlinear Integer Arithmetic (NIA), utilizing accelerated hill-climbing and a new operation called feasible-sets jumping. We implement the proposed approach in the MCSat engine of the Yices2 solver, and empirically evaluate its performance over the N IA benchmarks of SMT-LIB.

cs.LO↗

arXiv2025

Formal verification in Solidity and Move: insights from a comparative analysis

Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is correctly implemented. For Solidity, even though there already exist several mature verification tools, the semantical quirks of the language can make verification quite hard in practice. Move, on the other hand, has been designed with security and verification in mind, and it has been accompanied since its early stages by a formal verification tool, the Move Prover. In this paper, we investigate through a comparative analysis: 1) how the different designs of the two contract languages impact verification, and 2) what is the state-of-the-art of verification tools for the two languages, and how do they compare on three paradigmatic use cases. Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.

cs.CR↗

arXiv2024

Solvent: liquidity verification of smart contracts

Smart contracts are an attractive target for attackers, as evidenced by a long history of security incidents. A current limitation of smart contract verification tools is that they are not really effective in expressing and verifying liquidity properties regarding the exchange of crypto-assets: for example, is it true that in every reachable state a user can fire a sequence of transactions to withdraw a given amount of crypto-assets? We propose Solvent, a tool aimed at verifying these kinds of properties, which are beyond the reach of existing verification tools for Solidity. We evaluate the effectiveness and performance of Solvent through a common benchmark of smart contracts.

cs.CR↗

arXiv2023

Satisfiability of Non-Linear Transcendental Arithmetic as a Certificate Search Problem

For typical first-order logical theories, satisfying assignments have a straightforward finite representation that can directly serve as a certificate that a given assignment satisfies the given formula. For non-linear real arithmetic augmented with trigonometric and exponential functions (NTA), however, there is no known direct representation of satisfying assignments that allows for a simple independent check of whether the represented numbers exist and satisfy the given formula. Hence, in this paper, we introduce a different form of satisfiability certificate for NTA, and formulate the satisfiability problem as the problem of searching for such a certificate. This does not only ease the independent verification of satisfiability, but also allows the design of new algorithms that show satisfiability by systematically searching for such certificates. Computational experiments document that the resulting algorithms are able to prove satisfiability of a substantially higher number of benchmark problems than existing methods. We also characterize the formulas whose satisfiability can be demonstrated by such a certificate, by providing lower and upper bounds in terms of relevant well-known classes. Finally we show the existence of a procedure for checking the satisfiability of NTA-formulas that terminates for formulas that satisfy certain robustness assumptions.

cs.LO↗

arXiv2013

A Time Dependent Local Isospin Density Approximation Study of Asymmetric Nuclear Matter

The dynamic response of asymmetric nuclear matter is studied by using a Time-Dependent Local Isospin Density (TDLIDA) approximation approach. Calculations are based on a local density energy functional derived by an Auxiliary Field Diffusion Monte Carlo (AFDMC) calculation of bulk nuclear matter. Three types of excited states emerge: collective states, a continuum of quasi-particle-quasi-hole excitations and unstable solutions. These states are analyzed and discussed for different values of the nuclear density $ρ$ and isospin asymmetry $ξ=(N-Z)/A$. An analytical expression of the compressibility as a function of $ρ$ and $ξ$ is derived which show explicitly an instability of the neutron matter around $ρ\simeq 0.09 fm^{-3}$ when a small fraction of protons is added to the system.

nucl-th↗

arXiv2006

Optical response of two-dimensional few-electron concentric double quantum rings: A local-spin-density-functional theory study

We have investigated the dipole charge- and spin-density response of few-electron two-dimensional concentric nanorings as a function of the intensity of a perpendicularly applied magnetic field. We show that the dipole response displays signatures associated with the localization of electron states in the inner and outer ring favored by the perpendicularly applied magnetic field. Electron localization produces a more fragmented spectrum due to the appearance of additional edge excitations in the inner and outer ring.

cond-mat.mes-hall↗

arXiv2006

Spin-orbit effects in GaAs quantum wells: Interplay between Rashba, Dresselhaus, and Zeeman interactions

The interplay between Rashba, Dresselhaus and Zeeman interactions in a quantum well submitted to an external magnetic field is studied by means of an accurate analytical solution of the Hamiltonian, including electron-electron interactions in a sum rule approach. This solution allows to discuss the influence of the spin-orbit coupling on some relevant quantities that have been measured in inelastic light scattering and electron-spin resonance experiments on quantum wells. In particular, we have evaluated the spin-orbit contribution to the spin splitting of the Landau levels and to the splitting of charge- and spin-density excitations. We also discuss how the spin-orbit effects change if the applied magnetic field is tilted with respect to the direction perpendicular to the quantum well.

cond-mat.mes-hall↗

arXiv2006

Vertically coupled double quantum rings at zero magnetic field

Within local-spin-density functional theory, we have investigated the `dissociation' of few-electron circular vertical semiconductor double quantum ring artificial molecules at zero magnetic field as a function of inter-ring distance. In a first step, the molecules are constituted by two identical quantum rings. When the rings are quantum mechanically strongly coupled, the electronic states are substantially delocalized, and the addition energy spectra of the artificial molecule resemble those of a single quantum ring in the few-electron limit. When the rings are quantum mechanically weakly coupled, the electronic states in the molecule are substantially localized in one ring or the other, although the rings can be electrostatically coupled. The effect of a slight mismatch introduced in the molecules from nominally identical quantum wells, or from changes in the inner radius of the constituent rings, induces localization by offsetting the energy levels in the quantum rings. This plays a crucial role in the appearance of the addition spectra as a function of coupling strength particularly in the weak coupling limit.

cond-mat.mes-hall↗

arXiv2006

Spin-orbit effects on the Larmor dispersion relation in GaAs quantum wells

We have studied the relevance of spin-orbit coupling to the dispersion 00009 relation of the Larmor resonance observed in inelastic light scattering and electron-spin resonance experiments on GaAs quantum wells. We show that the spin-orbit interaction, here described by a sum of Dresselhaus and Bychkov-Rashba terms, couples Zeeman and spin-density excitations. We have evaluated its contribution to the spin splitting as a function of the magnetic field $B$, and have found that in the small $B$ limit, the spin-orbit interaction does not contribute to the spin splitting, whereas at high magnetic fields it yields a $B$ independent contribution to the spin splitting given by $2(λ_R^2-λ_D^2)$, with $λ_{R,D}$ being the intensity of the Bychkov-Rashba and Dresselhaus spin-orbit terms.

cond-mat.mes-hall↗

arXiv2005

Ground state structure and conductivity of quantum wires of infinite length and finite width

We have studied the ground state structure of quantum strips within the local spin-density approximation, for a range of electronic densities between $\sim$ 5$\times10^4$ and 2$\times10^6$ cm$^{-1}$ and several strengths of the lateral confining potential. The results have been used to address the conductance $G$ of quantum strips. At low density, when only one subband is occupied, the system is fully polarized and $G$ takes a value which is close to 0.7(2e$^2/h$), decreasing with increasing electron density in agreement with experiments. At higher densities the system becomes paramagnetic and $G$ takes a value near (2e$^2/h$), showing a similar decreasing behaviour with increasing electron density. In both cases, the physical parameter that determines the value of the conductance is the ratio $K/K_0$ of the compressibility of the system over the free one.

cond-mat.mes-hall↗

arXiv2003

Magneto-Optics in parabolic three-dimensional quantum dots in magnetic fields of arbitrary direction

We generalize the Kohn's theorem to the case of parabolic three-dimensional quantum dots in magnetic fields of arbitrary direction. We show numerically that the exact resonance frequencies in the magneto-optical absorption of these dots are reproduced by the adiabatic time-dependent local spin density approximation theory (TDLSDA). We use TDLSDA to predict spin density excitations in the dots.

cond-mat↗

arXiv2002

Electronic spin precession in semiconductor quantum dots with spin-orbit coupling

The electronic spin precession in semiconductor dots is strongly affected by the spin-orbit coupling. We present a theory of the electronic spin resonance at low magnetic fields that predicts a strong dependence on the dot occupation, the magnetic field and the spin-orbit coupling strength. Coulomb interaction effects are also taken into account in a numerical approach.

cond-mat.mes-hall↗

arXiv2002

Spin switching in semiconductor quantum dots through spin-orbit coupling

The spin-orbit coupling influences the total spin of semiconductor quantum dots. We analyze the theoretical prediction for the combined effects of spin-orbit coupling, weak vertical magnetic fields and deformation of the dot. Our results allow the characterization of the quantum dots as spin switches, controllable with electric gates.

cond-mat.mes-hall↗