## 5 Experiments
### Testing Using Tools  
This subsection presents the results of tests performed using automated analysis tools. The security evaluation utilized two widely adopted static analysis tools: Slither [46] and Mythril [47]. Slither was executed with enabled default detectors and targeted vulnerabilities related to reentrancy, access control, uninitialized storage, and gas optimization. Mythril was configured in symbolic execution mode, using Solidity 0.8.28 bytecode compiled without optimization. The detected issues were classified according to the Smart Contract Weakness Classification Registry (SWC), which provides standardized identifiers for common smart contract flaws. In this study, formal verification is understood as a property-oriented vulnerability analysis supported by symbolic execution, as implemented in the aforementioned tools, rather than in the form of mathematical proofs or theorem-proving techniques. We started with Mythril, a widely adopted tool to assess the security of solidity-based smart contracts. The results of the analysis are presented in Table 4.  
Each identified vulnerability is assigned a unique SWC code, which facilitates the identification and remediation of known security problems. The analysis identified potential risk categories commonly associated with Solidity-based contracts. However, in the case of BlockScribe, all relevant risks were inherently mitigated using the Solidity version 0.8.28 or explicitly addressed through appropriate access control and validation mechanisms. Table 4 summarizes the risk areas reviewed and the corresponding preventive measures applied in the contract design. One of the identified issues, classified as SWC 114, arises from the dependence on the order of the transactions. The function responsible for fund withdrawals is based on the contract balance at the time of execution, making it susceptible to race conditions. If the contract state changes between two function calls, an attacker could manipulate the balance before the transaction is completed, leading to incorrect fund distribution. Implementing reentrancy locks or unique transaction identifiers can help mitigate this risk. Another vulnerability, classified as SWC 110, is related to the improper use of assertions within the function that returns subscriber addresses. The use of the _assert()_ function in this context is inappropriate, as assertions should only validate conditions that are always true. If an attacker provides an invalid input, such as an excessively large index, the function may trigger an assertion failure, interrupting contract execution. Replacing _assert()_ with _require()_ would ensure that invalid inputs cause the function to terminate gracefully rather than leading to unexpected behavior. A more critical issue, classified as SWC-106, refers to smart contracts where the _selfdestruct()_ function is not properly access-controlled. In the case of BlockScribe, this risk is mitigated by design--the _selfDestructContract()_ function is protected by a _require_(_msg.sender \(==\)owner_) check, ensuring that only the contract owner can invoke this operation. The last identified risk, classified as SWC 101, concerns arithmetic operations that may be vulnerable to integer overflow and underflow. The mathematical operations within the contract could exceed the limits of the specified data types, resulting in unexpected errors. This vulnerability is inherently mitigated in Solidity 0.8.28, which includes native arithmetic checks that eliminate the need for external libraries such as SafeMath. Although this study adopts the SWC registry as the basis for identifying and categorizing vulnerabilities, it is worth noting that the SWC framework is no longer actively maintained. However, it remains widely used in academic and tool-supported analyses, particularly in automated vulnerability scanners such as Mythril. Its structured taxonomy still provides a valuable reference point for systematic assessment.