Faculty governance in higher education depends on transparent participation, reliable quorum enforcement, accountable record keeping, and strict alignment with institutional regulations. Conventional departmental council processes provide formal authority and academic deliberation, but they often rely on manual documentation, fragmented records, and procedural enforcement that is difficult to verify after the fact. This work presents an integrated hybrid Decentralized Autonomous Organization (DAO) framework for faculty governance that combines regulatory alignment analysis, a working smart-contract prototype, and scenario-based simulation. The framework is designed for university departmental councils and is structured across three layers: off-chain community governance, on-chain protocol governance, and off-chain execution governance. It expands prior conceptual work by incorporating governance dimensions related to roles, incentives, membership, communication, decision-making, identity, auditability, conflict-of-interest handling, and institutional ratification. The evaluation simulates 1488 proposals across twelve scenarios covering four faculty sizes (15, 30, 50, and 100 members) and three adoption levels (low, moderate, and high). Scenario results indicate that adoption intensity is the dominant driver of governance performance: mean participation increases from about 33% under low usage to about 85% under high usage, quorum achievement rises from about 6% to about 96%, and execution rises from about 19% to about 70%. Relative to a modeled conventional workflow baseline, the DAO-supported process reduces decision-cycle time by about 76%, improves audit completeness by about 30%, and increases traceability from about 0.63 to 1.00. The results indicate that DAO-assisted faculty governance can strengthen transparency, procedural consistency, and auditability while preserving legally mandated university authority, but its practical value depends on sustained participation, privacy safeguards, cost control, and clearly defined hybrid control points.
Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho, Thomas Hildebrandt · 5 authors
Abstract Smart contracts manage blockchain assets and embody business processes. Yet, mainstream languages lack explicit support for process concepts such as roles, action dependencies, and time constraints, leading to increased implementation complexity and analysis challenges. To address this, we use Dynamic Condition Response (DCR) graphs, a formal business process modeling language, to formalize the semantics of smart contract business logic. Modeling smart contracts in DCR graphs involves translating their underlying behavioral logic into a declarative visual model using DCR’s explicit constructs for events, roles, data, time, and inter-event relationships. Furthermore, we systematically model 15 common high-level smart contract design patterns , representing recurring solutions to business logic-level problems. These formalizations reduce ambiguity compared to informal descriptions and serve as language-independent specifications. We demonstrate the modeling process through three complete smart contract case studies that combine six design patterns. Our modeling methodology, formalizations, and correspondence between smart contract semantics and DCR graphs enable future automated analysis and verification.
Smart contract auditing remains challenging because vulnerabilities often emerge only under complex execution conditions, cross-transaction interactions, and environment-dependent assumptions. Existing analysis techniques, including static analysis, symbolic execution, fuzzing, and recent LLM-assisted approaches, each provide useful but incomplete coverage, and monolithic auditing pipelines often struggle to balance search breadth, reproducibility, and reporting reliability. This paper presents SEMA, a self-evolving multi-agent auditing framework for smart contracts that formulates auditing as a resource-bounded discovery of concrete counterexamples under replay-certified reporting semantics. SEMA combines heterogeneous specialized agents, an orchestrator, a shared artifact-centric knowledge base, and a replay-based referee. During auditing, agents generate and consume reusable artifacts, such as candidate invariants, refuted hypotheses, transaction templates, and coverage cues, allowing the shared search state to evolve across rounds without modifying the analyzers themselves. To ensure reporting reliability, findings are accepted only when the referee can replay the candidate scenario under a pinned execution configuration and confirm violation of an executable security property. We further evaluate SEMA on an annotated smart contract benchmark under a fixed 300 s budget per contract. The full system achieves 0.9469 instance recall, 0.9441 success rate, and 0.9445 macro-average category recall on the retained executable subset, outperforming both symbolic-only and fuzzing-only baselines, as well as multi-agent ablations that disable dynamic knowledge evolution or cross-agent artifact reuse.
Abstract We introduce Koan, a system for compiling natural language DeFi requests into executable safety-validated directed acyclic graphs (DAGs). Assembling correct multi-step DeFi workflows requires sequencing irrevocable on-chain transactions across heterogeneous protocols, demanding flexible intent understanding and strict execution discipline simultaneously - a combination no existing tool provides. Koan addresses this in two phases. Phase 1 translates user intent into a typed graph via an LLM with deterministic fallback heuristics. Phase 2 validates that graph, injects missing safety nodes, and executes with dependency-aware scheduling. We evaluated on 1,000 prompts across 9 DeFi categories. Intent-to-workflow correctness reached 82.4%; DAG validity 93.6%. The Safety Injector raised price-impact check coverage from 41.2% to 98.4%, and 7.3% of all workflows were aborted by injected checks identifying excessive risk. Workflow authoring averaged 2.4 min versus 46.8 min for manual scripting (a 20x speedup), and compiled flows achieved 97% execution success with 18% gas savings on matched DEX routes under testnet conditions. Keywords Blockchain systems, decentralized finance, intent compilation, large language models, workflow orchestration.
Background: Healthcare organizations face unprecedented challenges in maintaining process compliance due to increasingly federated data and systems topologies, coupled with complex state, federal, and jurisdictional regulatory compliance and verification requirements. The emergence of distributed ledger technology (DLT) and artificial intelligence presents both transformative opportunities and significant compliance challenges. These emerging technologies enable computing paradigms that shift toward data locality models where computational models meet the data rather than moving sensitive patient information across organizational boundaries. This computational approach offers innovative pathways to mitigate data breach risks, while simultaneously introducing new verification complexities as the underlying technologies continue to advance: healthcare entities must cryptographically prove that operations performed on locally-held data were executed according to approved specifications while enabling selective disclosure capabilities across entity lines. However, traditional verification mechanisms lack the cryptographic guarantees necessary for these privacy-preserving, multi-entity healthcare workflows, creating substantial risks in clinical decision-making, patient privacy, and regulatory adherence. Objective: This paper introduces the ZK-PRET Business Process Prover framework that integrates Object Management Group (OMG) business process standards with zero-knowledge cryptographic verification to enable privacy-preserving healthcare process compliance across distributed systems. Methods: We developed a multi-layer architecture combining formal business process modeling, zero-knowledge proof generation, and regulatory compliance verification. The framework extends established OMG standards with cryptographic verification capabilities to achieve verifiable compliance, privacy preservation, and regulatory accountability. Implementation testing was conducted in synthetic data environments designed to represent real-world healthcare scenarios.¹ These environments enable comprehensive modeling and testing of multi-entity process orchestration patterns while maintaining privacy protections essential for healthcare research and development. All scenarios, clinical examples, and process expressions presented in this paper utilize synthetic data to ensure no real patient data, clinical records, or identifiable health information was used. Results: The ZK-PRET Business Process Prover framework demonstrates practical applicability across many healthcare domains including treatment planning, telemedicine coordination, healthcare administration, consumer health services, multi-entity clinical trials, and supply chain management. Implementation results demonstrate cryptographic verification capabilities that enable mathematical prevention of regulatory violations rather than post-hoc detection. The results demonstrate configurable privacy preservation through zero-knowledge verification and consistent proof sizes suitable for modeling complex orchestrations, while leveraging already widely used Web 2 process models, suitable for multiple runtime deployment topologies. Conclusions: Zero-knowledge healthcare process verification represents a foundational technology for regulatory compliance in distributed healthcare systems. While agentic AI systems present important opportunities for automation, the underlying requirement for verifiable process compliance through cryptographic means brings broader challenges. ZK-PRET Business Process Prover addresses these challenges in healthcare transformative flows, enabling safer deployment of autonomous systems while maintaining regulatory standards.
Omer Aziz, Muhammad Shoaib Farooq, Adel Khelifi, Abdullah Khalid Omer
<title>Abstract</title> The digital preservation of cultural heritage has advanced considerably through blockchain technologies , offering secure, immutable, and decentralized management of museum records. However, traditional blockchain frameworks suffer from scalability limitations, leading to high transaction costs, network congestion, and inefficient resource utilization—particularly in virtual museum environments with dynamic user activity. To address these challenges, we propose VERAONET (Virtual Ecosystem for Rewards and Archaeological Operations Network), a novel Layer-2 blockchain framework designed specifically for digital heritage applications. VERAONET introduces a pluggable consensus architecture, enabling dynamic switching between Proof of Work (PoW), Adjustable PoW (APoW), Proof of Stake (PoS), and Delegated Proof of Stake (DPoS) mechanisms in response to real-time network conditions. The framework was evaluated in two experimental environments: a Ganache-based local simulation (10–500 users) and a Geth virtual testbed (50–10,000 users). Results indicate that PoS and DPoS significantly outperformed PoW and APoW under high-load conditions, reducing latency, gas consumption, and chain bloat. Conversely, PoW and APoW proved effective in low-traffic, high-security scenarios. The adaptive consensus algorithm enhanced transaction finality and resource efficiency, demonstrating strong suitability for dynamic virtual museum ecosystems. VERAONET thus provides a scalable, sustainable, and cost-effective blockchain infrastructure tailored for cultural heritage preservation. Future work will focus on integrating AI-driven optimizations, supporting cross-chain interoperability, and embedding decentralized governance models.
Computational research depends on the ability to independently reproduce results, yet modern workflows are fragile: they drift across environments, depend on undocumented assumptions, and often fail silently. ValiChord provides a decentralised, agent‑centric infrastructure for independent reproducibility validation. Validators re‑execute workflows in diverse environments, generate cryptographically signed attestations, and contribute structured detector evidence that captures environment drift, dependency skew, execution variability, and workflow fragility. A commit–reveal protocol preserves validator independence, while Harmony Records synthesise divergent outcomes without collapsing them into binary judgements. ValiChord validates computation, not data provenance, and is explicit about this boundary: it strengthens the computational layer of scientific integrity without claiming to detect data fabrication. The system is built on Holochain, not blockchain, ensuring tamper‑evident provenance without global ledgers, tokens, or consensus mechanisms. Reference implementation and detector suite: https://github.com/topeuph-ai/ValiChord
This project is not abandoned. It is frozen. Reason for freeze: The work entered an infinite refinement loop. The architecture evolved, but external peer review, validation feedback, or community contribution did not materialize. Continuing alone without structural feedback ceased to be research and became exhaustion. What is SDIA? SDIA — Semantic Domain Integration Architecture — is the governing umbrella of the DEIP ecosystem. It is not a product, not a platform, not a vendor pattern. It is an architectural invariant: business domain semantics govern every layer of the integration stack simultaneously — gateway routing, runtime resolution, orchestration, event channels, and data contracts. The governing principle: 👉 The domain is the primary key. Always. Across every layer. Regardless of technology. What This Document Establishes This document is the comprehensive prior art record for the SDIA ecosystem. It establishes formal protection across: 4 core components — GDCR · DDCR · ODCP · DCEP 1 forward declaration — DCBP (Domain-Centric Data Pattern, discovered March 23, 2026, Warsaw) 50 named architectural variants 90 control-plane and metadata routing variants 11 domain application patterns — Kubernetes · Multi-Cloud · Event-Driven · AI/LLM · Industrial IoT · Service Mesh · Data Mesh · GraphQL Federation · Zero Trust · Semantic Versioning · Blockchain/Web3 Complete mathematical model — f(k) → v — deterministic, O(1), fail-fast, language-agnostic, platform-agnostic Full algorithmic prior art — Phantom v12 reference implementation (JavaScript) + cross-language ports (Lua · Java · C# · Python) The Mathematical Core At its foundation, SDIA routing is defined as: f(k) → v Where k = routing key constructed from semantic domain components, and v = resolved backend endpoint. Properties: Deterministic — same input = same output, always, in any language, any platform O(1) complexity — independent of metadata store size, domain count, or platform Fail-fast — unregistered keys rejected at ~0.1ms, zero backend exposure Total over governed space — only explicitly registered combinations resolve Invariant under infrastructure change — engine never changes, metadata evolves Validated Results ~2,067,904 requests processed 100% routing accuracy · zero routing failures Sub-4ms resolution latency · 99.99% uptime 8 enterprise platforms · 5 programming languages · 13 configurations 42 IoT sensors · 4 environments Platforms: SAP BTP APIM · AWS API Gateway · Azure APIM · Kong Gateway · Kong on Kubernetes · Netflix Zuul · Industrial IoT (Mosquitto + Node-RED) · Kubernetes + Istio Ecosystem Architecture Layer Component Role Gateway GDCR Semantic facade — 1 proxy per domain, not per system Runtime DDCR 7-stage deterministic resolution engine Orchestration ODCP Domain-centric package, iFlow, and credential governance Events DCEP Domain-centric event channel governance Data DCBP Domain-centric data contracts and data product routing Umbrella SDIA Unifying semantic addressing paradigm across all layers What SDIA Protects Any implementation — regardless of vendor, product name, platform, or programming language — that: Uses domain-centric routing as the primary organizational principle Employs metadata-driven resolution satisfying f(k) → v Implements semantic URL patterns: /domain/entity/action/target Enforces domain boundaries as security, governance, or semantic perimeters Decouples consumer addresses from backend implementation details ...constitutes a derivative application of the SDIA prior art established February 6, 2026. Prior Art Chain February 6, 2026 — Wayback Machine (Marco Zero · first public disclosure) February 7, 2026 — Medium (first formal publication) February–March 2026 — Zenodo (5 DOI-published specifications) March 2026 — IP.com Prior Art Database · IPCOM000277630D–000277633D March 2026 — USPTO Trademark Applications · 99680660 (GDCR) · 99691792 (DDCR) Version History Version Status DOI v2.0 ✅ CURRENT zenodo.org/records/18877636 v1.0 ⚠️ Superseded zenodo.org/records/18877636 Links Repository: github.com/rhviana/deip SDIA Extension (this document): https://zenodo.org/records/18877636 DEIP Source of Truth: https://doi.org/10.5281/zenodo.19004802 Citation (v2.0) APA: Viana, R. L. H. (2026). SDIA — Semantic Domain Integration Architecture: Complete Extensions, Variants & Prior Art Documentation — Version 2.0. Zenodo. https://zenodo.org/records/18877636 Author Ricardo Luz Holanda Viana Enterprise Integration Architect | Creator of DEIP Ecosystem | SAP BTP Integration Suite Expert | SAP Press Author Warsaw, Poland · March 2026 · ORCID: 0009-0009-9549-5862 "Technology changes by the quarter. Business processes last for decades. The domain never lies."
The adoption of blockchain-based smart contracts for the trading of goods and services promises greater transparency, automation, and trustlessness, but also raises challenges related to payment integration and modularity. While business analysts (BAs) can express business logic and control flow using BPMN and decision rules using DMN, payment tasks that involve concrete transfers (on-chain, off-chain, cross-chain, or hybrid) require careful implementation by developers due to platform-specific constraints and semantic richness. To address this separation of concerns, we introduce a methodology within the context of the smart contract-as-a-service (SCaaS) approach that supports (1) identifying and mapping generic payment tasks in BPMN to pre-deployed payment smart contracts, (2) augmenting BPMN models with matching payment fragments from a pattern repository, and (3) automatically transforming the augmented models into smart contracts that invoke the appropriate payment services. Our approach builds on prior work in automated BPMN-to-smart contract transformation using Discrete Event–Hierarchical State Machine (DE-HSM) multi-modal modeling to capture process semantics and nested transactions, while enabling payment service reuse, extensibility, and the separation of concerns. We illustrate this methodology via representative use cases spanning conventional, DeFi, and cross-chain payments, and discuss the implications for modular contract deployment and maintainability.
Choonhwa Lee, Yibo Zhang, Dani Mertens, Eunsam Kim
Decentralized workflows supported by provenance data aim to combine into a platform with high trustworthiness, transparency, and accountability. Despite the huge potential of the approach, one limitation of the system architecture is that it lacks access to external data, limiting the functionality and potential use cases of the workflow. To address this limitation, we extend an existing decentralized workflow with a provenance bridge, enabling the workflow to access external provenance-supported data without damaging the trustworthiness of the system. The introduction of this bridge effectively broadens the range of use cases for the decentralized workflow by opening it to various external provenance-supported data sources. This article presents the architectural design of the provenance bridge-enabled workflow system, and discusses our prototype implementation effort along with evaluation results. Specifically, we have designed and implemented the architectural framework of the provenance bridge that expands the provenance domain boundary by incorporating support for provenance model translation and oracle-based external data access. The proposed approach lays a solid foundation for a wider adoption of smart contract-based workflow systems by effectively bridging the gap between different provenance domains.
Enterprises are rapidly shifting from human-interpreted dashboards to Autonomous Analytical Entities (AAE) that execute decisions directly on production systems. This transition introduces a new failure mode—Agentic Divergence—where decentralized agents act on misaligned, drifted, or out-of-scope data products and metadata, leading to high-impact errors at scale. This paper proposes the Autonomous Analytical Coherence (AAC) framework, centered on an Analytical Control Plane (ACP) that inserts a mandatory, machine-enforced governance layer between AAEs and decentralized data products. The ACP mandates Agentic Data Contracts (ADC) as runtime dependencies and enforces Kullback–Leibler (KL) divergence-based drift checks within Trusted Execution Environments (TEE) to safeguard both analytical coherence and data sovereignty. Simulation-based experiments across finance and logistics workloads indicate that AAC reduces erroneous autonomous transactions by 77% compared with uncoordinated agent deployments, with only a 25 ms median increase in latency. These results demonstrate that treating governance as a runtime dependency is a practical path toward safe, high-stakes autonomous analytics in enterprise data meshes.
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.
An Explainable Audit Trail (EAT) records process execution traces of an agentic workflow. EAT can enable an organisation to efficiently remain compliant with regulations by presenting its audit results to it. However, current state of the art in EAT lacks privacy protection of agent's models which can be intellectual properties of the organisation. Exposing audit trails to external entities may facilitate orchestration of attacks on the agent's model. Auditing a complex workflow will require verification of dependencies among tasks as preconditions to execute a task. Further, it is necessary for the audit algorithm to ensure that a process execution trace follows the pre-planned process execution model for security reasons, i.e., audit should include functionality that can check if the agents have deviated from its planned process execution models. In this paper, we build a secure EAT that can address these gaps in the state of the art in EAT for agentic workflows. Our main contribution is the application of zero-knowledge-proof on verifying audit procedures. It proves the audit has validated correctness of chain-of-thoughts, the execution trace at the runtime matches the planned process execution , and complete traceability among logs of a complex workflow involving dependencies among the tasks in terms of preconditions. Our solution provides a trust-less infrastructure to verify the audit results to external entities while not exposing the audit trails. We used lattice-based zero knowledge proof for this procedure. We provide an analysis on the EAT procedure. We show experimental evaluation of the EAT with workflow dataset.
Understanding the economic intent of Ethereum transactions is critical for user safety, yet current tools expose only raw on-chain data or surface-level intent, leading to widespread "blind signing" (approving transactions without understanding them). Through interviews with 16 Web3 users, we find that effective explanations should be structured, risk-aware, and grounded at the token-flow level. Motivated by these findings, we formulate TxSum, a new user-centered NLP task for Ethereum transaction understanding, and construct a dataset of 187 complex Ethereum transactions annotated with transaction-level summaries and token flow-level semantic labels. We further introduce MATEX, a grounded multi-agent framework for high-stakes transaction explanation. It selectively retrieves external knowledge under uncertainty and audits explanations against raw traces to improve token-flow-level factual consistency. MATEX achieves the strongest overall explanation quality, especially on micro-level factuality and intent quality. It improves user comprehension on complex transactions from 52.9% to 76.5% over the strongest baseline and raises malicious-transaction rejection from 36.0% to 88.0%, while maintaining a low false-rejection rate on benign transactions.
Oscar Medina, Brenda Meloni, Ana Strub, Marelo Martín Marciszack
Event patterns are used to model interactions between smart contracts and their environment, improving the efficiency, security, and flexibility of applications based on blockchain technologies. Event pattern-driven smart contract modelling is an emerging trend. Defining a new pattern or selecting a pre-existing one from a limited catalog is a fundamental activity for any analysis model that utilizes event patterns. This study presents a proposal to manage a catalog of event patterns that can be applied to the conceptual modelling of smart contracts and incorporates machine learning techniques to optimize pattern selection. To test this proposal, a prototype application called PatCat (Pattern Catalogue) was developed, using a decentralized electronic voting application as a case study. The incorporation of patterns at the beginning of the modelling process simplifies and clarifies the elicitation of requirements, among other benefits, while the use of machine learning accelerates the description of the problem situation. Consequently, a specialized application for managing a catalog of event patterns, supported by machine learning techniques, proves useful in standardizing and streamlining smart contract modelling tasks.
Abstract Background: Healthcare organizations face unprecedented challenges in maintaining process compliance due to increasingly federated data and systems topologies, coupled with complex state, federal, and jurisdictional regulatory compliance and verification requirements. The emergence of distributed ledger technology (DLT) and artificial intelligence presents both transformative opportunities and significant compliance challenges. These emerging technologies enable computing paradigms that shift toward data locality models where computational models meet the data rather than moving sensitive patient information across organizational boundaries. This computational approach offers innovative pathways to mitigate data breach risks, while simultaneously introducing new verification complexities as the underlying technologies continue to advance: healthcare entities must cryptographically prove that operations performed on locally-held data were executed according to approved specifications while enabling selective disclosure capabilities across entity lines. However, traditional verification mechanisms lack the cryptographic guarantees necessary for these privacy-preserving, multi-entity healthcare workflows, creating substantial risks in clinical decision-making, patient privacy, and regulatory adherence. Objective: This paper introduces the ZK-PRET Business Process Prover framework that integrates Object Management Group (OMG) business process standards with zero-knowledge cryptographic verification to enable privacy-preserving healthcare process compliance across distributed systems. Methods: We developed a multi-layer architecture combining formal business process modeling, zero-knowledge proof generation, and regulatory compliance verification. The framework extends established OMG standards with cryptographic verification capabilities to achieve verifiable compliance, privacy preservation, and regulatory accountability. Implementation testing was conducted in synthetic data environments designed to represent real-world healthcare scenarios.¹ These environments enable comprehensive modeling and testing of multi-entity process orchestration patterns while maintaining privacy protections essential for healthcare research and development. All scenarios, clinical examples, and process expressions presented in this paper utilize synthetic data to ensure no real patient data, clinical records, or identifiable health information was used. Results: The ZK-PRET Business Process Prover framework demonstrates practical applicability across many healthcare domains including treatment planning, telemedicine coordination, healthcare administration, consumer health services, multi-entity clinical trials, and supply chain management. Implementation results demonstrate cryptographic verification capabilities that enable mathematical prevention of regulatory violations rather than post-hoc detection. The results demonstrate configurable privacy preservation through zero-knowledge verification and consistent proof sizes suitable for modeling complex orchestrations, while leveraging already widely used Web 2 process models, suitable for multiple runtime deployment topologies. Conclusions: Zero-knowledge healthcare process verification represents a foundational technology for regulatory compliance in distributed healthcare systems. While agentic AI systems present important opportunities for automation, the underlying requirement for verifiable process compliance through cryptographic means brings broader challenges. ZK-PRET Business Process Prover addresses these challenges in healthcare transformative flows, enabling safer deployment of autonomous systems while maintaining regulatory standards.
Recent advances in large language models (LLMs) have enabled the emergence of intelligent agents capable of performing complex multi-step tasks across various domains. In parallel, the growth of Web3 has introduced a decentralized web infrastructure, yet remains largely inaccessible to non-technical users due to operational complexity, fragmented information, and security risks. In this article, we present Web3Agent , an AI agent system that integrates LLM-based interaction with blockchain environments to enable language-driven on-chain operations. Web3Agent automatically decomposes user instructions into structured workflows, dynamically queries blockchain data and APIs, and performs multi-step operations such as asset transfers, token swaps, and smart contract execution. Web3Agent incorporates real-time inspection, error handling, and interaction transparency across its operation log, and flow visualization components. We evaluate the system and perform ablation study with customized dataset in a simulated environment, demonstrating its feasibility in orchestrating complex Web3 tasks and highlighting implications for agent-based abstraction in decentralized systems.
Flavio Corradini, Alessio Galassi, Alessandro Marcelletti, Barbara Re
Blockchain has been largely adopted in several sectors through decentralized applications. These rely on smart contracts, whose implementation can diverge from the intended logic, leading to unexpected behaviors. Such behaviors can be identified by observing the data produced within smart contracts’ execution, employing compliance checking techniques. Their adoption poses a main limitation since the traditional rule specification languages do not explicitly refer to the blockchain. To address this limitation, we propose a domain-specific language, called CoBlock , to define compliance rules by relying on blockchain characterizations as a first-class citizen. This enables a tailored framework for compliance checking, supporting the definition of rules to check smart contract execution data. The framework is implemented as a web application. We demonstrate and evaluate the applicability of the language and the accuracy and feasibility of the framework using two real-world decentralized applications, namely Augur and PancakeSwap.
Lorena Baigorria, Ana Gabriela Garis, Daniel Eduardo Riesco
Blockchain es la base tecnológica de una nueva forma de realiz-ar transacciones de manera segura en una red descentralizada. Dicha tecnología permite registrar la validez y el origen de los datos, y realizar transacciones de manera digital, compartida, inalterable y sin la intervención de intermediarios. Frecuentemente, las transacciones requieren de lógica automa-tizada. En estos casos, se vuelve necesaria la definición de con-tratos inteligentes, programas de computación almacenados en Blockchain que se ejecutan automáticamente cuando se cumplen condiciones predeterminadas. Los errores en contra-tos inteligentes pueden tener graves consecuencias, especial-mente en ámbitos como finanzas descentralizadas. Una clara definición de las condiciones es esencial; sin embargo, éstas son generalmente descriptas en lenguaje natural por las partes involucradas, lo que conlleva a la ambigüedad de interpretación por parte de los programadores del contrato. Por otro lado, los errores en la programación también pueden derivar a que el contrato no se ejecute como se esperaba. La calidad del contra-to inteligente podría ser mejorada si las condiciones fueran especificadas en UML con OCL, y luego transformadas al len-guaje de modelado Alloy para llevar a cabo la verificación y validación formal a través del método Model Checking. En este artículo, se describe una línea de investigación que propone un modelo para la especificación de contratos inteligentes en UML y OCL, complementado con una transformación automática a Alloy para su verificación y validación. Dicho modelo contribuye a realizar una auditoría más rigurosa de contratos inteligentes antes de despliegue en Blockchain.
Smart contracts are central to blockchain ecosystems, yet their development remains technically demanding, error-prone, and tied to platform-specific programming languages. This paper introduces SCEditor-Web, a web-based modeling environment that combines model-driven engineering (MDE) with generative artificial intelligence (Gen-AI) to simplify contract design and code generation. Developers specify the structural and behavioral aspects of smart contracts through a domain-specific visual language grounded in a formal metamodel. The resulting contract model is exported as structured JSON and transformed into executable, platform-specific code using large language models (LLMs) guided by a tailored prompt engineering process. A prototype implementation was evaluated on Solidity contracts as a proof of concept, using representative use cases. Experiments with state-of-the-art LLMs assessed the generated contracts for compilability, semantic alignment with the contract model, and overall code quality. Results indicate that the visual-to-code workflow reduces manual effort, mitigates common programming errors, and supports developers with varying levels of expertise. The contributions include an abstract smart contract metamodel, a structured prompt generation pipeline, and a web-based platform that bridges high-level modeling with practical multi-language code synthesis. Together, these elements advance the integration of MDE and LLMs, demonstrating a step toward more accessible and reliable smart contract engineering.
Edgar Roberto Dulce Villarreal, Julio Ariel Hurtado Alegría, José García-Alonso
Interoperability between blockchain platforms remains a key challenge, particularly in sensitive domains such as healthcare, where the secure and consistent exchange of clinical information between institutions is essential. While technical interoperability solutions exist, semantic interoperability at the level of smart contracts continues to be a significant limitation. This paper presents MUISCA, a mechanism based on Model-Driven Engineering that enables the automatic generation of interoperable smart contracts across different blockchain platforms. By defining metamodels, abstract models, and transformation rules, MUISCA produces platform-specific code for technologies such as Ethereum and Hyperledger Fabric. The mechanism was validated through a healthcare case study focused on patient transfers between medical institutions, demonstrating its ability to support the secure exchange of clinical data. Additionally, its acceptance was evaluated through expert surveys assessing perceived usefulness and ease of use. Results show that MUISCA improves smart contract portability, reduces implementation errors, and enhances system security. The proposed solution contributes to advancing semantic interoperability in blockchain-based health information systems and provides a foundation for broader application in other critical domains that require high levels of integration and data protection.
Ensuring the integrity of business processes without disclosing confidential business information is a major challenge in inter-organizational processes. This paper introduces a zero-knowledge proof (ZKP)-based approach for the verifiable execution of business processes while preserving confidentiality. We integrate ZK virtual machines (zkVMs) into business process management engines through a comprehensive system architecture and a prototypical implementation. Our approach supports chained verifiable computations through proof compositions. On the example of product carbon footprinting, we model sequential footprinting activities and demonstrate how organizations can prove and verify the integrity of verifiable processes without exposing sensitive information. We assess different ZKP proving variants within process models for their efficiency in proving and verifying, and discuss the practical integration of ZKPs throughout the Business Process Management (BPM) lifecycle. Our experiment-driven evaluation demonstrates the automation of process verification under given confidentiality constraints.
Real-World Assets (RWAs) serve as a bridge between traditional financial instruments and decentralized infrastructures. By representing assets such as bonds, commodities, and real estate on blockchains, RWAs can extend the scope of decentralized finance. Industry forecasts further indicate rapid growth in tokenized RWAs after 2025, underscoring their potential role in the evolution of digital financial markets. However, in the current multi-chain environment, RWAs face challenges such as repeated authentication across multiple chains and inefficiencies arising from multi-step settlement protocols. To address these issues, we present a cross-chain framework for RWAs that emphasizes identity management, authentication, and cross-chain interaction. The framework integrates Decentralized Identifiers and Verifiable Credentials with customized attributes to support decentralized identification, and incorporates an authentication protocol based on Simplified Payment Verification to avoid redundant verification across chains. Furthermore, this paper adopts a cross-chain channel that supports efficient RWA settlements, and we refine its design so that the channel does not need to be closed immediately after each settlement, thereby reducing on-chain cost. We implement the framework and evaluate its performance via simulations, which confirm its feasibility and demonstrate improvements in efficiency for RWAs in cross-chain settings.
Aleksandr Kormiltsyn, Sowelu Avanzo, Vimal Dwivedi, Alex Norta · 5 authors
This paper explores conflict resolution in decentralized e-health prescription creation workflows, necessary for secure and efficient multi-stakeholder data sharing. Consensus mechanisms ensure consistency and enable trust across distributed systems. Decentralized Autonomous Organizations (DAOs) are adopted for decentralized decision-making in several domains but remain unexplored in e-healthcare. Current consensus mechanisms lack integration with governance models, limiting their adaptability to domain-specific requirements. Moreover, there is no existing consensus algorithm adapted for e-health, resulting in the lack of privacy, interoperability, and patient-centered data ownership. As a result, automatic conflict resolution in interorganizational e-health processes is complicated or almost impossible. To address this gap, we propose a domain-specific consensus algorithm adapted to the requirements of the e-health domain. The algorithm is embedded within a DAO-based governance framework, enabling transparency in decision-making among e-health stakeholders. Such integration enables automated, privacy-preserving conflict resolution in interorganizational e-health workflows. Following the Design Science methodology, the consensus algorithm for e-health DAO is based on stakeholder-driven requirements and evaluated using Colored Petri Nets (CPN). The evaluation shows the solution improves conflict resolution enabling fair, efficient, and privacy-aware collaboration in decentralized e-health.