Decentralized finance failures frequently arise not from a single obviously unsafe function, but from valid operations composed into an invalid state transition. Static analyzers and vulnerability checklists remain valuable, yet they often stop before answering the question that determines real risk: can an adversary control the preconditions, sequence, capital, ordering, and external dependencies required to turn a defect into impact? This working paper presents the Invariant-to-Exploit (I2E) framework, a practitioner-oriented method for connecting architecture assumptions to executable invariants, stateful counterexamples, exploitability evidence, and remediation regression tests. I2E consists of six linked activities: system scoping, invariant-ledger construction, adversarial controllability analysis, stateful sequence generation, exploitability tracing, and fix validation. The framework is applied retrospectively to three publicly documented incidents: KyberSwap Elastic, Euler, and the Curve sDOLA LlamaLend market. These analyses do not claim prospective vulnerability discovery; instead, they demonstrate the test signals that reviewers can derive from public root-cause information. The principal contribution is a reproducible audit worksheet that preserves the chain from protocol assumption to broken property, realistic exploitability, observable impact, and regression-tested remediation. The method is designed to remain usable by independent security researchers who cannot publish confidential client evidence. A benchmark design is proposed for future controlled comparison against checklist-only security review.
Web security has become a critical domain as modern applications increasingly rely on dynamic user-generated content, making them highly vulnerable to Cross-Site Scripting (XSS) attacks. Traditional detection systems struggle to cope with evolving payload patterns, limited generalisation across institutions, and strict privacy restrictions that prevent sharing of sensitive request logs. To address these challenges, this work proposes a Zero-Knowledge Federated Sequence Learning (ZK-FSL) framework that enables collaborative XSS detection without exposing raw data or intermediate gradients. The model integrates attention-based deep sequence learning with zero-knowledge proof validation, ensuring both strong predictive capability and verifiable trust among participating clients. Experimental evaluation demonstrates that ZK-FSL achieves superior performance compared to centralised and federated baselines, reaching 96.3% accuracy , 96.7% precision , 95.9% recall , 96.3% F1-score , and an AUC of 0.98 . These results confirm that the proposed framework effectively enhances privacy-preserving threat detection while maintaining high robustness against diverse and sophisticated XSS attack patterns.
Ethereum, one of the largest blockchain platforms, manages millions of dollars in digital assets daily and depends on consistent community standards and cohesive implementations to maintain network consensus. This study introduces a novel methodology for identifying and measuring temporal inconsistencies in opcode mappings across Ethereum clients and the Solidity compiler. Using this methodology, we uncover significant and previously undocumented discrepancies both among different components of Ethereum’s implementation and between theoretical specifications and practical execution behavior. We further demonstrate the potential consequences of these inconsistencies by illustrating their impact on the detection of vulnerabilities in Solidity smart contracts. Such discrepancies can substantially undermine the accuracy and reliability of vulnerability analysis, highlighting the critical need for strict consistency in Ethereum’s operational semantics. Ensuring this consistency is essential for preserving transaction security and the overall robustness of the platform.
Arman Kolozyan, Tom Sorger, Alexander Hicks, Stefanos Chaliasos
Zero-knowledge proofs (ZKPs) have become a core technology for privacy and verifiable computing. They are used to secure blockchains that handle billions of dollars and identity applications dealing with sensitive personal data. However, ZKP systems are complex, and subtle implementation errors can completely break their guarantees, letting attackers forge money or false proofs of identity. Researchers and practitioners have therefore developed a growing set of bug detection and formal verification methods to secure these systems. Yet their real-world effectiveness and adoption remain unclear. In this paper, we aim to shed light on the state of ZKP security tooling. We first systematize the landscape of these tools and observe that most target Circom, leaving newer DSLs and zkVMs with limited support. We then evaluate six tools across 70 real-world vulnerabilities and find that while the tools detect 45.7% of bugs on isolated targets, their effectiveness drops to 19.6% on full codebases, with important vulnerability classes left unaddressed. We also present the first systematic analysis of formal verification efforts, revealing that current work focuses primarily on constraint correctness and identifying key gaps and risks. Finally, we survey 48 practitioners, showing that development and security remain human-led, LLMs are widely used, and practitioners prioritize tools with clearer guarantees and lower integration effort. Overall, our results highlight the need for better integration of security tooling with the development and auditing process, and we provide actionable insights for researchers and practitioners.
VSAT (Vulnerability Saturation Auditing) makes the completeness of an LLM security audit a measurable, calibrated quantity. It runs several deliberately diverse LLM audit "lenses" over the same codebase and treats each lens as a capture occasion, so the overlap structure yields (i) a far more complete union vulnerability list and (ii) a Chao2 richness estimate of the undiscovered population. VSAT combines this statistical discovery saturation with a deterministic OWASP ASVS structural coverage into a single completeness score (Phi = C_struct x C_hat) and derives a saturation-based stopping rule. Implemented as a security-audit skill on the cc-rsg-web agentic platform, VSAT attains 94.7-100% category recall and 99.1% code-verified precision on three documented benchmark applications (NodeGoat, django.nV, DVWA), delivers a 2.4-3.4x discovery uplift over a single pass with a per-finding proof-of-concept and regression test, and its non-zero residual estimate is corroborated by an independent real-world field validation. To our knowledge this is the first method to bring capture-recapture completeness estimation and a saturation stopping rule to LLM-based web-application security auditing.
Blockchains have evolved from simple distributed ledgers into programmable platforms that process complex application logic and carry significant financial value. All modern Web3 systems share a common goal: providing secure, decentralized, and trustworthy execution in an increasingly interconnected environment. However, this evolution has shifted the attack surface from isolated infrastructure disruptions to programmable economic abuse and cross-domain exploits. In this article, we focus on the research of blockchain attacks and defenses. In particular, we categorize the threat landscape and corresponding mitigation strategies according to both a four-tier layered architecture (network, cryptographic, consensus, and application) and cross-domain trust boundaries. We seek to answer these important questions: How has the research in blockchain security evolved over the past decade, especially with the rise of decentralized finance (DeFi) and cross-chain interoperability? How do local security assumptions fail when protocols are composed, and what are the driving needs for Web3 security research in the future?
Abstract Smart contracts are the fundamental building block of decentralized applications (DApps) and decentralized finance (DeFi). However, their immutability makes security flaws exceptionally costly. Despite advancements in vulnerability detection, such as static and dynamic analysis, formal verification, and Solidity language improvements, vulnerabilities continue to result in substantial financial losses, exceeding $2 billion in 2024 alone. This paper presents a comprehensive analysis of smart contract vulnerabilities derived from real-world exploits, systematically categorized into seven distinct types. Each category is illustrated with Solidity code examples and insights from notable exploits. An Enhanced test suite is developed by restructuring the existing solidity-defects-and-bugs suite and supplementing it with new smart contract implementations to address underrepresented vulnerabilities, including flash loan and price oracle manipulation. We evaluate three widely used analysis tools (Slither, Mythril, and 4naly3er) on both the original and Enhanced suites, revealing substantial limitations in detection coverage. To address these limitations, we introduce the Solidity Defects and Bugs Analysis (SDABA), which incorporates advanced analyses and detectors to identify 28 vulnerability variations across both suites. Results on the SDB and Enhanced test suites show that SDABA improves overall precision, recall, and F1-score compared with the evaluated tools. Finally, we release the source code, test suite, and vulnerability reports to support future research in smart contract security.
Smart contracts have attracted rapid development and widespread application. Due to the complexity of real-world smart contracts, it is error-prone to correctly enforce all intended functionalities in code implementations, resulting in unintended functional behaviors and security issues in practice. Code-comment inconsistency detection has emerged as an important solution to these issues, which leverages the redundant functional specifications in comments to detect code implementations that violate developers' intentions. However, existing inconsistency detection solutions are typically pattern-based and limited to fixed types of inconsistencies, which prevents them from detecting the diverse inconsistencies between real-world code implementations and casually written comments. To bridge the gap, this paper presents SmartComment, the first technique that combines LLMs with program analysis techniques for detecting code-comment inconsistencies in smart contracts. SmartComment introduces an LLM-driven workflow which simulates real-world interactions between code reviewers and developers to identify inconsistencies. It incorporates various program analysis techniques into the workflow, including comment propagation and code context extraction for generating input context for inconsistency detection, as well as program variant generation and differential analysis for inconsistency confirmation. Our evaluation results show that SmartComment detects 203 valid inconsistencies from a dataset of 1,000 real-world contracts with a precision of 79.9%, highlighting its effectiveness in detecting prevalent and diverse real-world inconsistencies. Compared to previous work, SmartComment achieves both higher precision and recall, detecting over 90% of inconsistencies that existing methods fail to identify. Furthermore, an ablation experiment demonstrates the effectiveness of incorporating program analysis techniques into SmartComment, improving the F1-score from 58.7% to 81.3%.
Mingxi Ye, Yuhong Nan, Zhijie Zhong, Jianzhong Su · 7 authors
Given the critical nature of Ethereum, exploiting 1-day vulnerabilities that are patched but not yet widely deployed is essential. Meanwhile, Automatic Patch-based Exploit Generation (APEG) is a promising technique for this, as it helps developers understand root causes, verify fixes in downstream forks, and detect incomplete patches. However, existing exploit generation tools can not work well for vulnerabilities on Ethereum due to three key unique challenges: (1) navigating complex and cross-language exploit paths hidden within patches, (2) synthesizing complicated and stateful environment configurations, and (3) handling non-deterministic inconsistencies between blockchain nodes that lead to false alarms. To address these challenges, we introduce ChainDelta , a novel fuzzing agent framework driven by Large Language Models to automatically generate exploits based on Ethereum security patches. ChainDelta consists of three core modules: a directed fuzzer utilizes call graph analysis to guide testing towards vulnerable code based on the patch information; an agent-based environment fuzzer acts as an expert to automatically set up the necessary blockchain states to trigger vulnerabilities; and finally, a state-aware sanitizer performs differential analysis while monitoring the blockchain transient state to distinguish true inconsistencies from benign non-determinism. We evaluate ChainDelta on a diverse benchmark with real-world patches, covering a wide range of types such as data racing and denial-of-service. ChainDelta successfully generated exploits with a 64% success rate and only a 15.8% false positive rate. An ablation study confirms the contribution of each module to the overall performance. To demonstrate its practical impacts, we conducted a real-world auditing campaign on top of ChainDelta , leading to the discovery of four previously undisclosed vulnerabilities with bug bounties.
Serving as the first touch point for users to the cryptocurrency world, cryptocurrency wallets allow users to manage, receive, and transmit digital assets on blockchains and interact with emerging decentralized finance (DeFi) applications. Unfortunately, cryptocurrency wallets have always been the prime targets for attackers, and incidents of wallet breaches have been reported from time to time. Although some recent studies have characterized the vulnerabilities and scams related to wallets, they have mostly been studied at a coarse granularity, overlooking potential risks inherent in detailed designs of cryptocurrency wallets, especially from perspectives including user interaction and advanced features. To fill the void, in this paper, we present a fine-grained security analysis of browser-based cryptocurrency wallets. To pinpoint security issues in wallet components, we design WalleTruth, a visual-oriented testing framework specifically for browser-based wallet extensions. We have identified 12 attack vectors that can be abused by attackers to exploit cryptocurrency wallets and exposed 21 concrete attack strategies. By applying WalleTruth on 39 widely-adopted browser-based wallet extensions, we find that all of them can be abused to steal crypto assets from innocent users. Identified potential attack vectors were reported to developers in a timely manner and 26 issues have been patched already. This calls for urgent action from the community to mitigate threats related to cryptocurrency wallets.
Self-sovereign identity (SSI) represents a paradigm shift in digital authentication, transferring control from centralized identity providers to individual users (Mühle et al., 2018). This paper presents the Kathon Vault identity system, which implements self-sovereign browser identity through BIP39 mnemonic seed phrases (Palatinus et al., 2013) for Ed25519 hierarchical deterministic (HD) key generation (Bernstein et al., 2012; Wuille, 2012). The system generates a master seed from a BIP39 mnemonic (12, 18, or 24 words with configurable passphrase), derives Ed25519 keypairs through the SLIP-10 key derivation scheme (Přikryl, 2022), and enables zero-knowledge authentication across websites through a novel browser-native WebAuthn-hybrid protocol. We demonstrate that the BIP39-derived Ed25519 keys provide equivalent security to standard FIDO2/WebAuthn authenticators (316 bits of entropy for 24-word phrases) while offering three critical advantages: (1) deterministic key recovery from the mnemonic phrase alone, (2) hierarchical key organization matching the SLIP-44 registered coin type for Kathon, and (3) cryptographic privacy through zero-knowledge proofs that enable selective attribute disclosure without revealing the master public key. In a security analysis against brute-force, dictionary, side-channel, and social engineering attacks, the system achieves resistance levels exceeding NIST SP 800-63B Level 4 authentication assurance requirements (NIST, 2020). A usability study with 48 participants demonstrates that BIP39-based authentication achieves 96% successful login rates with 14% lower task completion time compared to password manager-based workflows. This work establishes mnemonic-based HD key generation as a viable and superior alternative to federated identity providers for browser-based authentication. --- Part of The Anticloud research corpus by Lois-Kleinner Alpasan (ORCID: 0009-0009-2233-6107). This work explores browser engine, privacy in the context of sovereign AI infrastructure, post-cloud computing architectures, and transparent, blackbox-free systems.
Vulnerability disclosure volumes now far exceed organizational assessment capacity, yet three adjacent research communities (proof-of-concept generation, vulnerability prioritization, and detection rule engineering) operate largely in isolation. Existing automated exploit generation systems report binary pass/fail outcomes, discarding partial progress and producing no signal for the other two communities. This paper presents FORGE, a multi-agent system that bridges these three silos through graduated exploitation depth. Five specialized agents (Intel, Generator, Planner, Exploit, and Detector) execute in a fixed pipeline that (1) generates targeted vulnerable applications from CVE metadata, (2) conducts coached, multi-turn exploitation assessed by an LLM-primary oracle on a four-level taxonomy (L0: no evidence through L3: full compromise), and (3) produces Sigma and Snort detection rules grounded in OpenTelemetry exploitation traces. Graduated depth is the bridging mechanism: deeper exploitation yields richer behavioral traces for detection engineering, while depth data across scoring bands provides ground truth for prioritization validation. A tiered knowledge architecture accumulates intelligence across assessments, transferring build and exploitation experience to subsequent CVEs. Evaluation on 603 CVEs from the CVE-GENIE dataset achieves 67.8% end-to-end L1+ exploitation at USD 1.50 per CVE across eight languages and 187 CWE types. Exploitation rates remain near 68% regardless of EPSS or CVSS band, indicating that pattern-level reachability is orthogonal to metadata-based prioritization. Detection rules from L2+ exploitation achieve significantly higher span-normalized grounding than L1-derived rules (p=0.035), and 93.4% of generated Snort rules produce zero false positives against a synthetic benign corpus.
Bagus Rakadyanto Oktavianto Putra, Muhamad Risqi U. Saputra, Widyawan, Guntur Dharma Putra
Smart contracts face critical security challenges that require thorough auditing in decentralized web services. While Large Language Models (LLMs) have shown promise in automated vulnerability detection, existing approaches lack severity evaluations with actionable remediation and demand unnecessarily massive computational overhead. In this study, we introduce an efficient end-to-end smart contract security audit framework utilizing lightweight, highly optimized open-source LLMs (0.6B-4B parameters). Our framework decouples comprehensive audit tasks into four interconnected components: vulnerability detection, explanation, severity classification, and remediation recommendation. To maintain high accuracy without massive parameters, we implement Rank-Stabilized Low-Rank Adapters (rsLoRA), knowledge distillation, and a custom Chain-of-Verification (CoVe) aggregation strategy to systematically screen and consolidate multiple draft responses from the model into a highly accurate audit report. Experimental results demonstrate that our lightweight pipeline consistently outperforms state-of-the-art open-source coder dense LLMs (7B to 34B parameters), achieving 98.25% accuracy in vulnerability detection and an alignment score of 0.4375 in generative explanation tasks. Furthermore, our extensive ablation studies empirically validate the superiority of our decoupled audit processes over unified prompting and uncover a novel severity centrality bias, establishing a critical benchmark for future research in LLM-assisted auditing.
Penelitian ini berfokus pada pengembangan framework autentikasi tanpa kata sandi (passwordless) berbasis Web3 yang diimplementasikan pada platform mobile guna mengatasi kerentanan metode tradisional terhadap serangan phishing dan brute force. Framework yang diusulkan mengintegrasikan aplikasi mobile dengan backend Node.js/Express.js dan smart contract standar ERC-5192 pada jaringan Ethereum Sepolia Testnet sebagai representasi identitas digital Soulbound Tokens (SBT) yang permanen dan non-transferable. Demi menjaga privasi, sistem ini menerapkan teknologi Zero-Knowledge Proof (ZKP) berbasis zk-SNARKs skema Groth16 menggunakan Circom dan SnarkJS yang dieksekusi di sisi klien (client-side browser) menggunakan WebAssembly (WASM), serta dipadukan dengan struktur data Merkle Tree tingkat kedalaman 20 dan mekanisme nullifier untuk mencegah replay attack. Hasil pengujian menunjukkan tingkat keberhasilan autentikasi mencapai 100% dari 50 kali percobaan. Pemindahan beban komputasi sirkuit ZKP (5.359 konstrain) ke sisi klien terbukti efisien dengan waktu eksekusi komputasi lokal jika diakumulasikan dari tahap awal koneksi wallet (0,8 detik), pembuatan witness (1,2 detik), pembuatan proof (4,8 detik), hingga verifikasi smart contract (210 ms), maka Total Authentication Time adalah sebesar 6,3 detik. Nilai ini membuktikan kelayakan framework ini sebagai solusi manajemen identitas yang aman, privat, dan responsif.
The rapid adoption of Web3 infrastructures has led to a growing number of security incidents affecting cryptocurrency exchanges, custody services and blockchain-based platforms. While existing research predominantly focuses on vulnerabilities in smart contracts and blockchain protocols, a substantial portion of real-world losses originates from off-chain systems, organizational processes and human-centered operational workflows. This paper presents a qualitative, incident-based analysis of publicly documented, high-impact security breaches in the Web3 ecosystem, including the Bybit exchange incident (2025), the Ronin Network bridge compromise (2022), and the DMM Bitcoin exchange breach (2024). The selected cases are systematically analysed and mapped to established Web2 security reference frameworks, including OWASP-based vulnerability categories and organizational security control domains. The results indicate that dominant failure patterns in Web3 environments are insufficiently addressed by generic security control catalogues, particularly with respect to cryptographic key management, transaction approval governance, signer and validator infrastructure, third-party tooling dependencies, and human-in-the-loop processes. Based on these findings, this paper argues for the adoption of established information security management systems (ISMS) in Web3 organizations and derives a structured set of blockchain-specific cybersecurity control categories to operationalize existing ISMS frameworks for blockchain-based systems. The proposed categories aim to bridge the gap between generic security governance frameworks and domain-specific risks inherent to Web3 infrastructures.
Zero-knowledge proofs (ZKP) provide strong cryptographic guarantees allowing a prover to demonstrate knowledge of a property without revealing the underlying secret. These mechanisms are increasingly deployed in blockchain systems, digital identity infrastructures, web proofs, confidential finance, and privacy-preserving computation. However, many practical deployments rely on an often-overlooked component: the trusted acquisition and semantic extraction chain responsible for obtaining, interpreting, and transforming real-world data into proof witnesses. While proof verification may be cryptographically trustless, the acquisition process itself frequently depends on trusted runtimes, transport security, credential issuers, parsers, APIs, browser hooks, secure execution environments, or privileged software components. This paper argues that practical proof systems do not eliminate trust entirely, but frequently displace it toward increasingly complex acquisition infrastructures. We introduce the notions of Trusted Acquisition and Governed Disclosure, where programmable trust anchors and trusted governance platforms provide explicit, attestable, and policy-controlled acquisition boundaries. We further show that once such trusted acquisition layers already exist — as is often the case in industrial, enterprise, embedded, regulated, and digital identity systems — they may also provide simpler and more deployable alternatives to selected zero-knowledge constructions through governed disclosure mechanisms. The paper does not argue against zero-knowledge proofs. Instead, it proposes a complementary architectural perspective distinguishing between trustless verification and trustworthy acquisition.
Gabriela Dobrita, Simona-Vasilica Oprea, Adela Bara
Smart-contract exploits have caused billions of USD in cumulative losses, yet audits remain expensive and slow. Automated tools have emerged to close this gap, but each class has a characteristic failure mode. Static analyzers report findings that frequently fail manual triage at high rates, while large language models (LLMs) hallucinate findings that contradict the source code. Thus, we propose Chaintrix, an end-to-end auditing framework whose central architectural commitment is that every LLM-generated claim must be discharged against a deterministic structural contract representation. We introduce a Cross-Contract Interaction Model (CCIM) that parses Solidity into a structured map of function-level reads, writes, modifiers and resolved cross-contract calls. CCIM serves as the substrate against which all 12 of Chaintrix's deterministic signal engines and the parallel LLM audit pipelines operate. A staged false-positive-reduction pipeline, terminating in a Structural Verdict Engine (SVE) that applies deterministic structural checks against parsed code, filters the merged finding set, with selected high-confidence findings further validated through symbolic execution and fuzz testing. We evaluate Chaintrix on EVMbench, the smart-contract security benchmark by OpenAI, Paradigm, OtterSec. Chaintrix detects 86 of 120 high-severity vulnerabilities (71.7% recall), with 25 audits scoring 100% recall, placing Chaintrix 26 percentage points above the strongest frontier-model baseline.
Smart contract vulnerabilities in Decentralized Finance caused over billions of dollars losses every year, yet the security community faces a critical bottleneck: identifying a vulnerability is not the same as proving it is exploitable. Manual PoC construction is prohibitively labor-intensive, leaving most disclosed vulnerabilities unverified and protocols exposed long before mitigation is applied. In this paper, we propose \sys, a knowledge-driven agentic system for end-to-end contract vulnerability detection and exploit synthesis. Our core insight is that exploit synthesis is not a code generation task but a \emph{structured reasoning problem} that requires grounded knowledge of protocol semantics, failure root cause, and exploit primitives. \sys organizes this knowledge into a \emph{Hierarchical Knowledge Graph} (HKG) that serves as structured memory for LLM-guided multi-hop reasoning. To validate exploit feasibility beyond code synthesis, \sys employs a two-stage validation framework that checks exploit-path reachability via SMT solving and profit realizability via asset-level state simulation, ensuring generated PoCs satisfy both logical and economic viability constraints. Evaluated on 88 real-world DeFi attacks and 72 audited projects (2,573 contracts), \sys achieves 98\% recall and 0.9 F1-score in detection, and a 96.6\% exploit success rate (ESR), reproducing 85 historical exploits and recovering over \$116.2M revenue. \sys outperforms SOTA fuzzers (\textsc{Verite}, \textsc{ItyFuzz}) by up to $5\times$ in ESR and $300\times$ in recoverable value, and the LLM-based exploit generator \textsc{A1} by $2\times$ and $8.5\times$ respectively. In bug bounty evaluation, \sys identified 16 confirmed 0-day vulnerabilities, helping secure over \$70.6M and earning \$2,900 in bounties.
Transform the web into your data source. Chapter 10 introduces methods for extracting financial data and downloadable files from websites using Python tools such as BeautifulSoup and requests. Learners will practise legal and ethical scraping through examples based on demonstration sites. The chapter includes a compliance checklist covering permissions, terms of service, and data protection. It also introduces the use of application programming interfaces for accessing financial data, including cryptocurrency prices from CoinGecko.
Detecting vulnerabilities in smart contracts is a critical challenge for blockchain security, as flaws such as reentrancy, timestamp dependence, and infinite loops have resulted in severe financial losses in decentralized systems. Accurate and interpretable detection of these vulnerabilities remains challenging due to the complex semantics of smart contract code. In this study, we propose a multimodal hybrid recurrent framework for smart contract vulnerability detection that integrates sequential and structural code representations. The framework introduces a Selective Subpattern Activation (SSA) mechanism, which highlights vulnerability-indicative code subpatterns during the pattern extraction phase and provides interpretable insights into model predictions. Pattern-based features enhanced by SSA are processed using a Bidirectional Gated Recurrent Unit (BiGRU), while structural features derived from control and data flow representations are modeled using a Bidirectional Long Short-Term Memory (BiLSTM) network. The proposed approach is evaluated on a publicly available Ethereum smart contract dataset using five independent experimental runs, with results reported as averages. The results show that the framework achieves an accuracy of 92.16% and an F1 score of 88.83% for reentrancy vulnerability detection, achieving higher performance compared to baseline deep learning and graph-based models. Ablation experiments are performed to demonstrate the contribution of the SSA mechanism to both detection performance and interpretability.
With the help of pact technology, a program that has been developed, the smart contract can take place between two or more entities without any third-party actor. Although smart contracts provide transparency and efficiency, security flaws in smart contracts have resulted in costly attacks, including re-entrancy, integer overflows, and access control violations. Current tools for intelligent contract verification, such as Mythril, Oyente, and Securify, mainly apply symbolic execution, taint analysis, and pattern matching to identify vulnerabilities. However, these tools have many false positives, take a lot of time to execute, and don't scale efficiently with large numbers of contracts. In this context, the paper presents VeriChain. This formal verification framework combines Control Flow Graph (CFG) analysis, symbolic execution, and static analysis to improve vulnerability detection and tackle the challenges above. VeriChain systematically constructs the contract’s Control Flow Graph (CFG), explores CFG execution paths with symbolic execution, and employs a set of rules for performing rule-based static analysis that can uncover vulnerabilities. Using CFG-based dependency tracking, VeriChain achieves enhanced analysis of dependencies among functions and coverage of execution paths, thereby reducing the number of false positives while achieving accurate detection results. The experimental results show that VeriChain obtains 98.3% detection accuracy, higher than Mythril, Oyente, and Securify. Compared to existing tools, VeriChain has a much lower false-positive rate (1 false alarm) and a much faster execution time (Running in only 2.3 seconds). This framework gives a structured security assessment by categorizing the vulnerabilities according to severity and execution traces, ensuring that the smart contracts are accessed under heavy security verification pre-deployment. With its ability to accomplish highly accurate results efficiently whilst providing structured ways to report on security, VeriChain will be an influential component in delivering safe, innovative contract launches to decentralized applications for blockchain developers and security analysts.