A controlled timestamp-only projection of an ABD-style multiwriter quorum-register tag leaves completed reads current, exact, and linearizable while omitting the writer-identity component of the full protocol tag. Correctness therefore does not imply auditability at a distributed read boundary. A deterministic five-state host gives the protocol-independent companion: four sequential operations are totally ordered in real time, yet the read boundary exposes no source evidence. For an external specification fixed before the realization is chosen, zero-error boundary recovery exists exactly when all co-encoding locations agree and native source evidence aligns with the specified source and derivation relation. Under edit-generated source semantics, boundary agreement is equivalent to temporal zero-delay synchronization. Disjoint audited systems compose, but two independently verified services can assign incompatible roles to one shared location. Value projection likewise fails to preserve auditability; a certified refinement law transports it. A CAP partition carrier induces the corresponding read-boundary discriminator, but carrier data alone cannot supply the scheduler continuations required for an FLP transport. Finite DLS histories yield an exact stabilization-certificate bound and exclude one fixed evidence budget across all horizons. Protocol and replicated-storage rows illustrate the criterion across distributed boundaries. The substrate-independent ledger records the broader scope. Lean 4 verifies the finite models, reductions, abstraction maps, and internal bounds; the premises linking named systems to those models remain documentary.
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."
Distributed Ledger Technology (DLT) engineering practices commonly rely on the adaptation and development of components as key building blocks. However, incorrect component specifications can lead to architectural flaws, which may propagate to implementation stages and result in faulty configurations. To address this, we build on declarative modeling techniques from program verification and refactoring to formally specify DLT components and their architectural composition. We introduce a component-based approach, Alloy4CMD , for the formal modeling and analysis of DLT architectural design. This approach maps individual components into well-formed formal specifications, enabling decidable (bounded) reasoning and property checking. We further employ a lattice-based abstract interpretation to approximate component semantics, with verification carried out in Alloy through assertions expressing conformance to requirements. The analysis involves automated model finding with bounded consistency checks using the Alloy Analyzer. Our approach provides validated, reusable modules, composes them into a validated architectural meta-model that supports early-stage DLT architectural design, and is independent of any particular DLT platform.
Decentralized Autonomous Organizations (DAOs) are a class of Decentralized Applications (DApps) using smart contracts to facilitate governance processes. The design of DAOs is affected by additional complexity compared to other DApps due to the need to specify organizational roles, permissions, and control relations early in the early development stages of the system. In addition, DAOs face scalability challenges. While existing Model-Driven Development (MDD) tools support general smart contract and DApp design, they lack constructs tailored to the organizational and governance features unique to DAOs. To bridge this gap, we develop a code generation approach for DAO-ML, a visual modeling language for DAO design. The translator we implement for this method generates smart contracts of DAOs with suitably configured roles and permissions from visual models. The generated smart contracts particularly optimize the representation of roles and permissions to improve the system scalability and handle complex governance structures, necessary to increase the utility of DAO systems. The approach is evaluated in the context of an in vivo case study on the development of a DAO for the disintermediated management of local tourism. This work advances MDD for decentralized systems by bridging high-level governance modeling with executable, gas-efficient smart contract code generation.
Igor Konnov, Jure Kukovec, Thomas Pani, Roberto Saltini · 5 authors
We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification. Our primary tools are TLA+ for specification and the Apalache model checker for verification. Our formalization builds on the executable Python specification of 3SF. To begin, we manually translate this specification into TLA+, revealing significant combinatorial complexity in the definition of Accountable Safety. To address these challenges, we introduce several layers of manual abstraction: (1) replacing recursion with folds, (2) substituting abstract graphs with integers, and (3) decomposing chain configurations. To cross-validate our results, we develop alternative encodings in SMT (CVC5) and Alloy. Despite the inherent complexity, our results demonstrate that exhaustive verification of Accountable Safety is feasible for small instances - supporting up to 7 checkpoints and 24 validator votes. Moreover, no violations of Accountable Safety are observed, even in slightly larger configurations. Beyond these findings, our study highlights the importance of manual abstraction and domain expertise in enhancing model-checking efficiency and showcases the flexibility of TLA+ for managing intricate specifications.
The creation of blockchain-based software applications requires today considerable technical knowledge, particularly in software design and programming. This is regarded as a major barrier in adopting this technology in business and making it accessible to a wider audience. As a solution, no-code and low-code approaches have been proposed that require only little or no programming knowledge for creating full-fledged software applications. In this paper we review academic approaches from the discipline of model-driven engineering as well as industrial no-code and low-code development platforms for blockchains. We further present a case study for an integrated no-code blockchain environment for demonstrating the state-of-the-art in this area. Based on the gained insights we derive requirements for the future development of no-code and low-code approaches that are dedicated to the field of blockchains.
Piero Fraternali, Sergio Luis Herrera González, Matteo Frigerio, Mattia Righetti
Distributed Ledger Technology (DLT) is one of the most durable results of virtual currencies, which goes beyond the financial sector and impacts business applications in general. Developers can empower their solutions with DLT capabilities to attain such benefits as decentralization, transparency, non-repudiability of actions and security and immutability of data assets, to the price of integrating a distributed ledger framework into their software architecture. Model-Driven Development (MDD) is the discipline that advocates the use of abstract models and of code generation to reduce the application development and integration effort by delegating repetitive coding to an automated model-to-code transformation engine. In this paper, we explore the suitability of MDD to support the development of hybrid applications that integrate centralized database and distributed ledger architectures and describe a prototypical tool capable of generating the implementation artefacts starting from a high-level model of the application and its architecture.
Decentralized systems have been widely developed and applied to address security and privacy issues in centralized systems, especially since the advancement of distributed ledger technology. However, it is challenging to ensure their correct functioning with respect to their designs and minimize the technical risk before the delivery. Although formal methods have made significant progress over the past decades, a feasible solution based on formal methods from a development process perspective has not been well developed. In this paper, we formulate an iterative and incremental development process, named formalism-driven development (FDD), for developing provably correct decentralized systems under the guidance of formal methods. We also present a framework named Seniz, to practicalize FDD with a new modeling language and scaffolds. Furthermore, we conduct case studies to demonstrate the effectiveness of FDD in practice with the support of Seniz.
Qinghua Lu, An Binh Tran, Ingo Weber, Hugo O'Connor · 9 authors
Abstract Blockchain has attracted broad interests to build decentralised applications. A typical class of applications uses blockchain for the management of cross‐organisational business processes as well as assets. However, developing such applications without introducing vulnerabilities is hard for developers, not the least because the deployed code is immutable and can be called by anyone with access to the network. Model‐driven engineering (MDE) helps to reduce those risks, by combining proven code snippets as per the model specification, which is easier to understand than source code. Therefore, in this article, we present an approach for integrated MDE across business processes and asset management (e.g., for settlement). Our approach includes methods for fungible/non‐fungible asset registration, escrow for conditional payment, and asset swap. The proposed MDE approach is implemented in a smart contract generation tool called Lorikeet, and evaluated in terms of feasibility, functional correctness, and cost effectiveness.
The realization of large and complex cyber-physical systems (such as "smart" transportation, energy, security, and health-care systems) is creating design and verification challenges which will soon become insurmountable with the current engineering practices. These highly heterogeneous systems, tightly combining physical processes with computation, communication, and control elements, would substantially benefit from hierarchical and compositional methodologies to make their design possible let alone optimal. Several languages and tools have been proposed over the years to enable model-based development of complex systems. However, an all-encompassing design framework that helps interconnect different tools, possibly operating on different system representations, is still missing.In this dissertation, we introduce a design methodology that addresses the complexity and heterogeneity of cyber-physical systems by using assume-guarantee contracts to formalize the design process and enable the realization of system architectures and control algorithms in a hierarchical and compositional way. In our methodology, components are specified by contracts, and systems by compositions of contracts. Contracts explicitly define the assumptions of a component on its environment and the guarantees of the component under these assumptions. Contract operations and relations, such as composition, conjunction and refinement allow proving that: (i) an aggregation of components are compatible, i.e. there exists a legal environment in which they can operate; (ii) a set of specifications are consistent, i.e. there exists an implementation satisfying all of them; (iii) an aggregation of components refines a specification, i.e. it implements the specification contract and is able to operate in any environment admitted by it. While horizontal contracts are used to specify components and aggregations of components at the same level of abstraction, we introduce the notion of vertical contracts to reason about richer refinement relations and mappings between different abstraction levels, possibly described by heterogeneous architectures and behavior formalisms. Moreover, we further investigate the problem of compatibility for systems with uncontrolled inputs and controlled outputs, by establishing a link between the theory of contracts and the one of interfaces, which rely on different mathematical formalisms, while sharing the same objectives. From this link, we derive a new projection operator on contracts that enables the preservation of the semantics of interface composition and compatibility.Resting on the above contract framework, the design is carried out as a sequence of refinement steps from a high-level specification to an implementation built out of a library of components at the lower level. To allow for requirement analysis and early detection of inconsistencies, top-level system requirements are captured as contracts, by leveraging a front-end pattern-based specification language and a set of back-end formal languages, including mixed integer-linear constraints and temporal logic. Top-level contracts are then refined to achieve independent development of system architectures and control algorithms, by combining synthesis from requirements and optimization methods.To enable efficient architecture selection under safety and reliability constraints, we explore two optimization-based methods that use an approximate reliability analysis technique to overcome the exponential complexity of exact computations. The Integer-Linear Programming with Approximate Reliability (ILP-AR) method generates larger, monolithic optimization problems using approximate but efficient reliability computations with an explicit theoretical bound on the error. Conversely, the Integer-Linear Programming Modulo Reliability (ILP-MR) method breaks the complex architecture selection task into a sequence of smaller optimization tasks without reliability constraints, interleaved with exact reliability checks. By relying on efficient mechanisms to prune out candidate architectures that are inconsistent with the reliability constraints, ILP-MR can run faster than ILP-AR on large problem instances.We further explore two methods to systematically design control strategies for a given architecture. The reactive synthesis-based optimal control mapping (RS-OCM) method generates controllers by combining reactive synthesis from linear temporal logic contracts with optimization techniques based on simulation and monitoring of signal temporal logic contracts. Different design concerns are then addressed by leveraging the most appropriate abstraction levels, using contracts from the pre-characterized library to accelerate verification tasks. The programming-based optimal control mapping (P-OCM) method uses, instead, a discrete-time representation of the system and a formalization of the design requirements in terms of arithmetic constraints over real numbers to cast the control problem as an optimization problem over a finite time horizon. The optimization problem is then solved with a receding horizon approach and scales better than monolithic reactive synthesis from linear temporal logic.We demonstrate, for the first time, the effectiveness of a contract-based design flow on real-life examples of industrial relevance, namely, the design of aircraft electric power distribution and environment control systems. In our framework, optimal selection of large, industrial-scale power system architectures can be performed in a few minutes. Design validation of power system controllers based on linear temporal logic contracts shows up to two orders of magnitude improvement in terms of execution time with respect to conventional techniques. Finally, our optimization-based load management scheme allows better resource utilization than a conventional one.
A key challenge for software engineering is to learn how to reconcile the formal world of the machine and its software with the non-formal real world. In this paper, we describe Problem Oriented Software Engineering (POSE), an approach that brings both non-formal and formal aspects of software development together within a single theoretical framework for software engineering design. We show how POSE captures development as the recordable and re-playable design theoretic transformation of software problems. Their representation and transformation allows for the identification and clarification of system requirements, the understanding and structuring of the problem world, the structuring and specification of a hard-ware/software machine that can ensure satisfaction of the requirements in the problem world, and the construction of adequacy arguments, convincing both to developers and to customers, users and other interested stake-holders, that the system will provide what is needed. Designs are recordable and re-playable through our adaptation of tactics, a (now standard) form of programming language used in transformational proof theoretic presentations. This brings to our system many other benefits of such approaches, including the ability to abstract from a captured design, and to combine programmatically captured designs. This paper provides an example-driven presentation of our framework for software engineering design.