Shaoyu Li, Hexuan Yu, Md Mohaimin Al Barat, Yang Xiao · 6 authors
With the rise of decentralized finance, fiat-to-cryptocurrency exchange platforms have become popular entry points into the cryptocurrency ecosystem. However, these platforms frequently fail to ensure adequate privacy protection, as evidenced by real-world breaches that exposed personally identifiable information (PII) and crypto addresses. Such leaks enable adversaries to link real-world identities to cryptocurrency transactions, undermining the presumed anonymity of cryptocurrency use. We propose FC-GUARD, a privacy-preserving exchange system designed to preserve user anonymity without compromising regulatory compliance in the exchange of fiat currency for cryptocurrencies. Leveraging verifiable credentials and zero-knowledge proof techniques, FC-GUARD enables fiat-to-cryptocurrency exchanges without revealing users' PII or fiat account details. This breaks the linkage between users' real-world identities and their cryptocurrency addresses, thereby upholding anonymity, a fundamental expectation in the cryptocurrency ecosystem. In addition, FC-GUARD complies with key regulations over cryptocurrency usage, such as know-your-customer requirements and auditability for tax reporting obligations by integrating a lawful de-anonymization mechanism that allows the auditing authority to identify misbehaving users. This ensures regulatory compliance while defaulting to privacy protection. We implement our system on both desktop and mobile platforms, and our evaluation shows its feasibility for practical deployment.
This technical disclosure describes integration patterns for comprehensive smart contract defence systems. The disclosed architecture includes a behavioural suspicion scoring framework, modular security architecture using the Diamond Standard (EIP-2535), graduated response mechanisms, and cross-contract coordination protocols. The system enables layered defence strategies that adapt to threat levels and coordinate responses across multiple contracts. This document is published as a defensive publication to establish prior art and prevent third parties from obtaining patent protection for similar approaches.
Niomi Langaliya, Vinay Thakor, Purna Tanna, Disha Shah
This research preprint presents Aegis, a zero-knowledge-proof-based security paradigm designed to mitigate validator-compromise attacks in cross-chain bridges. The work empirically evaluates a ZKP-based withdrawal verification mechanism against an optimized multi-signature validator model under controlled conditions, demonstrating complete resistance to unauthorized fund transfers at the cost of increased Layer 1 gas consumption. The study introduces the concept of the cost of trustlessness as an empirically derived techno-economic metric and provides quantitative justification for migrating cryptographic verification to Layer 2 environments. This work was previously presented at FINCON’25, National Forensic Sciences University (NFSU), Gandhinagar, India. This version is released as a non-peer-reviewed research preprint for open dissemination and citation. Journal submission is in progress.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
The modern integrated circuit ecosystem is increasingly reliant on third-party intellectual property integration, which introduces security risks, including hardware Trojans and security vulnerabilities. Addressing the resulting trust deadlock between IP vendors and system integrators without exposing proprietary designs requires novel privacy-preserving verification techniques. However, existing privacy-preserving hardware verification methods are all simulation-based and fail to offer formal guarantees. In this paper, we propose ZK-CEC, the first privacy-preserving framework for hardware formal verification. By combining formal verification and zero-knowledge proof (ZKP), ZK-CEC establishes a foundation for formally verifying IP correctness and security without compromising the confidentiality of the designs. We observe that existing zero-knowledge protocols for formal verification are designed to prove statements of public formulas. However, in a privacy-preserving verification context where the formula is secret, these protocols cannot prevent a malicious prover from forging the formula, thereby compromising the soundness of the verification. To address these gaps, we first propose a blueprint for proving the unsatisfiability of a secret design against a public constraint, which is widely applicable to proving properties in software, hardware, and cyber-physical systems. Based on the proposed blueprint, we construct ZK-CEC, which enables a prover to convince the verifier that a secret IP's functionality aligns perfectly with the public specification in zero knowledge, revealing only the length and width of the proof. We implement ZK-CEC and evaluate its performance across various circuits, including arithmetic units and cryptographic components. Experimental results show that ZK-CEC successfully verifies practical designs, such as the AES S-Box, within practical time limits.
Open access
4 source records
cs.CR
cs.LO
Physical Unclonable Functions (PUFs) and Hardware Security
IoT data demands are growing, with Distributed Ledger Technologies (DLTs) offering secure data management, provided they can meet scaling and efficiency requirements that are more restrictive than in conventional application environments. This article comprehensively surveys 27 DLTs of varying paradigms and implementation methods, proposes a scoring method for determining DLT-IoT integration suitability, and then applies that method to the surveyed DLTs. Six DLTs were shortlisted as the most promising, which were then subjected to in-depth analysis around three IoT use cases: health-IoT, e-commerce and automotive manufacturing. We discuss the viability of lightweight DLTs and identify crucial future research directions.
V. T. Krishnaprasath, T. Surya, B. Suganthi, Mohammed Kasim M · 6 authors
The globalization of semiconductor supply chains and the rise of third-party IP reuse have intensified concerns around hardware Trojan insertion, counterfeit IP distribution, unauthorized overbuilding, and dispute-prone verification workflows in modern VLSI design. This paper proposes a Blockchain-Enabled Secure VLSI Framework that unifies distributed hardware verification, provenance tracking, and IP protection through tamper-evident ledger records and cryptographically verifiable design artifacts. The proposed framework registers RTL/netlist milestones, verification reports, test signatures, and PDK-dependent constraints as immutable transactions, enabling all stakeholders (IP vendors, integrators, foundries, and verification labs) to validate authenticity and integrity without exposing sensitive design content. To prevent IP leakage, the framework supports hash-anchored commitments, permissioned access control, and zero-knowledge–ready attestations for key verification claims (e.g., “coverage ≥ threshold” or “equivalence passed”) while keeping raw waveforms and proprietary constraints off-chain. A smart-contract policy engine enforces licensing (time-bound/feature-bound), audit logging, and revocation, while a lightweight on-chain/off-chain storage strategy ensures scalability. Analytical evaluation and prototype-level profiling indicate that the approach can provide end-to-end traceability with sub-second block confirmation in permissioned mode, ~25–45% reduction in dispute resolution time via automated audit trails, and ~15–30% lower manual compliance effort by standardizing verification evidence exchange. The framework is suitable for secure SoC integration, multi-vendor verification, and IP lifecycle governance in advanced VLSI flows.
Open access
Physical Unclonable Functions (PUFs) and Hardware Security
Defensive publication establishing prior art for proof-first digital identity systems using prime-indexed state evolution, zero-knowledge proofs, and silence-by-default semantics. This specification defines the Meta-Theorem of Prime Identity (MTPI), an architectural framework requiring cryptographic proof for every state transition. Core components include: Prime-Indexed Recursive Tensor Mathematics (PIRTM) with contractive dynamics guarantee; prime-gated activation with drift bounds δ(t) ≤ 0.3; Conscious Sovereignty Layer (CSL) with ethical tensor field commutation relations; Archivum append-only audit schema; and conformance requirements including Surveillance Fork detection. Reference implementations provided in Solidity and Circom 2.1. Mathematical foundations, alternative embodiments, and public domain designations included for maximum prior art scope. Keywords: zero-knowledge proofs, prime-indexed identity, verifiable computation, AI safety, defensive publication, proof-first computing, MTPI, PIRTM, CSL
Open access
2 source records
Cryptography and Data Security
Physical Unclonable Functions (PUFs) and Hardware Security
Many Ethereum smart contracts rely on block attributes such as block.timestamp or blockhash to generate random numbers for applications like lotteries and games. However, these values are predictable and miner-manipulable, creating the Bad Randomness vulnerability (SWC-120) that has led to real-world exploits. Current detection tools identify only simple patterns and fail to verify whether protective modifiers actually guard vulnerable code. A major obstacle to improving these tools is the lack of large, accurately labeled datasets. This paper presents a benchmark dataset of 1,752 Ethereum smart contracts with validated Bad Randomness vulnerabilities. We developed a five-phase methodology comprising keyword filtering, pattern matching with 58 regular expressions, risk classification, function-level validation, and context analysis. The function-level validation revealed that 49% of contracts initially classified as protected were actually exploitable because modifiers were applied to different functions than those containing vulnerabilities. We classify contracts into four risk levels based on exploitability: HIGH_RISK (no protection), MEDIUM_RISK (miner-exploitable only), LOW_RISK (owner-exploitable only), and SAFE (using Chainlink VRF or commit-reveal). Our dataset is 51 times larger than RNVulDet and the first to provide function-level validation and risk stratification. Evaluation of Slither and Mythril revealed significant detection gaps, as both tools identified none of the vulnerable contracts in our sample, indicating limitations in handling complex randomness patterns. The dataset and validation scripts are publicly available to support future research in smart contract security.
We present Y.I.N.-AGENT-ACT, a privacy-preserving architecture for autonomous AI agent action chains that mathematically guarantees zero intent drift while maintaining cryptographic compliance across multi-step workflows. The core innovation is the mandatory DP→ZK→HE ordering (Differential Privacy → Zero-Knowledge Proof → Homomorphic Encryption) applied to every step in autonomous agent execution, combined with 136-byte Action Chain Compliance Tokens providing cryptographic chain integrity through HMAC-SHA256 chaining. Key results (measured on 48-step test corpus including 15 adversarial scenarios): (1) 100% drift prevention—all 15 drift scenarios caught with zero false negatives; (2) F1-score 0.882 at threshold 0.5 (precision 0.789, recall 1.000); (3) ~85ms per-step overhead with O(N) verification complexity; (4) 136-byte token size verified to match patent specification exactly; (5) native EU AI Act Article 50 compliance via verifiable privacy proofs. Y.I.N.-AGENT-ACT addresses the emerging agent autonomy crisis where AI systems like OpenAI Operator and Anthropic Computer Use execute multi-step tasks without cryptographic guarantees. The Intent Drift Elimination Theorem establishes that undetected drift probability is bounded by δ+(1−threshold), achieving zero false negatives across all measured adversarial scenarios including phishing, data exfiltration, and privilege escalation attacks. Protected by US Pending Patent 63/956,723 (106 claims). The agentic AI market is projected to reach $93.2 billion by 2032, but deployment remains at 2% of enterprises due to governance bottlenecks. Y.I.N.-AGENT-ACT eliminates the 6-18 month compliance barrier through cryptographic compliance-by-design.
Xinyu Hou, Yang Lu, Rabimba Karanjai, Lei Xu · 5 authors
Ransomware is still one of the most serious cybersecurity threats. Victims often pay but fail to regain access to their data, while also facing the danger of losing data privacy. These uncertainties heavily shape the attacker-victim dynamics in decision-making. In this paper, we introduce and analyze zkRansomware. This new ransomware model integrates zero-knowledge proofs to enable verifiable data recovery and uses smart contracts to enforce multi-round payments while mitigating the risk of data disclosure and privacy loss. We show that zkRansomware is technically feasible using existing cryptographic and blockchain tools and, perhaps counterintuitively, can align incentives between the attacker and the victim. Finally, we develop a theoretical decision-making framework for zkRansomware that distinguishes it from known ransomware decision models and discusses its implications for ransomware risk analysis and response decision support.
Firmware integrity is a foundational requirement for securing Cyber-Physical Systems (CPS), where malicious or compromised firmware can result in persistent backdoors, unauthorized control, or catastrophic system failures. Traditional verification mechanisms such as secure boot, digital signatures, and centralized hash databases are increasingly inadequate due to risks from insider threats and single points of failure. In this paper, we propose a decentralized firmware integrity verification framework built on the Ethereum blockchain, offering tamper-proof, transparent, and trustless validation. Our system stores SHA-256 hashes of firmware binaries within smart contracts deployed on the Ethereum Sepolia testnet, using Web3 and Infura for seamless on-chain interaction. A Python-based client tool computes firmware hashes and communicates with the blockchain to register and verify firmware authenticity in real-time. We implement and evaluate a fully functional prototype using real firmware samples, demonstrating successful contract deployment, hash registration, and integrity verification through live blockchain transactions. Experimental results confirm the reliability and low cost (in gas fees) of our approach, highlighting its practicality and scalability for real-world CPS applications. To enhance scalability and performance, we discuss extensions using Layer-2 rollups and off-chain storage via the InterPlanetary File System (IPFS). We also outline integration pathways with secure boot mechanisms, Trusted Platform Module (TPM)-based attestation, and zero-trust architectures. This work contributes a practical and extensible model for blockchain-based firmware verification, significantly strengthening the defense against firmware tampering and supply chain attacks in critical CPS environments.
This preprint introduces Risk Oracle, an exploit-intelligence–driven SBOM attestation framework designed to support practical risk gating in CI/CD. The system combines signals from Known Exploited Vulnerabilities (KEV) and Exploit Prediction Scoring System (EPSS) with SBOM-to-vulnerability matching to produce a policy-backed gate decision (e.g., pass / warn / block) while keeping the workflow interpretable and reproducible. A core design goal is bounded disclosure: the producer can commit to full findings and then disclose only a limited subset (e.g., top-K highest-risk issues) suitable for downstream verification, reducing disclosure risk while preserving auditability. The paper details the end-to-end pipeline (producer/verifier roles), a typed attestation schema, a scoring and decision procedure, and an evaluation that studies (i) signal behavior under pinned KEV/EPSS snapshots and (ii) operational overhead under synthetic SBOM scaling intended to approximate CI workloads. Key contributions A practical SBOM attestation pipeline that integrates exploit-intelligence signals for operational decision-making in CI/CD. A typed attestation schema and verifier procedure supporting bounded disclosure. A policy-driven scoring and gating framework (pass/warn/block) grounded in vulnerability-management practice. Evaluation focused on interpretability and operational cost (runtime/payload scaling) under reproducible, pinned snapshots. Artifacts / Reproducibility Code, scripts, and pinned snapshot references: [GitHub link] Suggested citationSudhir, S. (2026). Risk Oracle: Exploit-Intelligence–Driven SBOM Attestations with Bounded Disclosure (preprint). Zenodo. DOI: [10.5281/zenodo.18153487] Keywords: SBOM, software supply chain security, vulnerability management, KEV, EPSS, OSV, attestation, CI/CD, bounded disclosure, reproducibility
The rigorous security model of Bitcoin's UTXO architecture often comes at the cost of developer usability, forcing a reliance on manual stack manipulation that leads to critical financial vulnerabilities like signature malleability, unspendable states and unconstrained execution paths. Industry standards such as Miniscript provide necessary abstractions for policy verification but do not model the full imperative logic required for complex contracts, leaving gaps in state management and resource liveness. This paper introduces Bithoven, a high-level language designed to bridge the gap between expressiveness and formal safety. By integrating a strict type checker and a resource liveness analyzer with a semantic control-flow analyzer, Bithoven eliminates major categories of consensus and logic defects defined in our fault model prior to deployment. Our results indicate that this safety comes at modest cost: Bithoven compiles to Bitcoin Script with efficiency comparable to hand-optimized code, demonstrating that type-safe, developer-friendly abstractions are viable even within the strict byte-size constraints of the Bitcoin blockchain.
Kamil Ježek, Seongho Jeong, Yeonsoo Kim, Bernhard Scholz · 5 authors
Ethereum’s smart contracts operate on directly addressable storage that is represented as tries. The performance of the Ethereum Virtual Machine (EVM) suffers from slow storage access due to trie encoding, which hampers transaction throughput and scalability. To mitigate the Ethereum storage performance bottleneck, we propose a new storage representation for the EVM that supports asynchronous trie construction. Without changing the Ethereum protocol, we add a flat representation called Storage Replica to improve performance. Storage Replica provides a fast lookup of values in the program’s main thread, while a worker thread prepares the tries for subsequent cryptographic calculations. With a storage overhead of less than 5% (i.e., 10 GB), we achieve up to a 6× speedup in processing smart contracts and a 4× speedup in block commits for the initial 9 M blocks of the Ethereum blockchain.
Smart contracts deployed on the Ethereum blockchain execute on the Ethereum Virtual Machine (EVM) and handle financial operations such as payments, asset transfers, and auctions. Given the high value they control, correctness in these contracts is critical, as errors and vulnerabilities have led to losses totalling hundreds of millions of dollars. To address this problem, we develop a novel formalization of the EVM. Compared to existing formalizations, our formalization is in Isabelle/HOL, covers all current EVM opcodes, and formalizes cross-contract execution. Thus, it allows us to express properties which are out of scope for other formalizations. To allow for the execution of our formalization, we implement a code generator, allowing it to be exported as a stand-alone Haskell program. We then validate the semantics by executing νmprint{25000} test cases from the official Ethereum test suite. Our formalization can be used to verify concrete smart contracts but also to reason about the correctness of tools and techniques which manipulate bytecode, such as compilers or optimizers.
K501 is a deterministic temporal-structural integration framework designed to provide append-only state anchoring, canonical serialization, and hash-bound integrity across heterogeneous systems. The framework does not replace existing infrastructures such as databases, version control systems, or distributed ledgers. Instead, it operates as an optional structural overlay layer that encapsulates states in a formally defined frame model with explicit time anchoring (UTC + Unix Epoch). K501 focuses on: Deterministic canonical serialization Append-only historical discipline Explicit temporal positioning Snapshot-based integrity Cross-system structural interoperability The specification defines minimal compliance requirements for structural integration without modifying internal operational semantics of integrated systems. K501 is intended as a neutral structural discipline for temporal knowledge stabilization and reproducible state documentation. Peace 🕊️ Frames stehen nicht isoliert! Das ist eine formal belastbare Beschreibung. Keine Überhöhung.Kein AGI.Keine Spekulation.Aber diese hier ist solide. 🕊️
K501 is a deterministic temporal-structural integration framework designed to provide append-only state anchoring, canonical serialization, and hash-bound integrity across heterogeneous systems. The framework does not replace existing infrastructures such as databases, version control systems, or distributed ledgers. Instead, it operates as an optional structural overlay layer that encapsulates states in a formally defined frame model with explicit time anchoring (UTC + Unix Epoch). K501 focuses on: Deterministic canonical serialization Append-only historical discipline Explicit temporal positioning Snapshot-based integrity Cross-system structural interoperability The specification defines minimal compliance requirements for structural integration without modifying internal operational semantics of integrated systems. K501 is intended as a neutral structural discipline for temporal knowledge stabilization and reproducible state documentation. Peace 🕊️ Frames stehen nicht isoliert! Das ist eine formal belastbare Beschreibung. Keine Überhöhung.Kein AGI.Keine Spekulation.Aber diese hier ist solide. 🕊️
Yinhao Xiao, Chih-Chung Liu, Mingshu Cong, Le Yang
DeFi smart-contract vulnerabilities often arise from protocol-level financial semantics rather than syntactic Solidity patterns. Direct LLM prompting can generate plausible patches that compile but leave oracle, vault, lending, or AMM invariants unresolved. We aim to make LLM-based smart-contract repair more reliable by separating patch generation from domain-specific judgment and requiring accepted patches to improve check-visible semantic obligations. We present DeFiSent, a check-guided repair framework. It normalizes contract code, infers protocol roles, routes vulnerability-family checks, emits structured findings and violated invariants, and prompts an LLM with this evidence. Candidate patches are accepted only after compilation, tests, interface preservation, non-increasing semantic severity, and invariant-specific gates. We evaluate DeFiSent on a coverage-aware corpus from DeFiHackLabs, EVMbench, LISA-Bench, SmartBugs Curated, and BCCC-SCsVuls-2024. The DeepSeek campaign contains 40,452 paired tasks and 80,904 model-mode runs, including a 41,332-row code-level shard. On the unified 6,000-task DeepSeek subset, check guidance improves dynamic pass rate from 54.82\% to 79.95\%, semantic-improvement rate from 40.42\% to 53.92\%, and total severity reduction from 8,733 to 24,084. On a 2,000-task SiliconFlow matrix, aggregate semantic-improvement rate increases from 27.0\% to 57.8\%. Structured findings and gate-based validation substantially improve LLM repair behavior for DeFi contracts. DeFiSent does not replace expert auditing, but it provides a reproducible path for aligning LLM-generated patches with financial-semantic proof obligations.
Smart contracts are self-executing programs deployed on blockchain networks, automating trust-based operations in decentralized applications (DApps). At the same time, their transparency and immutability offer significant advantages; these characteristics make them vulnerable to security flaws that, once deployed, cannot be rectified without substantial consequences. Existing verification tools such as Mythril, Slither, Oyente, and Zeus primarily target Solidity contracts using static or symbolic analysis. However, they fall short in supporting diverse blockchain languages like Rust (used in Solana), Michelson (Tezos), and Move (Aptos/Sui). Additionally, these tools lack formal specification using temporal logic, provide limited scalability for large and complex contracts, and often yield high false favorable rates. This paper presents an enhanced SmartScan framework for formally verifying smart contracts across multiple blockchain ecosystems to address these gaps. The framework introduces language-specific parsers and FSM/BIP model generation pipelines for Solidity, Vyper, Rust, Michelson, and Move. These models are translated into SMV format for symbolic model checking using nuXmv. The proposed algorithms incorporate CTL-based specifications to verify key properties such as fund safety, reentrancy prevention, access control compliance, and arithmetic safety. Scalability is achieved through symbolic abstraction, partial-order reduction, and multi-threaded execution, with optional support for distributed verification using cloud platforms. Experimental evaluation on diverse real-world contracts demonstrated a verification accuracy of over 94%, a 40–50% reduction in FSM states after optimization, and speedups of up to 3.2× with parallel execution. The case study on a cross-chain DeFi contract confirmed consistent vulnerability detection across all supported languages. The proposed framework offers a scalable, secure, and language-agnostic solution for trustworthy, intelligent contract verification.
Reentrancy remains one of the most persistent and damaging vulnerabilities in Ethereum smart contracts, enabling adversaries to recursively drain funds despite the presence of static and runtime defenses. Existing studies mainly focus on detection or program analysis, but they do not explain why and under what conditions attackers decide to exploit. In this work, we introduce a decision-theoretic framework that models reentrancy as a profit-maximizing problem under gas, risk, and atomicity constraints. Our framework derives the conditions under which reentrancy attacks are economically viable and provides an algorithm for computing optimal exploit strategies. We further extend the analysis to multi-contract attacks, capturing sequential, parallel, and optimized execution strategies. A simulation environment evaluates profitability across varying balances and gas configurations, highlighting thresholds where attacks become infeasible. Finally, we translate attacker decision profiles into practical defense recommendations for developers, auditors, and DeFi system designers. This framework bridges the gap between exploit detection and adversarial economics, offering a rigorous basis for strengthening smart contract security. This framework establishes a theoretical baseline for adversarial economics in smart contract security, forming a foundation for future MEV-aware exploitability models and Layer-2 risk analysis.
Traditional digital trust architectures suffer from the “Library Problem”: dependency on pre-compiled, static lookup tables or binaries that must be trusted blindly, creating supply-chain vulnerabilities. This paper proposes a paradigm shift to Intrinsic Trust, where encoding infrastructure is mathematically regenerated at runtime rather than distributed. We introduce the 0MXI Calculus, a deterministic lattice system anchored on universal transcendental constants:the golden ratio Φ ≈ 1.618033988749895 and π ≈ 3.141592653589793, with a contraction ratio λ ≈ 0.339949771344778. Operations on a quantized F15 lattice ensure cross-platform determinism, bounded by a Prime Boundary Horizon (N = 23) that guarantees injective reversibility (Theorems 1 and 2).This framework underpins TreeOS, an operating system that bootstraps from a “Math Root-of-Trust” via autogenesis, regenerating a bijective Tick Table for byte encoding without stored dependencies. TreeBABEL, the verifiable data transport protocol, packages data as JSON artifacts with mathematical manifests for independent receiver validation. Extending this, the VMEM Node Architecture transforms online repositories into externalized memory banks, enabling AI models to scrape and derive OS state on demand, eliminating internal weight bloat and static knowledge cutoffs.We demonstrate adaptability to constrained ledgers (e.g., 280-character limits) for efficient chunking. Through rigorous proofs and a Python reference implementation, we show that trust can be calculated, not stored, decoupling systems from physical hardware and fostering entropy-neutral, zero-trust computation.
The smart contracts facilitated by blockchains allow the decentralized and automated implementation of digital contracts, yet the current security measures in this space are mostly geared towards vulnerability detection and post-implementation functionality, which do not provide much defence against runtime attacks. The paper analyses the concept of smart contracts as a unified approach to cybersecurity, and provides a Hardened Smart Contract Model (HSCM) as a proactive and runtime security quotient model. The suggested model places policy-conscious logic, formal safety requirements, risk aversive execution, upgradability under control by governance, and unchangeable auditability directly in the design of contracts. The framework guarantees the elimination of unauthorized access, re-entrancy and logic abuse by providing runtime verification and automated response measures that avert such violations even before state transitions take place. A fair amount of experimental confirmation on an Ethereum-compatible system proves that there is a high security guarantee with tolerable load overhead, the deployed smart contracts could be hardened.
Abstract Program verification provides stronger guarantees of correctness than standard testing. The verification process takes a program as input and derives a mathematical formula. Proving that a program is correct then reduces to establishing that this derived formula is unsatisfiable. Traditionally, automated reasoning tools can be used to determine unsatisfiability automatically. Furthermore, modern solvers can also produce a proof of unsatisfiability. However, these techniques typically rely on the proof and the underlying code being publicly available, which may not be desirable for certain applications. This work shows how to address this problem. Our team initially developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. Building on these initial results, we devised ZKSMT, a virtual machine for validating unsatisfiability results produced by SMT solvers in zero-knowledge settings. In this paper we describe the theoretical foundations of such virtual machines and demonstrate how they can be applied to the theories of uninterpreted functions and linear integer arithmetic, two of the most widely used theories in verification. We conclude by outlining how the full formal verification workflow can be adapted to operate in privacy-preserving settings.
Leanne Ngo, Tran Tien Nhat, anon anon, Triet Huynh Minh Le · 7 authors
Smart contracts underpin modern blockchain ecosystems, enabling decentralized applications in DeFi and digital asset management. However, their immutability exacerbates programming errors and vulnerabilities, leading to unpatchable flaws and significant financial losses, as seen in high-profile exploits. Current vulnerability detection methods including static and dynamic analysis—face critical limitations: (1) static analysis suffers from state-space explosion, control-flow complexity, over-approximation, and high false positives; (2) dynamic fuzzing relies on syntactic/random mutations lacking semantic awareness, inefficiently exploring deep state-dependent paths and complex transaction sequences; (3) both static and dynamic approaches overlook semantic-structural gaps, such as execution order semantics in reentrancy vulnerabilities; (4) fuzzing reports lack explainability, hindering practical auditing. To address these challenges, we propose MAESFuzz1, a multi-agent semantic-guided smart contract fuzzing framework that integrates static structural analysis, dynamic execution feedback, and Large Language Model (LLM)–assisted reasoning within a closed-loop architecture. MAESFuzz employs LLMs as semantic advisors to guide seed generation, transaction sequence construction, and mutation refinement, enabling effective exploration of deep state-dependent behaviors and complex multi-transaction vulnerabilities. Extensive evaluation on the SoliAudit benchmark and a real-world dataset of deployed Ethereum contracts shows that MAESFuzz improves vulnerability detection by up to 28.7% relative to state-of-the-art (SOTA) smart contract fuzzers on SoliAudit. On real-world contracts, MAESFuzz uncovers 25 more expert-validated vulnerabilities than the strongest SOTA baseline while maintaining 94.38% precision and competitive execution coverage. In addition, MAESFuzz generates structured, execution-grounded audit reports to enhance interpretability and support practical security auditing.