Agent systems, particularly multi-agent systems, are becoming increasingly important tools for modeling and decision-making in complex environments, including finance, optimization, and epidemics. These systems simulate interactions between autonomous agents, which are individual entities that make decisions based on predefined rules, enabling the study of decentralized phenomena such as market behavior, social interactions, and information diffusion. By incorporating advanced statistical techniques, agent systems offer a more dynamic and adaptable approach compared to traditional, centralized models, capturing emergent behaviors and optimizing decisions in uncertain environments. This paper explores the role of agent systems in addressing challenges in complex domains, with a focus on their application in finance, optimization, epidemic modeling, and combating disinformation. The integration of agent-based models with principles of statistics and information theory is examined as a key factor driving the effectiveness of these systems in real-world applications. Through this examination, the paper highlights the growing significance of agent systems in tackling modern, decentralized problems that traditional methods have struggled to address.
Good news for researchers in formal verification: smart contracts regularly suffer exploits such as the DAO bug, which lost the equivalent of 60 million USD on Ethereum. This makes a strong case for applying formal methods to guarantee essential properties.<br/><br/>Which properties would we like to prove? Most previous studies focus on contract-specific properties that do not generalize to a wide class of smart contracts. There is currently no commonly agreed upon list of properties to use as a starting point in writing a formal specification.<br/><br/>We propose three properties that we believe are relevant to all smart contracts: Validity, Liquidity, and Fidelity. Focusing on the concrete case of the Cardano platform, we show how these properties stop exploits similar to the DAO bug, as well as preventing other common issues such as the locking of funds and double satisfaction.<br/><br/>We model an account simulation, a multi-signature wallet, and an order book decentralized exchange, as example smart contract specifications using state transition systems in the Agda proof assistant. We formalize the above properties and prove they hold for the models. The models are then separately proven to be functionally equivalent to a validator implementation in Agda, which is translated to Haskell using agda2hs. The Haskell code can then be compiled and put on the Cardano blockchain directly. We use the Cardano Node Emulator to run property-based tests and confirm that our validator works correctly.
This thesis analyzes liquidity provision strategies in decentralized finance (DeFi), focusing on Uniswap V3's automated market maker protocol. The research addresses the challenge of developing effective frameworks for liquidity providers operating in decentralized exchanges, where participants face unique risks including impermanent loss and strategic positioning decisions. Using empirical analysis of on-chain data, the study examines different liquidity provision approaches across various asset pairs and fee tiers to establish quantitative frameworks for strategic decision-making in DeFi markets.
Smart contract technology has witnessed rapid evolution and widespread adoption across diverse industries. However, with the immutable nature of blockchain-deployed contracts, vulnerabilities—especially those embedded in complex business logic—pose severe security risks. Traditional static analysis tools have struggled to accurately capture such vulnerabilities, prompting exploration into novel techniques that integrate large language models (LLMs), static analysis, and property-based testing. Firstly, we proposed a unified evaluation framework called LLM4Vuln, systematically decouples and assesses LLMs’ intrinsic vulnerability reasoning from external aids like knowledge enrichment and context retrieval. Evaluated on 294 code snippets spanning Solidity, Java, and C/C++ over 3,528 scenarios, LLM4Vuln not only elucidated the impacts of various enhancements but also uncovered 14 zero-day vulnerabilities in real-world projects, demonstrating both practical value and potential for significant security improvements. Secondly, building on these insights, we proposed GPTScan, the first tool to integrate GPT with static analysis for smart contract logic vulnerability detection. By decomposing each vulnerability into specific scenarios and properties, GPTScan employs GPT to identify critical code elements and then confirms these findings through static analysis. This hybrid approach achieves high precision on token contracts, maintains acceptable performance on large-scale projects, and delivers an overall recall above 70%, thereby effectively identifying vulnerabilities often overlooked by human auditors. Thirdly, to extend the scope of detectable vulnerabilities, we designed PropertyGPT, a framework leverages retrieval-augmented property generation. By harnessing LLMs’ in-context learning abilities, PropertyGPT generates compilable, context-appropriate, and verifiable properties for formal verification of smart contracts. Experimental results demonstrate an 80% recall relative to ground truth, with the framework successfully detecting multiple CVEs and uncovering several zero-day vulnerabilities, which have resulted in substantial bounty rewards. Fourthly, to address the detection of reentrancy vulnerabilities, we developed ReeSem. ReeSem combines static analysis with semantic understanding through LLMs. Its three-stage detection pipeline—filtering external calls, analyzing affected state variables, and semantically recognizing reentrancy guards—delivers an F1 score of 75.14%, outperforming state-of-the-art baselines significantly. ReeSem’s ability to generate consistent attack paths in real-world scenarios underscores its practical applicability and robustness. Fifthly, complementing the data-driven methods, ZepScope focuses on static analysis by mining constraints directly from official smart contract implementations, specifically, from those provided by OpenZeppelin. Through its MINER and CHECKER components, ZepScope extracts both explicit and implicit security checks and validates their enforcement in real-world contracts. This approach achieves an impressive accuracy of 89.67% across tens of thousands of contracts, offering critical insights into common code practices and potential security pitfalls. Collectively, these contributions, LLM4Vuln, GPTScan, PGPT, ReeSem, and ZepScope, form a comprehensive framework for enhancing vulnerability detection in smart contracts. By synergistically integrating large language models, static analysis, security constraints mining and property-based testing, this work advances the state-of-the-art in secure code auditing and provides valuable methodologies for developers, auditors, and the broader security community.
With complete-information bilateral bargaining in network settings, holdup is eliminated when contracts across the network are agreed atomically (all or none) via a smart contract. Applications include over-the-counter trading, syndicated lending, multi-tranche securitizations, third-party financed purchases, and bookbuilding. Under a novel extensive-form bargaining protocol, any firm can give a “greenlight” to the terms of a contract proposed to that firm, which automatically converts those terms into a binding contract if the terms proposed to all other firms also receive greenlights. In any Perfect Bayesian Equilibrium with Markov strategies, firms immediately agree on socially efficient contracts that equalize expected gains across firms.
Smart contracts frequently fail due to transaction reverts, yet diagnosing the causes of these failures remains challenging. We present an analysis pipeline that automatically extracts and clusters invariants from on-chain reverted transactions, uncovering the underlying conditions that trigger failures. At the core of our approach is ReBERT, a custom embedding model fine-tuned on invariant data, which outperforms existing semantic similarity models in capturing subtle predicate relationships. Our analysis reveals meaningful clusters of failure causes—such as Access Control, Data Flow, and Status Checks—that highlight recurring vulnerabilities in smart contract execution. These findings advance understanding of failure patterns for Ethereum Smart Contracts.
The consensus problem in distributed ledger systems has two distinct dimensions that existing protocols systematically conflate. The first is the Byzantine fault-tolerance question: can a network reach agreement in the presence of arbitrary failures? The second — less formalised but no less fundamental — is the anti-cartel question: can the incentive structure of the consensus mechanism structurally resist the formation of cartels that reconstitute centralised authority under a nominally decentralised banner? Bitcoin's proof-of-work has produced a system where a small number of industrial mining pools control the majority of hash power. BitCell is a proposal that takes the anti-cartel question seriously as an engineering problem rather than an economic folk theorem. BitCell replaces hash-grinding and stake-weighting with cellular automaton tournaments as the computational substrate for block proposal rights. In each round, miners commit to a pattern in a bounded Conway's Game of Life grid, are verifiably randomly paired via a VRF-based pairing mechanism, and compete in a deterministic single-elimination tournament whose outcome depends on strategic pattern design rather than raw computational expenditure or capital size. Victory rights are not transferable and are not enhanced by pooling strategies: a cartel of sub-majority miners cannot coordinate to construct a jointly optimal pattern that dominates unilateral honest play, because the tournament's pairwise structure, hidden identities (via ring signatures), non-shareable rewards, and reputation-gated eligibility remove each of the primary economic motivations that make mining pools attractive. Under a simple Bayesian model of miner incentives, collusive strategies for sub-majority cartels yield strictly lower expected payoffs than unilateral honest participation. Tournament eligibility and reward weighting are governed by an Evidence-Based Subjective Logic (EBSL) reputation layer. All state transitions are proven using succinct zero-knowledge proofs, enabling a ZKVM-backed smart contract layer with native privacy. BitCell makes three primary contributions: (i) a proof-of-computation consensus mechanism whose computational task is verifiable, bounded, non-parallelisable by pooling, and intellectually non-trivial; (ii) a game-theoretic proof that the combination of pairwise tournaments, anonymised pairing, non-transferable victory rights, and reputation gating renders cartel coordination strictly dominated in a Bayesian Nash equilibrium; and (iii) a native ZKVM execution environment for privacy-preserving smart contracts.
Billions of dollars are lost every year in DeFi platforms by transactions exploiting business logic or accounting vulnerabilities. Existing defenses focus on static code analysis, public mempool screening, attacker contract detection, or trusted off-chain monitors, none of which prevents exploits submitted through private relays or malicious contracts that execute within the same block. We present the first decentralized, fully on-chain learning framework that: (i) performs gas-prohibitive computation on Layer-2 to reduce cost, (ii) propagates verified model updates to Layer-1, and (iii) enables gas-bounded, low-latency inference inside smart contracts. A novel Proof-of-Improvement (PoIm) protocol governs the training process and verifies each decentralized micro update as a self-verifying training transaction. Updates are accepted by PoIm only if they demonstrably improve at least one core metric (e.g., accuracy, F1-score, precision, or recall) on a public benchmark without degrading any of the other core metrics, while adversarial proposals get financially penalized through an adaptable test set for evolving threats. We develop quantization and loop-unrolling techniques that enable inference for logistic regression, SVM, MLPs, CNNs, and gated RNNs (with support for formally verified decision tree inference) within the Ethereum block gas limit, while remaining bit-exact to their off-chain counterparts, formally proven in Z3. We curate 298 unique real-world exploits (2020 - 2025) with 402 exploit transactions across eight EVM chains, collectively responsible for $3.74 B in losses. We demonstrate that on-chain ML governed by PoIm detects previously unseen attacks with over 97% attack detection accuracy and 82.0% F1. A single inference, such as one made via an external call, typically incurs zero cost. Fully on-chain inference consumes 57,603 gas (≈ $0.18) for linear models, 143,647 gas (≈ $0.49) for CNN(F2, K1), and 506,397 gas (≈ $1.77) for CNN(F8, K4) on L1 (e.g., Ethereum). Our results show that practical and continually evolving DeFi defenses can be embedded directly in protocol logic without trusted guardians, and our solution achieves highly cost-effective protection while filling a critical gap between vulnerability scanners and real-time transaction screening.
With the rise of smart contracts, decentralized autonomous organizations (DAOs) have emerged in public good auctions, allowing "small" bidders to gather together and enlarge their influence in high-valued auctions. However, models and mechanisms in the existing research literature do not guarantee non-excludability, which is a main property of public goods. As such, some members of the winning DAO may be explicitly prevented from accessing the public good. This side effect leads to regrouping of small bidders within the DAO to have a larger say in the final outcome. In particular, we provide a polynomial-time algorithm to compute the best regrouping of bidders that maximizes the total bidding power of a DAO. We also prove that such a regrouping is less-excludable, better aligning the needs of the entire DAO and the nature of public goods. Next, notice that members of a DAO in public good auctions often have a positive externality among themselves. Thus we introduce a collective factor into the members' utility functions. We further extend the mechanism's allocation for each member to allow for partial access to the public good. Under the new model, we propose a mechanism that is incentive compatible in generic games and achieves higher social welfare as well as less-excludable allocations.