{"id":"d06af2cc-90ff-40cb-8bec-a44836ccbc7f","arxiv_id":"2507.04357","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":3.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A tool predicts read-write, write-write, and call-chain conflicts in Ethereum smart contracts via static analysis, reporting 92% precision and claiming zero false negatives without proof.","lead":"This paper introduces a static analysis tool that scans Solidity smart contract code and flags pairs of transactions that could conflict by reading or writing the same state variables. It reports these conflicts before execution to help validators schedule transactions in parallel, but the evidence is based on a small manual review.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The claimed proof of zero false negatives is contradicted by the tool's syntactic access extraction and by Algorithm 1's exclusion of view functions, both of which omit real storage conflicts.","rationale":"The reader's weakest assumption correctly identifies the syntactic pattern-matching limitation in Step 2 as a source of false negatives. My pass agrees with that core concern and adds a second, distinct mechanism: Algorithm 1's SHOULDSKIP returns true for all view functions, so view functions cannot participate in any conflict pair, even though Section IV-B explicitly says they are considered for read-write conflicts. This is an internal inconsistency that independently breaks the zero-false-negative guarantee. The reader mentioned this inconsistency in the rationale but did not make it part of the weakest assumption. No formal proof is provided; the paper only asserts the guarantee. The evaluation measures precision (92% on a sample of 50), not recall, so it cannot support a completeness claim. My proposed minimal contract gives a concrete, checkable falsification: the deposit/check pair should be a read-write conflict but is excluded because `check` is skipped; the `arr.push` write should be recorded but is likely missed by the simple pattern matcher. Given these issues, the central claim as stated is unsupported and likely false for realistic Solidity code. However, the underlying approach is reasonable and could be made sound with a proper source-level data-flow analysis over storage slots, so a conditional verdict asking for such fixes and a recall-sensitive evaluation is the right balance. No ad hominem is intended; the critique is strictly on the argument and algorithm.","tokens_in":11402,"tokens_out":2391,"duration_ms":27813,"concrete_test":"Build a minimal Solidity contract with: (1) `mapping(address => uint256) public balances;` and a public function `deposit() external { balances[msg.sender] += msg.value; }`; (2) a public view function `check() external view returns (uint256) { return balances[msg.sender]; }`; and (3) a public function `pushValue(uint256 v) external { arr.push(v); }` where `arr` is a state array. Run the published tool on this contract. If it reports zero read-write conflicts between `deposit` and `check`, or fails to classify `arr.push` as a write, the zero-false-negative claim is falsified. Independently, patch Algorithm 1 so SHOULDSKIP does not exclude view functions, rerun the analysis on the same contract, and compare conflict counts; the increase reveals the missing read-write conflicts caused by the view-function exclusion.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is a proof of zero false negatives (Section I, contribution 5). This claim rests on Step 2 (Section IV-B) and Algorithm 1, but two concrete mechanisms produce false negatives. First, the pattern matcher recognizes only simple variable names followed by assignment or increment/decrement operators for writes, and variable names not followed by assignment for reads. Common Solidity storage accesses are not simple: `balances[msg.sender] += amount` has `balances` followed by `[`, and `storageArray.push(_value)` has `storageArray` followed by `.`. These writes are not recognized as writes, so read-write and write-write conflicts involving array, mapping, and struct storage are missed. Second, Algorithm 1's SHOULDSKIP returns true for view functions, so view functions are excluded from all conflict pairs. This directly contradicts Section IV-B, which states that view functions are considered for read-write conflicts. A concurrent read by a view function and a write by a non-view function is exactly a read-write conflict and is silently omitted. No formal proof is supplied anywhere; Section I merely asserts the guarantee. Section VI measures precision on 50 manually reviewed conflicts but never measures recall against a ground truth, so these omissions would not be detected. The completeness guarantee is load-bearing because the tool's usefulness for conflict-based scheduling depends on not missing conflicts.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a static analysis method and open-source tool for detecting potential transaction conflicts in Ethereum smart contracts. It parses Solidity source, identifies state-variable read/write/function-call accesses via pattern matching, and enumerates public/external function pairs to report read-write (RW), write-write (WW), and function-call (FCC) conflicts. The authors claim exhaustive coverage and a proof of zero false negatives and low false positives. They evaluate on 100 mainnet contracts, reporting 423 conflicts, 78% of contracts with at least one conflict, 92% precision on a manually reviewed sample of 50 conflicts, and an average analysis time of 312 ms.","tokens_in":11654,"tokens_out":3349,"duration_ms":38671,"significance":"If the completeness guarantee were sound, the tool would be valuable for conflict-aware transaction scheduling, auditing, and MEV analysis; the paper also contributes a useful conflict taxonomy, an open-source implementation, and a real-contract dataset. However, the central load-bearing claim is a formal 'zero false negatives' guarantee, and the described algorithm does not actually provide such a guarantee: the syntactic pattern matcher misses common Solidity storage accesses, and Algorithm 1 excludes view functions despite the text saying they are considered in RW conflicts. These are concrete false-negative mechanisms, and no proof or recall measurement is provided. The paper's empirical contribution is a limited precision assessment on 50 manually inspected conflicts, which cannot validate completeness.","major_comments":[{"comment":"The claimed zero-false-negative guarantee is contradicted by the described access-extraction method. Section IV-B states that read operations are 'variable names that are not followed by assignment operators' and write operations are 'variable names followed by assignment operators (=, +=, -=, etc.) or increment/decrement operators (++, --)'. This pattern matcher does not recognize standard Solidity storage accesses such as `balances[msg.sender] += amount`, `storageArray.push(_value)`, or `mapping[key] = value`, because the variable name is followed by `[` or `.` rather than by the assignment operator. Any RW or WW conflict involving mapping, array, or struct storage is therefore silently omitted. A pessimistic analysis that 'ensures no false negatives' must conservatively over-approximate all storage accesses; this pattern matching is not conservative. The proof promised in Section I (contribution 5) is never supplied, and Section IV's statement about the Turing-complete language making precise prediction impossible does not justify the weaker claim actually implemented.","section":"Section IV-B, Algorithm 1"},{"comment":"Algorithm 1's SHOULDSKIP function returns true for 'private, internal, or pure/view' functions, so all view functions are excluded from conflict enumeration. This directly contradicts Section IV-B, which states that 'View functions can read but not modify state variables, so they are only considered for read-write conflicts.' A read-write conflict between a view function and a non-view function is exactly the case the text says should be detected, yet the algorithm skips it. This is a concrete false-negative mechanism for the most common conflict type reported in the evaluation (58.6% RW conflicts). The contradiction must be resolved, and the completeness claim must be stated for the actual algorithm.","section":"Algorithm 1, line 24"},{"comment":"The precision and recall evaluation does not measure what the central claim requires. Precision is estimated by manually reviewing 50 detected conflicts (92% true positives), but no confidence interval, sampling procedure, or inter-reviewer agreement is reported. Recall is addressed only by saying the tool 'successfully identified all of them' on 'a subset of contracts with known transaction ordering dependencies', with no list of those contracts, no definition of known truth, and no quantitative result. Since the false-negative mechanisms in Algorithm 1 and Section IV-B would not be visible in a precision-only study, the evaluation cannot support the zero-false-negatives assertion. The paper should either provide a conservative access-extraction method with a correctness argument, or explicitly replace the completeness claim with a weaker soundness statement and evaluate recall against a real ground-truth set.","section":"Section VI-C"}],"minor_comments":[{"comment":"The pseudocode contains typographical and formatting errors that obscure the intended logic: 'fundctions' should be 'functions', the sentence after the algorithm is cut off at 'returns the ordered pair (fi, fj) where', and Algorithm 2 line 21 places `return conflicts` on the same line as the union operation without a newline. These should be cleaned up.","section":"Algorithm 1 and Algorithm 2"},{"comment":"The subsection heading 'subsectionResults' is missing a space and is not formatted as a proper subsection; the results section also references figures without showing them after the text, making the reported distributions hard to verify.","section":"Section VI-B"},{"comment":"The description of Solidity state mutability lists 'Non-reentrant and non-payable (default)' as a mutability type. Non-reentrancy is a modifier, not a state mutability; only pure, view, payable, and nonpayable are mutability qualifiers. This is a technical inaccuracy in the background section.","section":"Section II-A2"},{"comment":"The code listing is missing spaces and punctuation due to formatting, e.g., 'pragma s o l i d i t y^ 0 . 8 . 0 ;' and 'c o n t r a c tE x a m p l e{'. A reformatted, compilable version would improve reproducibility and clarity.","section":"Listing 1"}],"recommendation":"major_revision","confidential_remarks":"The paper is within scope and the artifact is potentially useful, but the central completeness claim is currently unsupported and contradicted by the described algorithm. The issues are fixable by reworking the access extraction to be conservative, including view functions in the enumeration, and either proving or explicitly weakening the guarantee. I see no reason to reject on novelty or circularity grounds; the self-citation to Conthereum is minimal and does not create circularity."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. First, the evaluation on 100 real contracts gives the community concrete numbers on how common read-write, write-write, and function-call conflicts actually are. That part is fine. Second, the advertised proof of zero false negatives is not just unproven; it is contradicted by the algorithm in the paper. The stress-test note is right.\n\nWhat is new: a simple syntactic static analyzer for Solidity storage conflicts, an open-source tool, and a dataset-derived picture of conflict prevalence (58.6% RW, 30.2% WW, 11.2% FCC). The taxonomy is standard but clearly laid out. Running the tool on 100 contracts and reporting precision on a 50-conflict manual sample is a reasonable first step, though it only measures precision.\n\nWhere it falls apart: the completeness claim. Section I says the paper provides a proof of zero false negatives and low false positives. No proof appears anywhere. More concretely, Algorithm 1's SHOULDSKIP returns true for view functions, yet Section IV-B says view functions are considered for read-write conflicts. That is a direct internal contradiction. And the pattern matcher in Step 2 only catches writes of the form `var = ...` or `var++`. It misses `balances[msg.sender] += amount` and `storageArray.push(_value)`, because the variable name is followed by `[` or `.`, not an assignment operator. Those are common Solidity storage writes, so the zero-false-negative guarantee fails on everyday code. The evaluation never measures recall against any ground truth, so these omissions would go unnoticed.\n\nThese are load-bearing flaws for the stated purpose: if the tool is meant to drive conflict-based scheduling, missing conflicts is exactly what matters. But the empirical mapping of conflict types and hotspots could survive if the authors drop the completeness claim, fix the view-function handling, and either use a real Solidity parser or formally justify the pattern matcher's coverage. As written, the paper overstates what it delivers.\n\nThis is for researchers working on parallel execution for EVM chains who need a quick, cheap conflict estimate and can tolerate false negatives. It is not safe for scheduling without a proof of coverage. I would send this to peer review, because a good referee can force the authors to correct the record, and the empirical part has some value. Just don't cite the zero-false-negative claim.","headline":"Useful empirical data, but the paper's advertised zero-false-negative guarantee is refuted by its own algorithm, so the central claim as stated is unsupported.","tokens_in":12121,"tokens_out":3202,"would_cite":false,"duration_ms":34035,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A static analysis tool claims to detect every read-write, write-write, and function-call conflict between pairs of Ethereum transactions before execution.","keywords":["Ethereum","smart contracts","static analysis","transaction conflicts","concurrency","Solidity","conflict detection","blockchain scalability"],"falsifier":"Take a contract whose function writes storage only through an inline assembly block (for example `assembly { sstore(slot, value) }`) and run the tool; if the write set for that function is empty while another function reads the same slot, the tool will miss the read-write conflict, contradicting the claimed zero false negatives. Repeating this on any real contract with assembly or delegatecall would settle the claim's scope.","tokens_in":11232,"feed_emoji":"🔍","tokens_out":6689,"duration_ms":60379,"temperature":0.7,"pith_summary":"This paper aims to show that the three main ways transactions can interfere on the Ethereum blockchain—reading a value another transaction writes, writing the same slot as another, and clashing indirectly through nested function calls—can all be detected ahead of execution by reading Solidity source code alone. If true, validators and rollup sequencers could group non-conflicting transactions for parallel execution and avoid the expensive rollback-based runtime schemes used today, while developers would see conflict-prone function pairs before deployment. The paper grounds this in a concrete tool that parses contracts, extracts per-function read/write/call sets, and checks every pair of externally callable functions. On 100 real-world contracts the tool flagged conflicts in 78% of them, with read-write conflicts the most common at 58.6%, and a manual review of 50 flagged conflicts put precision at 92%. The authors back the approach with a stated proof of zero false negatives, meaning that whenever the tool reports no conflict between a function pair, that pair is guaranteed conflict-free under the analysis's syntactic model.","feed_headline":"Static tool flags every transaction conflict in Ethereum contracts","feed_subtitle":"Read-write and write-write clashes are found before execution, enabling parallel scheduling and fewer rollbacks.","key_machinery":"The mechanism is a pair-wise conflict scan over transaction-callable functions, driven by three per-function sets extracted from the Solidity abstract syntax tree: read variables, written variables, and called functions. Recursive closure over the call sets propagates transitive state access, and conflict checks reduce to set intersections: read-write if one function's read set meets another's write set, write-write if write sets intersect, and function-call if recursively closed access sets intersect with at least one write. The zero-false-negative guarantee rests on these extracted sets being exact for the syntactic patterns the parser accepts.","core_discovery":"The central discovery is a static, execution-free method that reduces transaction-conflict detection to set algebra over storage accesses. For every function that can start a transaction, the tool computes the set of state variables it reads, the set it writes, and the set of functions it calls; calling it recursively gives the transitive access footprint. Two functions conflict if the read footprint of one intersects the write footprint of the other (read-write), if the write footprints intersect (write-write), or if the recursive footprints intersect with at least one write (function-call). The paper claims this detection is exhaustive: a proof is sketched that any conflict occurring during EVM execution must be mirrored by one of these syntactic intersections, so there are zero false negatives relative to the model, while 92% precision is measured on a sampled ground truth.","pith_inferences":["A bytecode-level counterpart of this extraction could restore completeness for contracts that use inline assembly or delegatecall, since SLOAD and SSTORE opcodes are the true conflict carriers; the authors list assembly-aware and cross-contract analysis as future work, and our inference is that those extensions are required for the zero-false-negative claim to hold across the full EVM contract pop","The 8% measured false positives, attributed to missing control-flow dependencies, could be cut substantially by ranking conflicts with a lightweight dataflow reachability check, turning the tool into a precise triage rather than a conservative alarm.","The conflict-percentage metric as defined averages over all function pairs and so can be diluted in large contracts; a hotspot-weighted index would better reflect scheduling risk and would be a natural, testable refinement of the evaluation."],"forward_implications":["Ethereum validators could precompute conflicting transaction pairs within a block and dispatch independent pairs to different cores without runtime conflict tracking or rollback.","Rollup and sharding systems that reorder batches could use the same conflict matrix to keep execution deterministic while raising throughput.","Developers could add the check to their CI pipeline: a new function that writes a hot variable is flagged immediately, along with the severity rating, before deployment.","Security analysts could use the conflict matrix to focus formal verification and fuzzing on the function pairs that actually share state, rather than auditing all pairs uniformly."],"supporting_citations":[{"why":"Supplies the baseline runtime conflict-detection-and-rollback approach whose overhead the paper aims to eliminate with static prediction.","marker":"[5]"},{"why":"Demonstrates a transaction scheduler whose performance depends on precomputed conflict information, motivating the need for this analysis.","marker":"[6]"},{"why":"Anchors the static-analysis methodology for smart-contract auditing that this work extends from vulnerability patterns to transaction-level conflicts.","marker":"[1]"},{"why":"Establishes the AST-based static analysis framework for Solidity that informs the tool's parsing and access-extraction design.","marker":"[3]"},{"why":"Documents exploitable transaction-ordering dependencies in real contracts, grounding the security relevance of pre-execution conflict detection.","marker":"[9]"}],"fun_headline_variants":["Static analysis predicts Ethereum transaction clashes","Detect smart contract conflicts without executing them","Set algebra reveals read-write conflicts in Ethereum code","High-precision static tool for Ethereum transaction conflicts","Find transaction conflicts in Solidity before deployment"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The zero-false-negative guarantee rests on the assumption that every storage read and write appears in the source as a variable name directly beside an assignment, arithmetic operator, or increment/decrement operator, and that no access hides behind inline assembly, indirect references, or external calls.","fun_headline_variants_meta":{"raw":{"variants":["Static analysis predicts Ethereum transaction clashes","Detect smart contract conflicts without executing them","Set algebra reveals read-write conflicts in Ethereum code","High-precision static tool for Ethereum transaction conflicts","Find transaction conflicts in Solidity before deployment"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000195,"raw_usage":{"total_tokens":1365,"prompt_tokens":960,"completion_tokens":405,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":576,"completion_tokens_details":{"reasoning_tokens":338}},"tokens_in":576,"tokens_out":405,"duration_ms":4830,"temperature":1.0,"reasoning_tokens":338,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T19:48:50.232140+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a contract whose function writes storage only through an inline assembly block (for example `assembly { sstore(slot, value) }`) and run the tool; if the write set for that function is empty while another function reads the same slot, the tool will miss the read-write conflict, contradicting the claimed zero false negatives. Repeating this on any real contract with assembly or delegatecall would settle the claim's scope.","supporting_citations":[{"cited_title":"Adding concurrency to smart contracts,","cited_arxiv_id":null,"evidence_quote":"Supplies the baseline runtime conflict-detection-and-rollback approach whose overhead the paper aims to eliminate with static prediction."},{"cited_title":"Conthereum: Concurrent Ethereum Optimized Transaction Scheduling for Multi-Core Execution","cited_arxiv_id":"2504.07280","evidence_quote":"Demonstrates a transaction scheduler whose performance depends on precomputed conflict information, motivating the need for this analysis."},{"cited_title":"Slither: A static analysis framework for smart contracts,","cited_arxiv_id":null,"evidence_quote":"Establishes the AST-based static analysis framework for Solidity that informs the tool's parsing and access-extraction design."},{"cited_title":"Exploiting the laws of order in smart contracts,","cited_arxiv_id":null,"evidence_quote":"Documents exploitable transaction-ordering dependencies in real contracts, grounding the security relevance of pre-execution conflict detection."}],"review_version":1}