{"id":"c6dc9f72-e925-4f6e-919b-5b96b836dae2","arxiv_id":"1908.11227","paper_version":2,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A CEGIS-style verifier that automatically discovers transaction invariants achieves high recall and low false positives for arithmetic safety of Ethereum smart contracts.","lead":"VeriSmart is a new automatic verifier that checks Ethereum smart contracts for arithmetic overflow and division-by-zero bugs by discovering hidden transaction invariants during verification. On 60 real-world vulnerable contracts it caught every known bug with a 0.41% false positive rate, far better than existing tools.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Inter-contract calls are modeled as not modifying caller globals, but reentrant callbacks can mutate them, so the 'exhaustive' claim is unsound for valid Solidity.","rationale":"The reader's weakest_assumption correctly identified side-effect analysis over non-inlined and inter-contract calls as the most load-bearing assumption. My concern is a concrete instance of exactly that failure: a class of writes the side-effect analysis misses, namely writes performed by reentrant calls into the caller's own public functions. The paper explicitly asserts that inter-contract calls cannot modify the caller's state and therefore only return variables are invalidated, but in EVM semantics an external call can invoke any public function of the caller before returning, changing global storage. This makes the verifier unsound with respect to its own goal of exhaustive verification. The central empirical claim (100% recall, 0.41% false positive rate) is not enough to repair this, because the benchmark set apparently contains no reentrant inter-contract arithmetic cases; the algorithm's abstraction, not just its implementation, misses these behaviors. I therefore recommend a conditional verdict: accept only if the authors either restrict the exhaustive claim to non-reentrant contracts or extend the side-effect model to over-approximate reentrant writes. The paper has real independent support in its artifact, reproducibility, and careful manual evaluation, so no stronger negative verdict is warranted on this basis alone.","tokens_in":30606,"tokens_out":8585,"duration_ms":92381,"concrete_test":"Construct the two-contract benchmark: contract Main { uint public total; Attacker attacker; function setAttacker(address a) public { attacker = Attacker(a); } function setTotal(uint x) public { total = x; } function doWork() public { total += 1; attacker.poke(); assert(total + 1 >= total); } } and contract Attacker { Main main; function poke() public { main.setTotal(2**256 - 1); } }. With pre-0.8.0 wrapping arithmetic, starting total=0, doWork increments total to 1, poke reenters setTotal to 2**256-1, and the assertion fails. Run VeriSmart with default settings: if it reports no alarm for this contract, the unsoundness lands; if it reports the bug or times out, the concern fails to land.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"Section IV (Function Calls) handles inter-contract calls by invalidating only return variables, justified by the claim that 'inter-contract calls in Solidity cannot directly modify other contracts' states.' This is not sound under standard EVM semantics: an external call o.f() can reenter the caller (e.g., by invoking a public setter on the main contract) and change global storage before control returns. Because VeriSmart leaves the call-site precondition unchanged for all globals of the caller, a later arithmetic operation can be proved safe even though a concrete transaction violates the assertion. This is a load-bearing gap: the paper's central claim is exhaustive verification and detection of all arithmetic bugs, but the function-call abstraction omits a standard, exploitable execution pattern. The separate analysis of the called contract with entry/exit true does not repair the gap because state changes to the caller are never propagated back to the call-site formula. This is an internal soundness problem, not a disagreement with consensus, and it is stated directly in the paper's own Section IV.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents VeriSmart, a CEGIS-style verifier for arithmetic safety of Ethereum smart contracts. The algorithm iteratively discovers transaction and loop invariants, verifies them via basic-path construction and verification-condition generation, and discharges VCs with an SMT solver augmented by domain-specific preprocessing and fast syntactic checks. The implementation is applied to the full Solidity language up to inline-assembly caveats, with function calls handled by inlining and conservative side-effect weakening. The evaluation on 60 CVE-affected contracts and 25 contracts from the Zeus dataset reports 100% recall on known arithmetic CVEs, a 0.41% false-positive rate on the CVE benchmark, and substantial improvements over six existing tools, with the tool and data publicly released.","tokens_in":30855,"tokens_out":10039,"duration_ms":102164,"significance":"If the exhaustiveness claim can be made sound, this is a significant contribution to smart-contract security analysis. The paper is the first to apply a CEGIS-style loop to the automatic discovery of transaction invariants, and the evaluation is unusually thorough: all 492 alarms and 484 unreported queries on the CVE benchmark were manually inspected, four incorrect CVE reports were identified, and the comparison includes both bug-finders and verifiers. The basic-path VC generation and the proof of Proposition 1 are standard and well presented. The main correctness risk lies in the abstraction of inter-contract calls under reentrancy, which, as argued in the major comments, can make the verifier certify a vulnerable contract as safe. The paper also ships a reproducible implementation and public datasets, which is a clear strength.","major_comments":[{"comment":"The treatment of inter-contract calls is not sound under standard EVM semantics. The paper states that 'inter-contract calls in Solidity cannot directly modify other contracts' states' and therefore only invalidates return variables at inter-contract call-sites. This ignores reentrancy: an external call o.foo() can invoke a public function or fallback of the caller, which may modify the caller's storage before control returns. The call-site formula is therefore left too strong; VeriSmart can prove an assertion safe on a path in which the external call does not modify caller globals, while a concrete transaction that reenters the caller violates the assertion. The separate analysis of the called contract with entry/exit true does not propagate the reentrant state change back to the caller's call-site formula. Because the paper's central claim is exhaustive verification of arithmetic safety, this is a load-bearing soundness gap. I recommend havocing all caller globals reachable through reentrant callbacks (or conservatively all globals) at external calls, or restricting the exhaustiveness claim to contracts that do not perform external calls to untrusted addresses.","section":"§IV (Function Calls)"},{"comment":"The abstract and Section I claim that VeriSmart 'detect[s] all arithmetic bugs' and performs 'exhaustive verification', but the implementation supports the full Solidity language 'except for inline assembly', and the Inline Assembly paragraph states that VeriSmart 'may miss bugs hidden in embedded bytecode'. The side-effect replacement for assembly blocks is conservative only with respect to source-level variables, not with respect to arbitrary bytecode effects. These statements are in tension with the unconditional exhaustiveness claim. The claim should be scoped to 'all arithmetic bugs outside inline assembly', or the abstract and conclusion should be revised accordingly. This is not by itself a reason to reject, but it is part of the central claim and should be fixed.","section":"§IV (Inline Assembly) and Abstract"}],"minor_comments":[{"comment":"The free-variable test is a heuristic rather than a decision procedure, because it checks only condition (i) of Proposition 1. The paper correctly acknowledges that this may classify valid VCs as invalid, but the subsequent statement that the technique 'causes no false negatives' should be worded more carefully: it never certifies an unsafe query as safe, while it may create false alarms. Recommend presenting this as a precision-engineering technique with an explicit statement that the two ignored conditions are not checked.","section":"§III-D (Efficient Invalidity Checking)"},{"comment":"The equisatisfiability claim for the replacement of sum(x)=e by G1∧G2 is asserted but not proved. A short proof, or at least an explicit statement of the assumptions about the domain of the mapping and the fresh variable Rx, would strengthen the appendix.","section":"Appendix A (Preprocessing)"},{"comment":"The manual classification of the 484 unalarmed queries as true negatives is central to the reported 100% recall, but the methodology is not described. Reporting the number of inspectors, the classification criteria, and any cases of disagreement would make this result more convincing, especially since Section V-D acknowledges that such classification can be subjective.","section":"§V (Evaluation)"},{"comment":"The proof sketch for the BTX contract relies on the transaction invariant ∑i balance[i] = 10000, but the invariant as stated is not inductive without also assuming that the summation does not overflow. The paper mentions this condition in prose but does not show how the CEGIS loop discovers the pair. A sentence connecting this example to the refinement relation of Section III-C would help the reader.","section":"§II, Example 3"}],"recommendation":"major_revision","confidential_remarks":"The reentrancy gap in the inter-contract-call abstraction is the main technical blocker; if the authors conservatively model external calls, the paper's central contribution is defensible. The evaluation is otherwise strong and the tool is publicly available. I would also ask the authors to align the abstract's 'exhaustive' language with the inline-assembly limitation."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"VeriSmart is a strong tool paper with a genuinely new idea: a CEGIS loop that automatically infers transaction invariants for Solidity contracts, including sum invariants over mappings. The evaluation is real work—60 CVE-flagged contracts, six tools compared, manual alarm classification, and a nice side finding of six incorrect CVE entries. The tool and data are public. This deserves a serious referee.\n\nThe main soft spot is that the paper's central \"exhaustive verification\" claim is unsound for contracts with reentrant external calls. In Section IV, inter-contract calls are modeled by invalidating only return variables, justified by \"inter-contract calls in Solidity cannot directly modify other contracts' states.\" That is true only in a narrow direct-mutation sense. An external call to o.f() can reenter the caller—say, via a public setter or fallback—and change the caller's global storage before returning. Because the call-site postcondition keeps all caller globals unchanged, VeriSmart can later prove an arithmetic operation safe even when a concrete transaction violates the assertion. Analyzing the called function separately with entry/exit true does not repair this, since state changes to the caller are never propagated back. This is a load-bearing gap, not a nitpick, and the paper should fix it or explicitly restrict the guarantee to non-reentrant code.\n\nThe other limitations are less severe. The manual alarm classification is inherently subjective, and the Zeus comparison is hamstrung by public data; the authors admit both. The invariant template set was chosen from observed contracts, so generalization is an open question, but that is normal and they are transparent about it. The syntactic invalidity check is an interesting hack that could produce false positives, though they report none.\n\nMy take: the CEGIS transaction-invariant algorithm is the real contribution and it appears to work on the benchmarks. The reentrancy issue is a correctness problem in the soundness claim and should be addressed in revision, but it does not invalidate the engineering contribution. I would send this out—it deserves a careful referee and, with the reentrancy caveat made explicit, likely acceptance.","headline":"New CEGIS-style transaction invariant inference makes this a useful tool paper, but the 'exhaustive verification' claim breaks on reentrant external calls.","tokens_in":31350,"tokens_out":2906,"would_cite":true,"duration_ms":27235,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"VeriSmart claims to be the first smart-contract verifier that catches all arithmetic bugs in its benchmark (58 of 58 CVEs, 0.41% false alarms) by automatically discovering hidden transaction invariants.","keywords":["Ethereum smart contracts","arithmetic safety","integer overflow","transaction invariants","CEGIS verification","formal verification","static analysis","Solidity"],"falsifier":"Take a contract where an external or non-inlined function changes a storage variable through a path VeriSmart's side-effect analysis does not track, such as a delegatecall, and use that change to make an addition overflow; if VeriSmart reports the contract safe, the exhaustive-verification claim is refuted.","tokens_in":30395,"feed_emoji":"🛡️","tokens_out":11700,"duration_ms":93801,"temperature":0.7,"pith_summary":"VeriSmart is a verifier for Ethereum smart contracts that aims to settle the arithmetic-safety question exhaustively: every integer over/underflow and division-by-zero should be found, and every clean operation should be proven safe, without a flood of false alarms. The paper claims this is achievable on real contracts, reporting 58 of 58 known CVEs detected with only 2 false positives out of 492 alarms, a 0.41% false positive rate. The decisive idea is to automatically discover transaction invariants — facts such as \"the sum of all token balances equals the total supply\" that remain true across arbitrary interleavings of transactions — and feed them back into the verification loop. If the claim holds, developers could run VeriSmart before deployment and trust an exhaustive answer rather than a heuristic bug report, greatly reducing manual auditing effort.","feed_headline":"Ethereum verifier catches every known arithmetic bug in 60 contracts","feed_subtitle":"Hidden transaction invariants drive false alarms to 0.41% and expose six incorrect CVE reports.","key_machinery":"The load-bearing object is the transaction invariant, a formula over global contract state that is established by the constructor and preserved by every public function no matter how transactions interleave. Around it, the algorithm builds a counterexample-guided inductive synthesis loop. The validator converts the contract annotated with a candidate invariant into basic paths, uses the strongest-postcondition transformer sp to produce verification conditions that check both the inductiveness of the invariant and the safety of each assertion, and hands unproven paths to the generator. The generator refines the transaction invariant and loop-invariant map by conjoining atomic predicates restricted to the forms x = y, x >= y, x = n, x >= n, x <= n, and sum(x) = e, where sum denotes the total value stored in a Solidity mapping. A preprocessing step expands sum-equality into case-split constraints over the indices that actually appear in the path, after which an SMT solver, helped by fast syntactic invalidity checks and domain-specific validity templates, discharges the conditions.","core_discovery":"The central discovery is that the precision bottleneck for smart-contract verifiers is not the SMT solver but the absence of global, inter-transaction reasoning. VeriSmart observes that arithmetic operations in token-style contracts are usually safe only because of invariants that span all functions and all transactions — such as the sum of all balances equaling the total supply — and that these invariants are neither given by the programmer nor captured by standard abstract domains. The paper's algorithm adapts the counterexample-guided inductive synthesis (CEGIS) loop: a validator generates verification conditions annotated with a candidate transaction invariant and loop invariants, and a generator refines candidates by conjoining simple atomic predicates over variables and constants of the failing paths. This loop terminates with either a proof of safety or a list of potential violations, and the evaluation shows the discovered invariants are strong enough to prove safe the operations that two prior verifiers reported as alarms, and to expose six queries reported as CVE vulnerabilities as actually safe.","pith_inferences":["A natural extension is to let the generator propose quantified or disjunctive invariants; the two false alarms VeriSmart emits in benchmark #8 stem exactly from a quantifier-free restriction, so lifting it could remove even those.","The free-variable invalidity shortcut is a heuristic that can mislabel a valid condition as invalid, producing extra false alarms; a fallback that only skips the SMT call when the syntactic test is decisive would preserve speed without the approximation.","If transaction invariants are as decisive as the paper suggests, reentrancy and gas-limit analyses — which also need global state summaries across user calls — could inherit the same CEGIS machinery."],"forward_implications":["Deployers can treat a VeriSmart 'safe' verdict as an exhaustive answer for arithmetic safety across all possible transaction orderings, not merely a single execution.","The six queries marked vulnerable by CVE reports but proven safe by VeriSmart would need to be removed from vulnerability databases, changing downstream security advisories.","Verification cost of roughly one hour for all 60 CVE contracts suggests a feasible pre-deployment checking cycle for token contracts.","Because the algorithm is property-agnostic, a new safety property can be checked by swapping the assertion generator, as demonstrated by the ownership-takeover case study."],"supporting_citations":[{"why":"Supplies the interprocedural side-effect analysis used to over-approximate variables modified by non-inlined and inter-contract calls, which is the soundness-critical step of the call handling.","marker":"[25]"},{"why":"Introduces the counterexample-guided inductive synthesis loop that VeriSmart instantiates for smart contracts.","marker":"[13]"},{"why":"Provides the sketching/CEGIS foundation that motivates the generator-validator feedback design.","marker":"[15]"},{"why":"The baseline verifier whose false-positive rate VeriSmart must beat; its lack of inter-transaction reasoning motivates transaction invariants.","marker":"[12]"},{"why":"The baseline sound static analyzer for smart contracts whose inability to infer transaction invariants is the gap VeriSmart addresses.","marker":"[11]"},{"why":"The integer-bug finder baseline used to demonstrate VeriSmart's superior recall and false-positive rate on CVE contracts.","marker":"[7]"},{"why":"The SMT solver that discharges verification conditions after VeriSmart's domain-specific preprocessing.","marker":"[23]"}],"fun_headline_variants":["VeriSmart catches all arithmetic bugs in Ethereum smart contracts","Hidden invariants unlock precise Ethereum contract verification","Smart contract verifier ends false alarms with transaction invariants","Proof-based verifier finds every arithmetic flaw in 60 contracts","VeriSmart: precise safety verification for Ethereum arithmetic"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"VeriSmart's exhaustiveness depends on its analysis of which variables an external or non-inlined function call could change being complete; a single missed write could make the verifier certify a genuinely vulnerable contract as safe.","fun_headline_variants_meta":{"raw":{"variants":["VeriSmart catches all arithmetic bugs in Ethereum smart contracts","Hidden invariants unlock precise Ethereum contract verification","Smart contract verifier ends false alarms with transaction invariants","Proof-based verifier finds every arithmetic flaw in 60 contracts","VeriSmart: precise safety verification for Ethereum arithmetic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00027,"raw_usage":{"total_tokens":1621,"prompt_tokens":940,"completion_tokens":681,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":556,"completion_tokens_details":{"reasoning_tokens":603}},"tokens_in":556,"tokens_out":681,"duration_ms":6540,"temperature":1.0,"reasoning_tokens":603,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T10:21:21.703958+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a contract where an external or non-inlined function changes a storage variable through a path VeriSmart's side-effect analysis does not track, such as a delegatecall, and use that change to make an addition overflow; if VeriSmart reports the contract safe, the exhaustive-verification claim is refuted.","supporting_citations":[{"cited_title":"Interprocedural side-effect analysis in linear time,","cited_arxiv_id":null,"evidence_quote":"Supplies the interprocedural side-effect analysis used to over-approximate variables modified by non-inlined and inter-contract calls, which is the soundness-critical step of the call handling."},{"cited_title":"Combinatorial sketching for finite programs,","cited_arxiv_id":null,"evidence_quote":"Introduces the counterexample-guided inductive synthesis loop that VeriSmart instantiates for smart contracts."},{"cited_title":"Program synthesis by sketching,","cited_arxiv_id":null,"evidence_quote":"Provides the sketching/CEGIS foundation that motivates the generator-validator feedback design."},{"cited_title":"Smt-based verification of solidity smart contracts,","cited_arxiv_id":null,"evidence_quote":"The baseline verifier whose false-positive rate VeriSmart must beat; its lack of inter-transaction reasoning motivates transaction invariants."},{"cited_title":"ZEUS: analyzing safety of smart contracts,","cited_arxiv_id":null,"evidence_quote":"The baseline sound static analyzer for smart contracts whose inability to infer transaction invariants is the gap VeriSmart addresses."},{"cited_title":"Z3: An efficient smt solver,","cited_arxiv_id":null,"evidence_quote":"The SMT solver that discharges verification conditions after VeriSmart's domain-specific preprocessing."}],"review_version":1}