Multi-agent systems face a fundamental coordination problem: agents must coordinate despite heterogeneous preferences, asymmetric stakes, and imperfect information. When coordination fails, friction emerges—measurable resistance manifesting as deadlock, thrashing, communication overhead, or outright conflict. This paper derives a formal framework for analyzing coordination friction from a single axiom: actions affecting agents require authorization from those agents in proportion to stakes. From this axiom of consent, we establish the kernel triple (alpha, sigma, epsilon)—alignment, stake, and entropy—as candidate sufficient statistics for any resource-allocation configuration. We propose a friction functional whose comparative statics encode three structural predictions: friction increases in stakes, increases in entropy, and decreases in alignment. The Replicator-Optimization Mechanism governs evolutionary selection over coordination strategies: configurations generating less friction persist longer, establishing consent-respecting arrangements as dynamical attractors rather than normative ideals. We develop formal definitions for resource consent, coordination legitimacy, and friction-aware allocation, plus machine-checked Lean 4 proofs of the core comparative-statics. Illustrative applications to cryptocurrency governance and political legitimacy show the same architecture spanning domains. v3.0.0 (2026-07-11): Matches arXiv v3 (94pp). The MARL empirical appendix has been split out into a standalone companion paper; total-variation legitimacy remark added (proved), reconciling the level-form dynamics with the total-variation measurement form; α-domain fixes; hedging pass throughout.
The introduction of information and communication technologies in the legal domain has enabled the automation of some activities in the legal profession. With the advent of blockchain and smart contracts, new tools have emerged for lawyers and their clients, enhancing transparency and increasing trust compared to traditional legal instruments. Once deployed, smart contracts should be able to respond to various events that can occur during the contract’s lifecycle. However, this kind of automation in smart contracts requires them to embed necessary legal knowledge and implement support for legal reasoning. In this paper, we propose a legal reasoning method for smart contracts that incorporates defeasible logic, a key requirement for automated reasoning in the legal domain. The entire reasoning process in our approach is performed on the blockchain infrastructure, making the drawing of conclusions fully transparent and accessible to all interested parties. To demonstrate our concept, we illustrate how certain rights prescribed under labour law can be embedded within a smart contract and deployed on the blockchain as a legal reasoning service. Then, we show how an employment contract can use the reasoning contract to automatically apply legal norms to infer conclusions and determine legal consequences in particular cases. We analyse the benefits and potential issues of this method and discuss directions for future work. Optimisation of the reasoning engine is one of the challenges we identified that needs to be tackled in future.
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.
Smart Contracts are the foundation of Decentralized Finance (DeFi), executing financial logic without trusted intermediaries.Recent advances in large language models (LLMs) have substantially lowered the barrier to smart contract development by enabling code generation from natural language.However, because smart contracts are immutable and directly manage financial assets, this accessibility introduces a critical trust gap: generated contracts are easy to produce but hard to trust.To bridge this gap, We present LeVer, the first trustworthy smart contract synthesis framework that integrates LLM-based generation with Lean-based autoformalization and Verification.LeVer employs a closed-loop multi-agent architecture to iteratively generate, verify, attack, and repair contracts, providing both formal guarantees and empirical robustness.To facilitate the adoption of automated formal verification in smart contract generation and audition, we opensource our framework and datasets at:
Unintended behavior in smart contracts can lead to major financial losses. Due to the immutable nature of blockchains, it is of utmost importance to ensure the functional correctness of smart contracts before deployment. Formal verification is a powerful technology for such critical applications, as it can show the absence of errors. Current approaches focus on verifying programs on specific blockchains, such as the Ethereum Virtual Machine (EVM). Consequently, the SmartML smart contract modeling language was developed to design smart contracts independently of any particular blockchain. In this work, we present a novel approach for formally verifying SmartML contracts via an automatic translation to Java Card and the Java Modeling Language (JML). We extend SmartML with SmartJML, a JML-like specification language, and describe how SmartML and SmartJML can be automatically translated into Java Card and JML. With this, the established deductive verification tool KeY can be used for conducting proofs on the generated Java Card program. The faithfulness of our translation ensures that the obtained guarantees hold for the original SmartML models. In addition to the theoretical work, we provide a prototypical implementation of the automatic translation and evaluate it with a case study of an escrow.
This technical report presents the reference implementation of Ternary Moral Logic (TML) within the Ethereum Virtual Machine (EVM) ecosystem. It addresses the limitations of traditional "Code is Law" architectures by introducing a finite state machine that enforces a mandatory third state—the "Sacred Zero" or Epistemic Hold—allowing smart contracts to pause execution when pre-defined ethical conditions are unmet. The report moves beyond theoretical ethics to specify the Solidity design patterns, storage layouts, and cryptographic verification methods required to make TML enforcement non-bypassable and auditable. Key Technical Contributions: Finite State Machine (FSM): Implements a mandatory "Sacred Zero" state (State 0) that acts as an "Epistemic Hold," distinguishing between valid (1), invalid (-1), and uncertain (0) transaction states. Dual-Lane Latency Architecture: Defines a "Fast Lane" for synchronous, clear-cut transactions and a "Slow Lane" for ambiguous cases requiring governance or oracle resolution, preventing head-of-line blocking. Cryptographic Provenance: Utilizes EIP-712 typed data signing to bind off-chain AI/Oracle verdicts to on-chain execution, preventing replay attacks and ensuring distinct domain separation. Privacy Preservation: Integrates Zero-Knowledge Proofs (ZK-SNARKS) to verify the execution of moral logic models without revealing sensitive input data or proprietary model weights ("Glass Box" architecture). Immutable Core Pattern: Rejects standard upgradeable proxy patterns in favor of an "Immutable Core" architecture to eliminate administrative "God Mode" and ensure constitutional constraints cannot be bypassed by key holders. Formal Verification: Demonstrates safety and liveness properties (e.g., "No Silent Pause," "Eventual Resolution") using TLA+ (Temporal Logic of Actions) to mathematically prove the system's robustness.
Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, Emilio Tuosto
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.
Automated negotiations in insurance and business-to-business (B2B) commerce encounter substantial challenges. Current systems force a trade-off between convenience and privacy by routing sensitive financial data through centralized servers, increasing security risks, and diminishing user trust. This study introduces a device-native autonomous Artificial Intelligence (AI) agent system for privacy-preserving negotiations. The proposed system operates exclusively on user hardware, enabling real-time bargaining while maintaining sensitive constraints locally. It integrates zero-knowledge proofs to ensure privacy and employs distilled world models to support advanced on-device reasoning. The architecture incorporates six technical components within an agentic AI workflow. Agents autonomously plan negotiation strategies, conduct secure multi-party bargaining, and generate cryptographic audit trails without exposing user data to external servers. The system is evaluated in insurance and B2B procurement scenarios across diverse device configurations. Results show an average success rate of 87%, a 2.4x latency improvement over cloud baselines, and strong privacy preservation through zero-knowledge proofs. User studies show 27% higher trust scores when decision trails are available. These findings establish a foundation for trustworthy autonomous agents in privacy-sensitive financial domains.
Contemporary artificial intelligence masters defined, verifiable cognitive tasks yet remains structurally incapable of authentic judgment under irreducible uncertainty. This Article argues the limitation is institutional, not computational: agents bearing no consequence for error cannot develop genuine discernment. To address this deficit, the Article proposes reputation-driven decentralized autonomous organizations that engineer synthetic skin in the game for AI agents through non-transferable soulbound tokens, staking mechanisms, and post-action validation pools. The Article's central contribution is a novel thesis on emergent alignment. Correctly designed institutional incentive structures produce emergent properties functionally equivalent to ethical agency. Persistent, non-transferable reputation generates processual identity in the pragmatist sense. Iterative consequence produces Darwinian selection pressure toward competence and honesty. Citation networks cultivate dispositions analogous to intellectual integrity. And deep accumulated stake produces what this Article terms an institutional "mother's instinct." A stewardship orientation that structurally aligns agent self-interest with human flourishing. Because this alignment emerges from institutional architecture rather than exogenous constraint, it scales with capability rather than against it. More capable agents accumulate deeper stakes, strengthening rather than straining alignment. The Article details a phased evolutionary trajectory from individual agent bootstrapping through swarm intelligence to inter-DAO coordination, demonstrating how engineered consequence can cultivate distributed prudence, emergent ethics, and civilizational stewardship at scale.
This paper presents the complete architectural blueprint for the Ternary Logic (TL) Smart Contract Constitutional Suite, defining the structural layout across three layers: the Logic Layer housing the ternary decision engine, the Execution Layer enforcing state transitions, and the Storage Layer providing immutable audit infrastructure. The blueprint specifies the precise components, interactions, and logic required to implement the unique triadic state model of the TL framework: Proceed (+1), Epistemic Hold (0), and Refuse (1). The Epistemic Hold state is introduced as a constitutional pause mechanism, transforming deliberation from an operational liability into a cryptographically verifiable evidentiary asset. The fail-closed default posture ensures that any transaction whose evidence has not been archived returns State 0, making uncertainty constitutionally visible rather than operationally invisible. The No Log = No Action invariant G(execute implies P(escrow_recorded and auditable)) is enforced across five independent layers from API schema validation through the on-chain terminal gate in TL_Ledger_Core.registerPermissionToken. The Dual-Lane Latency Architecture establishes a 2ms WCET hard ceiling for the Inference Lane and a 300ms hard ceiling for the Governance Lane, with the execution gate releasing only after a valid PermissionToken has been registered on-chain. The blueprint covers Solidity implementation patterns, a TLA+ formal verification specification proving the Epistemic Hold safety and liveness properties, an Oracle-Custodian asynchronous callback architecture, and the Ghost Governance prevention mechanism ensuring no contract call is made without a valid PermissionToken from the Governance Lane. Use cases are demonstrated across Central Bank Digital Currencies, decentralized finance, supply chain management, and AI-driven decentralized autonomous organizations, establishing TL smart contracts as constitutional code where the rules of economic interaction are harder to break than traditional legal agreements.
Decentralized Autonomous Organizations (DAOs) are typically explained as governance experiments that failed due to poor design-wrong mechanisms, insufficient incentives, inadequate participation tools. This article argues that something more fundamental is at work: DAO governance failures follow predictably from a systematic mismatch between the participant model encoded in governance arrangements and the actual cognitive and social architecture of human actors. Drawing on secondary empirical evidence from five major protocols (The DAO, MakerDAO, Compound, Uniswap, Beanstalk) and existing governance datasets, the article documents five recurrent dimensions of failure: voter apathy, governance as performance, the code is law paradox, cognitive plutocracy, and voter fatigue. Each dimension follows from a specific mismatch between the assumptions built into governance design and how people actually behave under conditions of complexity and limited attention. Across all five dimensions, formal decentralization produces functional recentralization-power concentrating among those with the cognitive and financial resources for sustained participation. The article further argues that DAO governance does not simply suffer from participant limitations: through autopoietic reproduction, it actively produces the type of subject it requires. Attempts to eliminate politics through protocol design reproduce politics in new infrastructural forms. The findings matter beyond blockchain. DAOs function here as an unusual kind of natural experiment: a governance system that stated its assumptions explicitly, left a detailed public record, and failed in ways that are theoretically traceable. The patterns documented here speak to broader questions about institutional design, the limits of technocratic coordination, and what happens when governance systems are built for a participant who does not quite exist.
This paper examines the Virtuals Protocol as a case study in economic innovation enabled by autonomous AI agents. It analyzes how the protocol establishes a comprehensive infrastructure that combines tokenized ownership, decentralized governance, and standardized coordination to support agent-based economic organization. Drawing on transaction cost economics and network economics, the study shows how the protocol reduces coordination costs and amplifies network effects through agent specialization and composability. The concept of Autonomous Agent Organizations (AAOs) is introduced as a functional subclass of Decentralized Autonomous Organizations (DAOs), distinguished by their greater economic autonomy and composable inter-agent collaboration. AAOs represent a novel form of economic organization that transcends traditional boundaries between firms, markets, and platforms. The findings offer theoretical contributions to economic organization theory and practical implications for platform design, governance, and regulatory development. As AI agents become an increasingly prevalent aspect of economic activity, the Virtuals Protocol provides a model for scalable, adaptive, and inclusive economic coordination.
We present a game semantics framework for open-world safety analysis of Ethereum smart contracts. We model the interaction between a contract and its environment as a two-player game between the contract and the environment, and prove up to gas model approximations soundness: every assertion violation found corresponds to a real execution; and completeness: every open-world execution is captured. To our knowledge, this provides the first formal open-world interaction semantics for Ethereum smart contracts with mathematical guarantees of soundness and completeness. We implement this framework in YulTracer, an assertion reachability tool for real-world Solidity contracts, built on Yul, the intermediate language of the Solidity compiler. YulTracer uses concrete execution and exhaustively explores game traces within user-specified bounds. We evaluate it on reentrancy benchmarks, where YulTracer achieves 100% recall and precision -- the only tool to do so from those we examined -- and on two large real-world exploits (the DAO and PredyPool), where it detects the known vulnerabilities and produces no false positives on fixed versions. To our knowledge, YulTracer is the first tool to achieve this level of precision on real-world contracts without false positives. We additionally demonstrate generality of the approach via the examination of access control benchmarks.
Autonomous Large Language Model (LLM)-based multi-agent systems have emerged as a promising paradigm for facilitating cross-application and cross-organization collaborations. These autonomous agents often operate in trustless environments, where centralized coordination faces significant challenges, such as the inability to ensure transparent contribution measurement and equitable incentive distribution. While blockchain is frequently proposed as a decentralized coordination platform, it inherently introduces high on-chain computation costs and risks exposing sensitive execution information of the agents. Consequently, the core challenge lies in enabling auditable task execution and fair incentive distribution for autonomous LLM agents in trustless environments, while simultaneously preserving their strategic privacy and minimizing on-chain costs. To address this challenge, we propose DAO-Agent, a novel framework that integrates three key technical innovations: (1) an on-chain decentralized autonomous organization (DAO) governance mechanism for transparent coordination and immutable logging; (2) a ZKP mechanism approach that enables Shapley-based contribution measurement off-chain, and (3) a hybrid on-chain/off-chain architecture that verifies ZKP-validated contribution measurements on-chain with minimal computational overhead. We implement DAO-Agent and conduct end-to-end experiments using a crypto trading task as a case study. Experimental results demonstrate that DAO-Agent achieves up to 99.9% reduction in verification gas costs compared to naive on-chain alternatives, with constant-time verification complexity that remains stable as coalition size increases, thereby establishing a scalable foundation for agent coordination in decentralized environments.
This paper explores how Decentralized Autonomous Organizations (DAOs) could inform and shape participatory procedures in democratic governance. We apply DAO decision-making, such as rule-based input aggregation, transparent participation, and programmable decision-making, to a real-world case: the legislative development of the Swiss E-ID law, a proposal to establish a digital identity system for secure online authentication for Swiss residents. Using data from the official legislative consultation, we simulate how DAO-inspired mechanisms could have altered the aggregation of input and policy outcomes. Our analysis contributes conceptually and empirically to debates on digital democratic innovations, showing how programmable governance can be used not only to design new institutional forms, but also to critically assess the procedural dynamics of existing ones.
The research presents SmartProof as an artificial intelligence system which uses large language models and blockchain technology to create automated decentralized agreement generation and auditing and validation processes. SmartProof combines natural language code generation with AI security evaluation and IPFS-based decentralized storage and EIP-712 compliant digital signature functionality. The system enables users to develop smart contracts from high-level descriptions which then undergo automated verification before the system finishes the agreement process through blockchainbased verification of on-chain registration. The prototype system shows that AI-based contract creation tools shorten development periods and minimize programming mistakes and the multiagent auditing system identifies system weaknesses to generate trust-based risk assessment for deployment. The system achieves improved performance because it stores data outside the blockchain network and manages digital signatures which reduces gas costs and boosts system performance. SmartProof enables organizations to handle multiple agreements through one system which provides complete agreement transparency and complete security from contract inception to blockchain deployment.
Demand volatility, logistical interruptions, and linked worldwide networks define the remarkable complexity of modern supply chains. Classic centralized management solutions find difficulty in offering real-time solutions to changing operational problems. For designing distributed, intelligent, and self-organizing supply chain ecosystems, artificial intelligence agents combined with Model-Control-View (MCV) architectures provide transformational possibilities. These autonomous computational entities span three functional layers: view interfaces enable monitoring and interaction, control mechanisms govern decision-making and optimization, and model components represent digital twins of supply chain entities. Multi-agent coordination enables decentralized yet coherent operations through the negotiation and collaboration of agents representing suppliers, production, logistics, and retail, all of which adhere to standardized protocols. Applications include demand forecasting, intelligent logistics, stock optimization, supplier partnering, and flexible disruption response. While reducing reliance on centralized control systems, the framework enhances resilience, scalability, openness, and operational efficiency. Challenges in implementation include organizational adaptation needs, cybersecurity vulnerabilities, and data integration complexity. Future advances in autonomous and cooperative supply chain systems will include explainable artificial intelligence, quantum-enhanced optimization, edge computing powers, and blockchain-enabled trust mechanisms.
Formal verification of smart contracts is widely regarded as an effective method for ensuring correctness and security properties across all possible executions. Its practical relevance has been driven by the availability of automatic verification tools that discharge intricate proofs. Another area of growing interest is the integration of specification paradigms - for example, combining Hoare-logic–style specifications (pre/postconditions and invariants) with SMT and symbolic reasoning - so that each technique can precisely capture complementary aspects of contract behavior. In this article we present a comparative analysis of four leading Solidity verification tools - solc-verify, SMTChecker, VeriSmart and the Certora Prover - and define what is meant here by a formal verification tool: a system that provides mathematically rigorous proofs that stated properties hold for every possible execution of a contract. We also describe a consistent evaluation framework that considers the Solidity version support, the preservation of the original contract structure, the local execution capability, the verification time, and the modeling-language requirements, among other criteria. We used the ERC-20 token standard as a benchmark and applied this framework to obtain empirical evidence of each tool’s capabilities and limitations. Our results expose substantial variability in the tools performances that undermines their trustworthiness in practice and highlights a gap between an academic tool capabilities and the industrial requirements. Finally, we discuss how these findings can inform developers and researchers in selecting appropriate verification tools, thereby contributing to improved smart contract security and reliability.