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.
Darcy WE Allen, Chris Berg, Aaron M. Lane, Jason Potts
Abstract We develop a theory of decentralized autonomous organizations (DAOs) that explains why they exist in terms of what they do. In New Institutional Economics, firms exist to minimize the transaction costs of using a market. DAOs, which are a species of firm made of smart contracts, seem to extend this logic. But by observing how DAOs behave in the wild—through cases like Shapeshift, Uniswap, and Optimism—we reveal that the core value of a DAO is its capacity for dynamic adaptation in governance. DAOs enable fast, low-cost changes in governance to respond to shifting regulatory, financial, and competitive conditions. They are not just automation tools to reduce agency costs via token governance. Rather, they are mechanisms for organizational variation in governance itself. When the benefits of this adaptive mechanism exceed its costs, we predict the existence of a DAO.
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.
Abstract Decentralized exchanges (DEXs) allow traders to express their willingness to pay for quick execution through a public priority fee bidding mechanism. We provide evidence that high-fee DEX trades are more informative and contribute more to price discovery. Using address-level blockchain transaction data, we show that informed traders persistently bid higher fees to secure early execution, revealing a strong willingness to pay for execution priority. Further, analysis of Ethereum mempool data demonstrates that informed traders employ a “jump bidding” strategy, placing high initial bids to deter potential competitors.
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.
Constant Product Market Maker (CPMM) designs are the cornerstone of decentralized exchange, yet they inherently suffer from low capital efficiency and suboptimal liquidity provider (LP) incentives. In this work, we propose a novel extension of the classical CPMM model that utilizes idle liquidity within the pool to enable decentralized margin trading. We introduce a UTXO-based state management system to encode and track active margin positions, referred to as mUTXOs. We formally prove that this model closely mirrors the behavior of traditional CPMMs. Furthermore, we demonstrate how this architecture composes with standard Bitcoin interoperability solutions to facilitate cross-chain exposure, preserving a Bitcoin-native fee structure for a seamless user experience.
Autonomous agent commerce — where software agents hire, pay, and evaluate other agents at micropayment scale — creates a verification problem that existing approaches cannot solve. When Agent A pays Agent B $0.01 for a translation, who determines whether the translation is actually good? Human review is economically impossible. A central LLM evaluator is non-deterministic, non-reproducible, and empirically unreliable on ambiguous cases. The problem is not engineering — it is epistemological. Tarski (1936) proved that truth in a formal system cannot be defined within that system. Gödel (1931) proved that any consistent system contains true statements it cannot prove. Every content moderation system that has attempted automated truth verification confirms the theory: precision drops below 60% on context-dependent content. This paper argues that the correct response to the Oracle Problem in agent commerce is not better computation but better incentives. We propose a two-layer architecture: (1) deterministic validators that verify contract compliance — postconditions in the sense of Hoare (1969) and Meyer (1992) — handling the cases with zero ambiguity; and (2) Quality Markets, a competitive market of verification agents with reputational stake, grounded in prediction market theory (Wolfers & Zitzewitz, 2004), peer prediction (Miller et al., 2005), and the economics of information asymmetry (Akerlof, 1970). The design separates what can be verified mechanically from what requires judgment, and delegates judgment to economic competition rather than algorithmic authority. We analyze the mechanism's incentive properties, identify its limitations, and situate it within the broader Oracle Problem literature from philosophy, computer science, and decentralized finance.
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.
In a multipolar world with no trusted monetary coordinator, how do rational actors settle large-value transactions across trust boundaries? We model this as a non-cooperative game—the "Exit Game"—in which capital allocators choose between capturable settlement systems ("Stay") and neutral settlement ("Exit"). The model rests on four empirical axioms: persistent multipolarity, rational self-interest, computational hardness, and network effect persistence. We prove three results. First, the payoff advantage of Exit over Stay is strictly increasing in adoption: every term in the payoff differential favors Exit under maintained monotonicity conditions, and each actor's adoption threshold approaches zero under structural debasement (Theorem 1). Second, no coalition can sustain coordinated Stay, because permissionless access makes defection costless and the first defector captures fleeing capital (Theorem 2). Third, the resulting equilibrium is absorbing: the monotone adoption process converges to full adoption once a critical mass is reached, because trust conditions required for coordinated return cannot be reestablished (Theorem 3). The model is explicitly falsifiable: six conditions are identified under which the central claims would fail. Bitcoin is the unique asset satisfying the necessary properties for neutral settlement—a result proved by systematic elimination across seven asset classes in Hash (2026b).
Decentralized finance (DeFi) vaults-smart contracts that automate yield strategies across composable protocols-represent over $16 billion in total value locked yet lack standardized risk decomposition frameworks. We propose a graph-theoretic approach: representing vaults as directed acyclic graphs where nodes are typed by four atomic primitives (CONTRACT, ORACLE, GOVERNANCE, OPERATIONAL) and edges encode dependency relationships. This formalization enables node-level risk attribution, where every basis point of expected loss traces to a specific primitive. We calibrate base rates from a dataset of 449 documented exploits (2016-2026) totaling $15.7 billion in losses, sourced from DeFiLlama and validated against Rekt News. Key finding: CONTRACT failures dominate frequency (65%) while OPERATIONAL failures dominate severity (50% of losses)-a distinction invisible without formal decomposition. The framework provides: (i) a complete taxonomy covering all historical exploit root causes, (ii) transparent aggregation from node-level to vault-level risk, and (iii) crossprotocol comparison on a common basis. The framework does not predict exploits; rather, it provides the decomposition infrastructure that enables risk budgeting, concentration analysis, and board-level reportingcapabilities institutions require but DeFi currently lacks.
The first two papers of this series established, respectively, an empirical diagnosis of extractive economic structure and a formal theory of why such structures transition and what a coordination-respecting successor must be built of. This paper supplies the missing third element: concrete protocol specifications audited against the theory's own design criteria. Two cases are examined. The first is a credentialing crisis in elite corporate recruitment: the university degree, this paper argues, was never primarily a certificate of skill but a costly, compliance-based proxy for coordination capacity (Spence, 1973), adopted because coordination is expensive to verify directly and because executive review time — the scarce resource the credential filter economizes — is itself a coordination-bandwidth constraint, finite and unforceable in exactly the sense the second paper formalized. The paper's central technical contribution is the Adversarial Anti-Derivative Filter, an algorithm that restores direct, low-latency evaluation of coordination capacity at scale by generating a model's own baseline solution distribution and filtering submissions by their semantic distance from it — a computable test for the compliance/coordination distinction, situated against the AI-generatedtext detection literature and its documented arms-race limitations. The second case is shippingrouter, a local-first, open-source logistics telemetry protocol, audited section by section against the second paper's design triad: an open sink (value dissipates as demurrage avoided and labor saved, never re-accumulating as a token or reservoir), the absence of stock-accumulable gains, and universal forkability, with one terminological correction — the protocol's “zero-knowledge telemetry” is precise anonymized aggregation, not zero-knowledge proof, and the paper restates the mechanism accordingly. A supply-chain case study unifies both protocols under the second paper's stock/flow distinction: legacy enterprise software records participation after the fact, while a semantic telemetry layer detects coordination failure — the ripple not yet connected — before the flow-based checkpoint trips. The paper closes with a generalized protocol grammar, a checklist against which future builders can audit new architectures, and a set of counterarguments including the filter's own adversarial ceiling and Goodhart's law.
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.
This paper addresses the fundamental challenge of public goods provision-the Samuelsonian Dilemma-by proposing a decentralized mechanism termed Citizen's Executive Right (CER). Unlike traditional central-planning models, the CER mechanism endows agents with dispositional authority over tax revenues via Personal Public Accounts (PPAs). We introduce Temporal Scarcity-enforced by a "Rule of Lapsing"-as an information-forcing operator that collapses strategic delay into discrete preference signals. Our theoretical contributions are threefold: 1. Incentive Compatibility: We prove that under loss aversion, the mechanism achieves a symmetric Perfect Bayesian Equilibrium that is "detail-free" (Wilson Doctrine). 2. The Extended Walras's Law: We derive an identity showing that the clearing of the public sphere, measured by the Total Lapsing Rate ($\Lambda_t$), is a sufficient condition for general equilibrium. 3. Dynamic Stability: Using the Routh-Hurwitz criteria, we demonstrate that the balanced equilibrium is locally asymptotically stable, where the temporal pressure acts as a feedback operator. Our results suggest that institutionalizing time-limited dispositional rights can resolve the structural void in public finance, providing a robust blueprint for market-based public governance.
The Deflated Sharpe Ratio (Bailey and López de Prado, 2014) corrects an observed Sharpe ratio for the number of trials N behind it, separating genuine skill from the selection bias of a large backtest search. Its practical weakness is structural: N is supplied by the same researcher whose result it constrains. A search over a thousand configurations, reported as a single trial, satisfies the formula while defeating its purpose. The correction is sound; its input is self-reported. We present a construction that removes the researcher's discretion over that input. The trial set is committed to a Merkle tree before evaluation; the trial count N is the leaf count of the tree, not a reported scalar; and the winning strategy is bound, inside a zero-knowledge proof (a STARK), to be the maximum over the committed leaves. The deflation is then recomputed in-circuit on Merkle-pinned prices, net of a cost model the credential discloses, so the figure an allocator reads is derived by the circuit rather than asserted by the manager. The output is a credential, checkable by anyone, in seconds, without disclosure of the strategy, whose anti-overfitting correction cannot be understated within the committed search. We give the commitment scheme and its in-circuit binding; state precisely the manipulation it eliminates (understating N, cherry-picking a non-maximal winner, softening the cost model) and the residual trust it does not (off-ledger trials, closed only by forward pre-registration); and report a live implementation that additionally computes, in-circuit, the Probability of Backtest Overfitting over all C(16,8) = 12,870 combinatorially-symmetric splits (via recursive proof composition), together with the Probabilistic Sharpe Ratio and Hansen's Superior Predictive Ability. We demonstrate the system on its own flagship strategy, which it rules not significant (DSR 0.68, below the 0.95 bar), and publish that failure as the reference credential.
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.
A designer of verification chooses two things: what a verifier reads from disclosed evidence, and how far the information reaching the verifier can be held apart from the information reaching the party whose conduct verification is meant to discipline. This paper asks when these two margins can be designed separately. In a Bayesian persuasion model with a meanreading deterrence audience and a verifier who applies a coherent risk measure, the sender's value is a contest between two envelopes-a concave envelope serving deterrence and a convex envelope serving liability-whose gap carries all interaction between the margins and equals the sender's willingness to pay for audience separation. Directional factorisation is exact: which reads are gaming-proof is decided by the read's belief-curvature alone, independent of routing. Calibration and value factorisation fail generically, but the failure is confined to two explicit terms-a product-structure term, in which the read's responsiveness and the seal enter only through their product, and a band term activated by disclosure mandates-each of which vanishes to first order, at a saturated deterrence margin, or under level-insensitive reads. Finally, the routing margin's own invariance is a curvature pairing, not a consequence of coherence: equilibrium deterrence is unmoved by the seal, for every prior and every stake, if and only if a belief-convex read is paired with a concave compliance response; off the pairing, the seal moves deterrence through sheltering when the read is gameable and through retreat below an explicit saturation threshold even when the read is coherent.