The past decade has witnessed the burgeoning and continuous development of blockchain and its applications. Besides various cryptocurrencies, an industry that has quickly embraced this trend is gaming. Thanks to the support of blockchain, games have started to incorporate non-fungible tokens (NFTs) that can enable a new gaming model, play-to-earn (P2E), which incentivizes users to participate and play. While recent studies looked at several NFT games qualitatively and individually, an in-depth understanding is still missing, particularly on how the P2E model has transformed traditional games. In this work, we set to conduct a measurement study of NFT games, aiming to gain a comprehensive understanding of the effectiveness of P2E in practice. For this purpose, we collect and analyze relevant NFT transaction data from the underlying blockchain (e.g., Ethereum) of 12 games, supplemented with various data scraped from their websites. Our study shows that (1) a few top wallets control unproportionally high percentage of NFTs, and the majority of wallets own only one or two NFTs and do not actively trade; (2) promotion events do boost the trade amount and the NFT price for some games, but their effect does not sustain; and (3) few players actually earned a profit, and players in 9 out of 12 games who traded NFTs have a negative profit on average. Motivated by these findings, we further investigate effective incentive mechanisms based on game theory to improve the trading profits that players can earn from these NFT games. Both modeling and simulation results confirm the effectiveness of the proposed incentive mechanism.
Liquidation of collateral are the primary safeguard for solvency of lending protocols in decentralized finance. However, the mechanics of liquidations expose these protocols to predatory price manipulations and other forms of Maximal Extractable Value (MEV). In this paper, we characterize the optimal liquidation strategy, via a dynamic program, from the perspective of a profit-maximizing liquidator when the spot oracle is given by a Constant Product Market Maker (CPMM). We explicitly model Oracle Extractable Value (OEV) where liquidators manipulate the CPMM with sandwich attacks to trigger profitable liquidation events. We derive closed-form liquidation bounds and prove that CPMM transaction fees act as a critical security parameter. Crucially, we demonstrate that fees do not merely reduce attacker profits, but can make such manipulations unprofitable for an attacker. Our findings suggest that CPMM transaction fees serve a dual purpose: compensating liquidity providers and endogenously hardening CPMM oracles against manipulation without the latency of time-weighted averages or medianization.
We present SPEAR, a multi-agent coordination framework for smart contract auditing that applies established MAS patterns in a realistic security analysis workflow. SPEAR models auditing as a coordinated mission carried out by specialized agents: a Planning Agent prioritizes contracts using risk-aware heuristics, an Execution Agent allocates tasks via the Contract Net protocol, and a Repair Agent autonomously recovers from brittle generated artifacts using a programmatic-first repair policy. Agents maintain local beliefs updated through AGM-compliant revision, coordinate via negotiation and auction protocols, and revise plans as new information becomes available. An empirical study compares the multi-agent design with centralized and pipeline-based alternatives under controlled failure scenarios, focusing on coordination, recovery behavior, and resource use.
Essais sur le crédit, la découverte des taux et les facteurs déterminants du prix des jetons en finance décentralisée Cette thèse explore les fondements économiques et comportementaux de la finance décentralisée (DeFi), un champ en pleine expansion où les fonctions de prêt, d'emprunt et de fixation des taux d'intérêt sont assurées par des contrats intelligents plutôt que par des institutions financières. À travers trois essais complémentaires, ce travail analyse la conception des protocoles de crédit décentralisés, la formation des taux d'intérêt dans des marchés automatisés et les déterminants fondamentaux et comportementaux de la valorisation des tokens DeFi.Le premier essai examine l'architecture du protocole Atlendis, qui permet des prêts non ou partiellement collatéralisés grâce à l'articulation entre souscription off-chain et exécution on-chain. Le deuxième propose un modèle théorique de découverte de taux basé sur une approche de jeu multi-unités, identifiant les conditions d'efficience et les frictions propres aux marchés décentralisés. Le troisième évalue empiriquement les facteurs économiques et comportementaux influençant les rendements des tokens, révélant le rôle central du sentiment des investisseurs et de la liquidité on-chain dans la dynamique des prix. En combinant ingénierie financière, modélisation théorique et analyse empirique, cette recherche met en lumière les mécanismes par lesquels la DeFi redéfinit l'intermédiation, la formation des prix et la gouvernance financière dans un environnement transparent et programmable.
In blockchain systems operating under the Proof-of-Stake (PoS) consensus mechanism, fairness in transaction processing is essential to preserving decentralization and maintaining user trust. However, with the emergence of Maximal Extractable Value (MEV), concerns about economic centralization and content manipulation have intensified. To address these vulnerabilities, the Ethereum community has introduced Proposer Builder Separation (PBS), which separates block construction from block proposal. Later, enshrined Proposer Builder Separation (ePBS) was also proposed in EIP-7732, which embeds PBS directly into the Ethereum consensus layer. Our work identifies key limitations of ePBS by developing a formal framework that combines mathematical analysis and agent-based simulations to evaluate its auction-based block-building mechanism, with particular emphasis on MEV dynamics. Our results reveal that, although ePBS redistributes responsibilities between builders and proposers, it significantly amplifies profit and content centralization: the Gini coefficient for profits rises from 0.1749 under standard PoS without ePBS to 0.8358 under ePBS. This sharp increase indicates that a small number of efficient builders capture most value via MEV-driven auctions. Moreover, 95.4% of the block value is rewarded to proposers in ePBS, revealing a strong economic bias despite their limited role in block assembly. These findings highlight that ePBS exacerbates incentives for builders to adopt aggressive MEV strategies, suggesting the need for future research into mechanism designs that better balance decentralization, fairness, and MEV mitigation.
We prove that first homology of the control flow graph provides a complete characterization of reentrancy vulnerability in smart contracts. Specifically, we establish the Homological Reentrancy Theorem: a contract admits a reentrant execution path if and only if H₁(G) ≠ 0, where G is the extended control flow graph incorporating external call returns. We prove soundness (no false negatives) and completeness (no false positives) for contracts satisfying a non-degeneracy condition. For multi-contract systems, we apply the Mayer-Vietoris exact sequence to compute H₁ of the composed system from individual components, enabling detection of cross-contract reentrancy. We validate empirically against 17 known exploits including The DAO (2016), Parity Wallet (2017), and Cream Finance (2021), achieving 100% detection with zero false positives.
Gauhar Ali, Sajid Hussain Shah, Muhammad Asim, Abdelhamied A. Ateya · 5 authors
The global energy sector is experiencing a significant revolution, propelled by the necessity to address climate change and shift towards sustainable energy sources. Particularly, the extensive implementation of distributed solar photovoltaic generation is converting traditional power grid systems into decentralized, prosumer-oriented energy grids. However, the traditional centralized energy trading frameworks cannot handle the complexity and volatility of a distributed grid, resulting in delay, costly transactions, a single point of failure, and insufficient transparency. Although blockchain (BC)-based peer-to-peer (P2P) energy trading presents an attractive solution, current models frequently neglect to ensure dependable and steady market convergence, instead concentrating mainly on transactional elements. This study proposed an innovative smart contract-based P2P renewable energy trading framework intended for decentralized grids. The proposed two-tiered framework, i.e., intra-microgrid and inter-microgrid layers, expands P2P trading from regional equilibrium to full grid connectivity. It utilizes a game-theoretic, iterative bidding approach, entirely automated by smart contracts. This method is formally proven to attain market convergence to a singular Nash equilibrium, optimizing utility for prosumers and consumers in the energy trading. Moreover, the decentralized ledger, smart contract-based market clearance, and limited disclosure of consumer/prosumer’s private data enhanced its resilience against replay, false data injection, and DoS/DDoS attacks. Additionally, the proposed energy trading market is proved monotonic and convergent formally by implementing a Promela model using the SPIN model checker.
Mohsen Minaei, Ranjit Kumaresan, Andrew Beams, Pedro Moreno-Sánchez · 9 authors
Blockchain auction plays an important role in the price discovery of digital assets (e.g.NFTs).However, despite their importance, implementing auctions directly on blockchains such as Ethereum incurs scalability issues.In particular, the on-chain transactions scale poorly with the number of bidders, leading to network congestion, increased transaction fees, and slower transaction confirmation time.This lack of scalability significantly hampers the ability of the system to handle largescale, high-speed auctions that are common in today's economy.In this work, we build a protocol where an auctioneer can conduct sealed bid auctions that run entirely off-chain when parties behave honestly, and in the event that k bidders deviate (e.g., do not open their sealed bid) from an n-party auction protocol, then the on-chain complexity is only O(k).This improves over existing solutions that require O(n) on-chain complexity, even if a single bidder deviates from the protocol.In the event of a malicious auctioneer, our protocol still guarantees that the auction will successfully terminate.We implement our protocol and show that it offers significant efficiency improvements compared to existing on-chain solutions.Our use of zkSnark to achieve scalability also ensures that the on-chain contract and other participants do not learn anything about the bidders' identities and their respective bids, except for the winner and the winning bid amount.
Protocol-level validity mechanisms, such as validity rollups and STARK-based proving systems, improve blockchain scalability, but do not remove the cost of executing computation-intensive application logic inside smart contracts. At the application layer, a meaningful class of structured arithmetic workloads—including polynomial evaluations, cryptographic primitive computations, and signal-processing operations over finite fields—arises naturally in contract logic, yet remains subject to the on-chain fee model regardless of protocol-level optimizations. This paper investigates whether outsourcing such workloads and replacing direct execution with transparent on-chain verification can provide a practical cost advantage under realistic smart-contract fee models. We present a cross-platform implementation of GKR-based transparent on-chain verification for outsourced structured arithmetic circuits on the Ethereum Virtual Machine (Solidity) and Starknet (Cairo). GKR requires no trusted setup, which makes it particularly suitable for deployment in permissionless public blockchain environments where trust assumptions must be minimized. The design targets layered circuits with regular structure and incorporates implementation techniques that reduce verifier-side overhead and eliminate the linear input-handling bottleneck in naive deployments. These workloads can be represented as layered arithmetic circuits with regular wiring and logarithmic depth. Our evaluation shows that direct execution cost increases rapidly with input size, whereas GKR-based verification scales much more favorably. At size 4096, verification reduces execution cost by approximately 84% on the EVM and 91% on Starknet. These results identify outsourced execution with on-chain GKR verification as a practical design point for application-layer verifiable computation, especially in public blockchain environments where transparency and the absence of trusted setup are important.
Formal verification is essential for ensuring the safety of smart contracts in decentralized finance (DeFi), but scaling these techniques across diverse blockchain ecosystems remains a challenge. In this talk, we present our experience making formal verification practical across multiple platforms, including the EVM, Solana, Stellar, and Sui. We discuss how automated reasoning techniques can be adapted to different execution models and programming paradigms while still providing strong correctness guarantees. We focus on what it takes to apply verification in real-world settings: handling complex DeFi primitives, integrating with development workflows, and maintaining usability for engineers. Drawing from verification projects with production protocols, we highlight key challenges and lessons learned in bringing formal methods from theory into practice.
Damaris Jepkurui Kangogo, Bertalan Zoltán Péter, Attila Klenik, Imre Kocsis
<title>Abstract</title> Smart contracts in blockchains often implement critical functionality; consequently, their development time software fault detection, removal, and avoidance have been the target of intensive research. However, the applicability of runtime dependability mechanisms to smart contracts has not been explored systematically, mainly due to the transaction pricing models of public blockchains. In this paper, we propose a novel and practical runtime verification approach for Hyperledger Fabric, the leading cross-organizational blockchain platform, as an error detection facility for fault tolerance mechanisms; building on the proposition that, in contrast to the public setting, cross-organizational blockchains have ample computational headroom for their systematic use. We introduce a smart contract entity framework architecture with reusable domain models and encapsulated runtime verification. We describe Hypernate, our open-source implementation of the approach for Java smart contracts, which uses the Java Modelling Language for requirement specification and integrates the OpenJML verification tool. We demonstrate and evaluate the approach on a Fabric implementation of the TPC-C benchmark.
Sara Migliorini, Mauro Gambini, Veronica Paternolli, Mila Dalla Preda
In the socio-economic landscape, we can recognize an emerging form of organization: the network coalition. A network coalition is a form of concerted cooperation in which a group of agents decides to collaborate to achieve a common goal. The decentralized and cooperative nature of a network coalition presents new challenges in automating its processes, which cannot be treated as traditional business processes managed by a centralized information system. In the literature, the notion of Exogenous Business Process (XBP) has been introduced to capture such processes. An XBP specification is intended as a potentially incomplete, renegotiable, procedural contract to which different parties adhere in order to achieve a predefined business goal. The concept of Enforceable Business Process (EBP) has been proposed as a possible abstraction for modeling and automating the XBPs of a network coalition. An EBP is essentially an evolution of the original concept of smart contract, which is able to properly manage contractual incompleteness while providing automatic enforceability. The aim of this paper is to formalize the notion of EBP and discuss how contractual incompleteness can be handled by a Decentralized Autonomous Information System (DAIS). The complete formalization of both procedural and incompleteness aspects of EBPs, as provided by this paper, lays the basis for the construction of the next generation of DAIS, as well as the diffusion of network coalition into many application domains, such as supply chains, business alliances, joint ventures, and others.
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 central component of DeFi, providing the core functionality of swapping assets of different types at algorithmically computed exchange rates. Several mainstream AMM implementations are based on the constant-product model, which ensures that swaps preserve the product of the token reserves in the AMM - up to a trading fee used to incentivize liquidity provision. Trading fees substantially complicate the economic properties of AMMs, and for this reason some AMM models abstract them away in order to simplify the analysis. However, trading fees have a non-trivial impact on users' trading strategies, making it crucial to develop refined AMM models that precisely account for their effects. In this work, we extend a foundational model of AMMs by introducing a new parameter, the trading fee ϕ ∈ (0,1], into the swap rate function. Fee amounts increase inversely proportional to ϕ. When ϕ = 1, no fee is applied and the original model is recovered. We analyze the resulting fee-adjusted model from an economic perspective. We show that several key properties of the swap rate function, including output-boundedness and monotonicity, are preserved. At the same time, other properties - most notably additivity - no longer hold. We precisely characterize this deviation by deriving a generalized form of additivity that captures the effect of swaps in the presence of trading fees. In particular, we prove that when ϕ < 1, executing a single large swap yields strictly greater profit than splitting the trade into smaller ones. Finally, we derive a closed-form solution to the arbitrage problem in the presence of trading fees and prove its uniqueness. All results are formalized and machine-checked in the Lean 4 proof assistant.