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.
Smart contracts are immutable once deployed, making security auditing crucial before deployment. Existing automated tools such as Slither are limited to pattern-matching based detection and cannot reason about the contract’s intended behaviour. Manual expert reviews help address this gap but do not scale to the volume of contracts requiring analysis. Large Language Models (LLMs) offer contextual reasoning capabilities that static analysers lack, but single-pass LLM outputs suffer from high false positive rates and unreliable vulnerability detection. This project proposes and evaluates a multi-agent LLM workflow for automated Solidity smart contract vulnerability detection. The system combines Slither static analysis with a staged reasoning pipeline comprising a context agent, a Retrieval Augmented Generation (RAG)-powered research agent, a two-round specialist debate, a judge synthesis agent, and an automated Foundry test generation and verification loop. Slither is retained to cover syntactically identifiable patterns, while the LLM agents focus on contextual and semantic reasoning that static analysis cannot capture. The workflow was evaluated against a labelled dataset of 360 Solidity contracts across twelve vulnerability categories, using a local model (DeepSeek-Coder-V2:16B) and a frontier model (Claude Sonnet 4.6) as baselines. Results show that the workflow substantially improved the local model's detection capability, nearly quintupling recall and doubling F1 over its one-shot baseline, demonstrating that structured multi-agent reasoning can partially compensate for model scale. However, precision remained low across all configurations and certain vulnerability categories remained difficult to detect. The automated test generation stage gives auditors a working starting point rather than requiring tests to be written from scratch. Overall, the results suggest that LLMs, when structured through a multi-agent workflow, show potential as a triage and scaffolding layer in the auditing process, improving coverage and reducing manual effort. However, they are still insufficient to entirely replace expert review.
d IoT security perspective. It makes use of three essential Blockchain features— transparency, immutability, and decentralization— to build environment that are reliable and impenetrable. This application is realized through the utilization of features such as AI-driven fraud detection, Blockchain security, data privacy, the reliability of Smart Contracts, transaction speed, and system scalability. The result is, Blockchain-IoT Security Perspective, the first rank is System Scalability, the lowest rank is AI-based Fraud Detection, Blockchain Security is the fourth rank, Data Privacy is the fifth rank, Smart Contract Reliability is the third rank, and Transaction Speed is the first rank.
In the process of building materials supply chain management, there are problems such as information opacity, low logistics coordination efficiency, difficulty in material quality traceability, and weak trust mechanism among supply chain entities, which lead to rising costs, low efficiency, and waste of resources. In addition, the construction industry has a large amount of carbon emissions, and the impact of supply chain management on carbon emission reduction cannot be ignored. To this end, this paper introduces blockchain technology to improve supply chain transparency, optimize logistics management, enhance material quality traceability, and explore its role in carbon emission reduction. This paper constructs a blockchain-based building materials supply chain management system, using distributed ledgers to ensure data transparency, smart contracts to automate procurement, acceptance and payment, which is a material traceability system to ensure quality control, the Internet of Things combined with blockchain to optimize logistics management, and establish a carbon emission monitoring and optimization mechanism to achieve real-time data recording and low-carbon scheduling. The system built in this study shows significant advantages in multiple key indicators. The overall carbon emissions of the supply chain in the experimental group are 88 tons of CO2, a 12% decrease compared to 100 tons of CO2 in the control group. The average transportation time in the experimental group is 4.5 hours, while that in the control group is 8.2 hours, a 45.1% decrease. The application of blockchain technology has effectively improved the efficiency and transparency of building materials supply chain management, optimized logistics and material quality control, and played a positive role in carbon emission reduction.
This paper analyzes the shortcomings of traditional authentication mechanisms in web applications operating over the secure TLS 1.3 protocol. It is established that even with an encrypted channel, the transmission of secret data (passwords, tokens) remains a primary attack vector. An improved protocol is proposed that integrates an authentication mechanism based on zero-knowledge proofs (zk-SNARK) immediately after session establishment via Elliptic Curve Diffie-Hellman (ECDHE) key exchange. This approach completely eliminates the transmission of client credentials, significantly increasing resistance to phishing and server database compromises.
1 Use of Smart Contracts in Copyright Law Abstract This Master's thesis examines smart contract technology and its potential application within specific institutes of Czech copyright law. The primary objective of the research is to evaluate whether blockchain-based smart contracts can be effectively utilised in the fields of collective rights management and related licensing agreements, while respecting the existing Czech legal framework. The study focuses on the potential for streamlining and accelerating economic transactions in a digital environment where copyright protection faces novel challenges, including the rise of generative artificial intelligence. The thesis is structured into four chapters, which sequentially analyse the technical nature of smart contracts, their practical application within collective management and licensing agreements, and finally, the legal and technical obstacles hindering more extensive practical implementation. The analysis demonstrates that the greatest potential for smart contracts lies in their integration into the processes of existing collective management organisations (CMOs), specifically OSA, particularly regarding rights under the voluntary collective management regime. This technology could significantly support independent musical artists by increasing the...
In the digital age, Bitcoin remains the first and most notable cryptocurrency. Over the years, its value has increased, making it a desirable digital asset with millions of enthusiasts who trade and invest daily. Bitcoin is highly volatile in comparison with traditional assets and in absolute terms. Understanding its volatility history helps investors decide whether to buy, sell, or hold. A mathematical model that accounts for volatility is essential for these decisions. Unfortunately, Bitcoin’s vast profit potential for investors comes with the dilemma of its negative impact on global environmental health, which needs serious attention. This study aims to model Bitcoin’s return volatility that can support investment decisions and, on the other hand, the negative impact of Bitcoin mining and outline the actions necessary to mitigate it.
Taras Maksymyuk, Francesco Meloni, Matias Torres Diaz, Domenico Romano · 6 authors
This paper presents a blockchain-centered system architecture for cultural heritage provenance that replaces fragmented, paper-based tracking with a tamper-evident, auditable digital workflow. We assume that each object can be reliably bound to a stable physical fingerprint through an established scan-based pipeline, and we focus on how that fingerprint is represented, stored, and verified within a practical distributed ledger design. The proposed framework separates high-assurance settlement events, such as registration and ownership transfer, from high-volume operational records, such as condition updates and monitoring logs, by routing data across multiple layers and committing verifiable summaries of frequent activity to a high-security anchor chain. We also describe a deployable decentralized application stack that integrates standard token interfaces for asset representation, event-driven synchronization for user-facing services, and scalable node access to reduce read latency without requiring institutions to maintain their own node infrastructure. The result is a concrete system model that clarifies how the end-to-end provenance trail remains verifiable under realistic performance constraints.
Blockchain-based decentralized identity (DID) technology provides a more secure and efficient paradigm for identity verification. However, along with the promotion of applications, data storage of DID has gradually become one of the restrictions for the implementation due to the dramatically increasing size of the distributed ledger, and the issue becomes more complicated when considering the diversity of practical conditions and interoperability. In this article, we propose a scalable on-chain-off-chain storage for decentralized identity (SCOOP) scheme to minimize the total storage cost of blockchain-based DID while guaranteeing the efficiency of the implementation. The proposed scheme consists of a two-phase decision-making process, and a method that integrates the on-chain storage with off-chain storage in a scalable manner, so that an optimal storage task scheduling can be generated. In addition, to reduce on-chain storage overhead, we propose a multilinear tree-based commitment scheme that supports sublinear proof aggregation and updates. Our experiment evaluations have demonstrated that the proposed scheme can successfully achieve a superior performance in storage saving for DID while considering the time constraint.
In the domain of agricultural product traceability, while traditional blockchain technologies ensure data immutability, they struggle to verify the authenticity of digital twins generated by generative artificial intelligence (GAI), resulting in a se mantic gap between the physical world and its virtual representation. To address these challenges, this paper proposes Verifiable Twin model driven by Cross-Modal Alignment (VTA-CMAD), which targets three core issues: cross-modal consistency verification between blockchain-stored data and AIGC-generated twins, lightweight zero-knowledge proof framework construction, and incentive-compatible suppression of malicious behaviors. The innovation of this article is reflected in three aspects. Firstly, this article proposes a 3D multimodal alignment algorithm that integrates dynamic time warping. B y integrating physical sensing temporal data, production process images, and cultural semantic descriptions, the optimal transmission mapping of feature space is established. Secondly, design a verifiable circuit zk Vector to transform the inference process of the fine-tuning diffusion model into zero knowledge proof constraints, generating proof files with a size less than 1.2KB. Finally, a dynamic consensus mechanism Proof of Trustworthiness based on Feature Alignment (PoTV) based on feature alignment is constructed to achieve adaptive adjustment of data weights. Experimental results demonstrate that the proposed approach achieves a tamper detection rate of 86.2%, a Gini coefficient of 0.19 for incentive fairness, and reduces multimodal alignment error to 0.11 ± 0.03.
This article argues that the extraction of value through informational asymmetry, what the article formalizes as the Blaeu rent, is categorically distinct from Ricardian scarcity rents and Schumpeterian innovation rents: it scales with the counterparty’s blindness, is invariant to productive merit, and is dissolved entirely by symmetric closure. The argument proceeds in three interlocking registers. The first is philosophical: drawing on Maurice Merleau-Ponty’s account of motor intentionality, Martin Heidegger’s analysis of the ready-to-hand, and Antonio Damasio’s somatic-marker hypothesis, the article defends the existential claim that some intentional states carry content before they are verbalized, and that pre-articulate knowledge, alongside acquired, derived, received, and inherited knowledge, constitutes a legitimate and analytically distinct mode of knowledge entry. The second is formal: the article introduces a fiber bundle topology to represent semantically overloaded concepts without metric distortion; formalizes the Blaeu rent as a function of the information set differential between counterparties, subject to strict conditions of merit-invariance; presents a mechanism-design proof, grounded in adverse selection dynamics, demonstrating that institutional adoption of symmetric instruments is the dominant rational strategy for capital; and formalizes the irreversible loss of cognitive potential under asymmetric conditions as a cognitive entropy law, drawing on Nicholas Georgescu-Roegen’s thermodynamic framework, showing that the waste is path-dependent and permanent. The third is architectural: the article specifies the federated, homomorphically encrypted governance structure required to make the sovereignty claim real rather than nominal, and addresses the warrant-adjudication problem through cryptographically verifiable zero-knowledge credential systems. The central finding is that symmetric closure of the information gap dissolves the Blaeu rent entirely while leaving earned competitive advantage, including first-mover position, execution capacity, and risk tolerance, wholly intact.