Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction

Affan Rauf; Muhammad Ali Amer; Muhammad Ali Hassan Ahmad; Muhammad Hashim Ali; Muhammad Hassan; Muhammad Naiman Jalil

REVIEW 4 major objections 6 minor 31 references

Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction

T0 review · 4 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Adding vulnerability-specific rules to Mythril cuts false positives by up to 89 percent while preserving true detections.

desk verdict The FP-reduction numbers are real but in-sample: the rules are fit to the same benchmark and 'ground truth' is treated as complete, so the 'without compromising true positives' claim is untested. read the letter →

arxiv 2608.10265 v1 pith:P3A7MIZ3 submitted 2026-08-10 cs.SE

Muhammad Ali Hassan Ahmad , Muhammad Hashim Ali , Muhammad Ali Amer , Muhammad Naiman Jalil , Muhammad Hassan , Affan Rauf This is my paper · ORCID

classification cs.SE

keywords smartcontractsecuritysymbolicexecutionfalsepositivereductionMythrilrule-basedanalysisEthereumGigahorsebenchmarkvulnerabilitydetection

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that the large volume of false positives produced by symbolic execution tools for Ethereum smart contracts is a reliability problem that can be attacked directly with lightweight, vulnerability-specific rules. The authors patch six such rules into Mythril, a widely used symbolic execution analysis tool, and evaluate the patched version on the Gigahorse benchmark. False positives fall from 102 to 51 on the invulnerable set and from 130 to 14 on the vulnerable set, while true positives rise from 12 to 13 and the F1-score increases from 0.152 to 0.605. A sympathetic reader would take the paper to establish that targeted rule-based filtering can substantially improve precision of symbolic execution tools without sacrificing detection of actual vulnerabilities.

What carries the argument

The mechanism is a set of six vulnerability-specific rules patched into Mythril's analysis code, mostly in its analyze_state functions and arithmetic helper. Each rule acts as an additional constraint or feasibility check that suppresses an alert unless a concrete exploitable path is shown to exist: state access after an external call is reported only when no reentrancy guard constrains the path; assertion violations are reported only when the previous opcode is REVERT and the assertion is always false; predictable-environment dependence is reported only when a tainted value actually influences world-state constraints and a satisfying transaction sequence exists; external calls to user-supplied addresses are reported only when an SSTORE follows the call and a valid transaction sequence is found; integer overflow or underflow is reported only when the Z3 solver confirms the wrap; and multiple calls in a single transaction are reported only when at least two external calls occur and the previous call succeeded. The rules therefore convert broad syntactic alarms into path-sensitive findings.

What would settle it

Have independent smart-contract auditors manually review a randomized sample of the alerts that the rules suppressed (the 51 invulnerable-set and 14 vulnerable-set remaining false positives, plus the alerts removed by each rule): if a substantial share are actually exploitable vulnerabilities omitted from the benchmark labels, the claim that true detection was not compromised fails; if the suppressed alerts are genuinely infeasible or guarded paths, the claim is supported.

Watch

Extended reading notes

Core claim

The paper's central claim is that a rule-based filtering layer, implemented directly inside a symbolic execution engine, can remove a large share of false vulnerability alerts while keeping, and even slightly improving, the detection of real ones. On the Gigahorse ground truth, the patched Mythril reduces false positives by 50.0 percent on the invulnerable contracts and by 89.2 percent on the vulnerable contracts, increases true positives from 12 to 13, raises recall from 75.0 percent to 81.2 percent, and lifts the F1-score from 0.152 to 0.605. The authors attribute the gains to rules that check path feasibility, require state changes or successful previous calls before reporting reentrancy, skip constructor calls, inspect taint and predictable environment variables, and use the Z3 solver to confirm overflow or underflow conditions.

Load-bearing premise

The evaluation treats the Gigahorse benchmark labels as complete and authoritative ground truth, so every Mythril report that does not match a label is counted as a false positive; if those labels miss real vulnerabilities or classify severity differently, the headline reductions could reflect label coverage rather than genuine false alarms.

Editorial extensions

If this is right

Mythril users would see a substantially smaller triage burden, since the number of alerts that must be manually inspected drops by half on clean contracts and by nearly ninety percent on vulnerable contracts.
Precision becomes a designable property of symbolic execution tools rather than an afterthought, because each fix is a small, localized enforcement of feasibility and state-effect checks.
The filtering layer is described as portable: any analyzer offering path feasibility queries, taint tracking, call-type classification, and state-effect detection could adopt the same rules, so the precision gains are not presented as exclusive to Mythril.
The remaining false positives concentrate almost entirely in integer arithmetic overflow and underflow, identifying that vulnerability class as the next target for more sophisticated rules.
Because recall also rose from 75.0 to 81.2 percent, the rules did not merely delete alarms; one true vulnerability missed by vanilla Mythril was recovered.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the same rules were ported to other symbolic execution engines, the size of the gain would likely depend on how many of their baseline alerts already survive a basic feasibility check; tools with different over-approximation patterns may need additional rules tuned to their own false-positive modes.
The concentration of remaining false positives in integer arithmetic suggests that a semantic treatment of wraparound, tied to the actual path constraints rather than to a syntactic overflow pattern, may be a more direct route to closing the gap than further per-vulnerability rules.
Because the evaluation counts any Mythril finding absent from the benchmark labels as a false positive, the magnitude of the reported improvement would change if a different, independently audited label set were used; a testable extension is to rerun the patched tool on a second labeled corpus and compare the false-positive reduction.
For practitioners, the practical value may be larger than the F1 improvement suggests, since the cost of investigating a false alarm is not linear in the alert count: removing the most obviously infeasible paths first removes the cheapest categories of false alarms.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this is a plausible engineering contribution with an evaluation that doesn't support its strongest claim. The authors hand-patched Mythril to suppress false positives across six vulnerability classes and measured 50% and 89% FP reductions on the Gigahorse benchmark. The numbers are internally consistent, but the rules were designed from that same benchmark's false positives, and the benchmark labels are treated as if they were complete. That makes the headline result an in-sample improvement, not a general one.

What's genuinely useful: the paper documents concrete rule ideas—path feasibility checks, taint tracking, call classification, state-effect checks—and gives enough detail (algorithms and partial code descriptions) that someone could port them to another tool. It also honestly reports the integer overflow outlier, where FPs got worse on both datasets while it was the only class with confirmed true positives.

The soft spots are the usual ones, but they bite hard here. First, no held-out evaluation. The rules are hand-crafted after inspecting the very false positives they're then measured against. Second, the FP definition is 'not in the ground truth reference,' which conflates 'not labeled' with 'not a vulnerability.' On the vulnerable set, five of the six classes have zero true positives, so 116 of the 130 baseline FPs are reports in classes where the benchmark provides no evidence that any report is real. Suppressing those alerts might be suppressing genuine findings. Third, the only class with confirmed TPs, integer arithmetic, saw FP counts increase from 34 to 50 (invulnerable) and 11 to 12 (vulnerable). The net TP gain is one, so the phrase 'without compromising detection of true vulnerabilities' is untested. Fourth, the novelty claim is overstated: Clairvoyance, RA, and GPTScan already prune alerts via path feasibility and state effects. Finally, no code or data release, so the numbers can't be independently checked.

Who's this for? Practitioners who want to reduce alert noise in Mythril will find useful starting points. For the research claim, the paper needs a held-out benchmark, released code, and a deeper analysis of the integer overflow rule. I'd send it to peer review—a good referee could push it toward a usable evaluation—but it's not ready as-is.

Referee Report

4 major / 6 minor

Summary. This paper addresses the false-positive problem in symbolic execution-based smart contract vulnerability detection by proposing six rule-based modifications to Mythril, one per vulnerability class. The rules are derived from an analysis of Mythril's baseline reports on the Gigahorse benchmark. The authors evaluate the enhanced Mythril on the same benchmark (40 invulnerable and 100 vulnerable contracts), reporting a reduction in false positives from 102 to 51 on the invulnerable set and from 130 to 14 on the vulnerable set, while true positives increase from 12 to 13, raising the F1-score from 0.152 to 0.605.

Significance. If the reported reductions were representative of out-of-sample behavior, the paper would provide a practical, lightweight recipe for improving the precision of symbolic execution tools. The strengths are the reproducible setup (pinned commit hashes for Mythril and the benchmark), the internally consistent counts in Table I, and the candid acknowledgment of the integer-arithmetic outlier. However, the evaluation design limits what can be concluded: the rules are developed and measured on the same dataset, and the ground-truth labels are treated as complete. The contribution is therefore an engineering demonstration on a single benchmark rather than a validated general method.

major comments (4)

[Sections IV–VI] The rules are designed from the baseline false positives observed on the Gigahorse benchmark (Section IV) and then evaluated on the same Gigahorse benchmark (Section VI), making the reported FP reductions in-sample results rather than out-of-sample predictions. For example, the 'State access after an external call' rule in Section V.A is described as eliminating false positives by changing how reentrancy checks are invoked, which directly addresses the 15 invulnerable-set FPs counted in Table I. Because no held-out dataset or cross-validation is used, the headline numbers (102→51 and 130→14) may overstate the improvement on new contracts. The authors should evaluate the same rules on a separate benchmark (e.g., SmartBugs Wild or a manually audited contract set) to support the generalizability claim.
[Section IV] The evaluation defines 'Any vulnerability flagged by Mythril but absent in the ground truth reference was considered a false positive,' which conflates 'not labeled' with 'not a vulnerability.' Since Table I shows zero true positives for five of the six targeted classes on the vulnerable set, the entire vulnerable-set FP reduction in those classes (e.g., 57→0 for State Access after an External Call and 18→0 for Dependence on Predictable Environment Variable) consists of reports whose status is unverified. If a suppressed report corresponds to an unlabeled real vulnerability, the tool has silently traded false positives for false negatives. The claim 'without compromising the detection of true vulnerabilities' is therefore untested for the classes that contribute most of the reported FP reduction. A manual audit of a sample of the suppressed reports, or a comparison against a more complete vulnerability database, is needed.
[Table I and Section VI.B] The single class with confirmed true positives and false negatives is Integer Arithmetic (TP 12→13, FN 4→3), yet Table I shows that in this class the improved Mythril increases FPs on the invulnerable set from 34 to 50 and on the vulnerable set from 11 to 12. The paper acknowledges this as an 'outlier,' but because this class is the only one where the benchmark provides TP evidence, the overall improvement of F1 from 0.152 to 0.605 rests on suppressing reports in classes with no positive evidence while the confirmed class gets worse in FPs. This undermines the abstract's statement that the reduction is achieved 'without compromising the detection of true vulnerabilities' for the vulnerability type where detection is actually observable.
[Section VI and Table III] The claim of a 'significant reduction' in false positives is not supported by any statistical test or uncertainty quantification. The counts are small (e.g., 12 vs. 13 true positives, 130 vs. 14 FPs), and the F1 increase from 0.152 to 0.605 is a point estimate. A simple McNemar test on the paired contract-level TP/FP outcomes across the 140 contracts, or bootstrap confidence intervals on the F1 difference, would establish whether the observed improvement is likely to be reproducible. Without this, 'significant' is an informal descriptor rather than a statistical claim.

minor comments (6)

[Section III.C] The word 'benchamarks' is a typo and should be 'benchmarks.'
[Table I] The total row reads 'Total Functions Flgged'; this should be corrected to 'Total Functions Flagged.'
[Section II] The related work section is a series of per-paper summaries rather than a synthesis, and several references are inconsistently formatted (e.g., [4] and [13] have malformed author lists).
[Section V.A] Algorithm 1 is incomplete and detached from the surrounding text: the numbered list describes steps that do not correspond one-to-one to the algorithm's pseudocode, making it hard to reproduce the rule from the text alone.
[Sections VIII–IX] The paper has two future-work sections: Section VIII (Conclusion and Future Work) is followed by Section IX (Future Work). These should be merged into a single section.
[Section VII.C] The claim that Oyente and Manticore are 'conceptually suited' for porting the rules is speculative, since no implementation on those tools is provided; the portability claim is unsubstantiated beyond the stated prerequisites.

Circularity Check

1 steps flagged · score 6.0 of 10

Rule-based FP reductions are measured on the same Gigahorse benchmark from which the rules were derived; the headline gains are in-sample rather than out-of-sample.

fitted input called prediction [Abstract / Section III-A / Section III-C / Tables I and III]
"We analyze the root causes of these inaccuracies and devise a rule-based approach based on the gained insight to reduce false positives. ... Any vulnerability flagged by Mythril but absent in the ground truth reference was considered a false positive."

The rules are explicitly derived from root-cause analysis of the same false positives that Table I then counts. The improved Mythril is evaluated on the same Gigahorse datasets (40 invulnerable, 100 vulnerable), and the reported reductions (102→51 and 130→14; F1 0.152→0.605) are in-sample measurements of the data that motivated the rules. No independent or held-out benchmark is used; Section IX lists expanding the ground truth as future work. The claim 'without compromising the detection of true vulnerabilities' is also assessed only against the same labels, so suppressed unlabeled reports cannot count as lost true positives. The rule set is thus a hand-fitted input whose effectiveness is reported as a validation result rather than a prediction.

full rationale

The paper does not rely on self-citations to justify its central claim, and the rules themselves are concrete code changes (feasibility checks, taint tracking, call classification) rather than definitions of the target result. However, the abstract states that the rules were devised from root-cause analysis of the inaccuracies, and the evaluation then measures false positives on the same Gigahorse benchmark (Tables I and III). No held-out dataset or external validation is reported; the paper's own future-work section says the ground truth should be expanded for more rigorous testing. The vulnerable-set reduction (130→14 FPs) is concentrated in the five classes with zero labeled true positives, so the 'without compromising true vulnerabilities' claim is only tested against labels that define FP as absence from the ground truth. This is partial circularity: the fitted rule set is validated on its training data. I do not count the label-completeness issue as a separate circular step; it is a ground-truth validity threat rather than a definitional equivalence.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

The central claim rests on a small number of assumptions: the completeness of Gigahorse labels, the choice of six vulnerability classes, a specific reentrancy model, and an unverified portability claim. There is one hand-set numeric threshold in the arithmetic rule. No new theoretical entities or fitted parameters are introduced.

free parameters (1)

MAX_GAS_LIMIT = 1,000,000 (hard-coded)
Algorithm 5 uses a hand-set maximum gas limit of 1,000,000 when deciding whether overflow constraints are satisfiable. This is an arbitrary threshold, not derived from data or theory, and it affects which arithmetic reports survive filtering.

assumptions (4)

domain assumption Gigahorse benchmark labels are complete and correct ground truth.
Section IV defines true positives, false positives, and false negatives relative to these labels and counts any unlisted Mythril report as a false positive. If the labels are incomplete or use a different taxonomy, the FP counts are inflated.
ad hoc to paper The six targeted vulnerability types are the most impactful and representative choices.
No formal criterion is given for selecting these six types. Table I shows one of them, Integer Arithmetic, worsened on the invulnerable set, so this selection materially shapes the aggregate improvement.
domain assumption Reentrancy requires a state modification after an external call.
Rules C and D assume that a state write after an external call is necessary for a reentrancy vulnerability. This is a common modeling assumption, but variants such as read-only reentrancy do not satisfy it, so true positives of those variants could be discarded.
domain assumption The proposed rules are portable to other symbolic execution frameworks.
Section VII asserts that only basic primitives are needed and that Oyente and Manticore are conceptually suited, but no implementation in another tool is provided. The portability claim is unverified.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction." pith.science (2026). https://pith.science/paper/P3A7MIZ3

@misc{pith2026260810265,
  author       = {Pith},
  title        = {Pith review of: Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/P3A7MIZ3}},
  note         = {Machine review of arXiv:2608.10265}
}

read the original abstract

A blockchain is a decentralized, secure ledger system that enables transparent and immutable record-keeping, essential for trust and security in digital transactions. Smart contracts are self-executing agreements encoded on a blockchain, enabling different parties to fulfill the terms of the agreement automatically. These contracts trigger corresponding actions when conditions are met, ensuring decentralized and transparent transactions. Writing reliable smart contracts is challenging due to the lack of standardization. To find security vulnerabilities, tools based on various approaches, including symbolic execution, are used. However, these tools often report a large number of false positives, raising concerns about their reliability. The time and effort spent investigating false positives diverts resources from addressing actual vulnerabilities. Therefore, such tools must also be evaluated according to the rate of false positives they exhibit. More importantly, the algorithms and heuristics used by the tools must be enhanced to distinguish between true vulnerabilities and false alarms. In this paper, we first demonstrate the prevalence of false positives in vulnerability reports generated by Mythril, a symbolic execution-based analysis tool for Ethereum smart contracts. We analyze the root causes of these inaccuracies and devise a rule-based approach based on the gained insight to reduce false positives. We implement our rules for the most impactful vulnerabilities in Mythril and assess the effectiveness of our approach. Our results show a significant reduction in false positives without compromising the detection of true vulnerabilities, thus enhancing the tool's reliability.

Figures

Figures reproduced from arXiv: 2608.10265 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 25 canonical work pages

[1]

Mythril,

“Mythril,” 2018. [Online]. Available: https://github.com/ConsenSys/ mythril

work page 2018
[2]

Gigahorse-benchmarks,

N. Grech, “Gigahorse-benchmarks,” 2019. [Online]. Available: https: //github.com/nevillegrech/gigahorse-benchmarks

work page 2019
[3]

How Effective are Smart Contract Analysis Tools? Evaluating Smart Contract Static Analysis Tools Using Bug Injection

A. Ghaleb and K. Pattabiraman, “How effective are smart contract analysis tools? evaluating smart contract static analysis tools using bug injection,”CoRR, vol. abs/2005.11613, 2020. [Online]. Available: https://arxiv.org/abs/2005.11613

work page Pith review arXiv 2005
[4]

Solidifi benchmark,

K. Asem Ghaleb and Pattabiraman, “Solidifi benchmark,”

work page
[5]

Loi Luu, H

D.-H. Loi Luu, H. Chu, P. Olickel, A. Saxena, and Hobor, “Oyente,”

work page
[6]

Securify,

P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. B ¨unzli, and M. Vechev, “Securify,” 2020. [Online]. Available: https://github.com/ eth-sri/securify

work page 2020
[7]

Available: https://github.com/enzymefinance/oyente

[Online]. Available: https://github.com/enzymefinance/oyente

work page
[8]

Manticore,

“Manticore,” 2017. [Online]. Available: https://github.com/trailofbits/ manticore

work page 2017

Show all 31 references

[9]

Smartcheck: Static analysis of ethereum smart contracts,

S. Tikhomirov, E. V oskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y . Alexandrov, “Smartcheck: Static analysis of ethereum smart contracts,” in2018 IEEE/ACM 1st International Work- shop on Emerging Trends in Software Engineering for Blockchain (WETSEB), 2018, pp. 9–16

2018
[10]

Empirical vulnerability analysis of automated smart contracts security testing on blockchains,

R. M. Parizi, A. Dehghantanha, K. R. Choo, and A. Singh, “Empirical vulnerability analysis of automated smart contracts security testing on blockchains,”CoRR, vol. abs/1809.02702, 2018. [Online]. Available: http://arxiv.org/abs/1809.02702

2018 arXiv
[11]

Precise attack synthesis for smart contracts,

Y . Feng, E. Torlak, and R. Bodik, “Precise attack synthesis for smart contracts,” 2019

2019
[12]

Remix - solidity ide,

“Remix - solidity ide,” 2017. [Online]. Available: http://remix.ethereum. org

2017
[13]

Security vulnerabilities in ethereum smart contracts,

A. Dika and M. Nowostawski, “Security vulnerabilities in ethereum smart contracts,” in2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CP- SCom) and IEEE Sma...

2018
[14]

Formal verification of smart contracts: Short paper,

K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamyet al., “Formal verification of smart contracts: Short paper,” inProceedings of the 2016 ACM workshop on programming languages and analysis f...

2016
[15]

Security vulnerabilities in ethereum smart contracts,

A. Mense and M. Flatscher, “Security vulnerabilities in ethereum smart contracts,” inProceedings of the 20th International Conference on Information Integration and Web-Based Applications & Services, ser. iiW AS2018. New York, NY , USA: Association for Computing Machinery, 201...

2018
[16]

Analysis of blockchain smart contracts: Techniques and insights,

S. Kim and S. Ryu, “Analysis of blockchain smart contracts: Techniques and insights,” in2020 IEEE Secure Development (SecDev), 2020, pp. 65–73

2020
[17]

Under-optimized smart contracts devour your money,

T. Chen, X. Li, X. Luo, and X. Zhang, “Under-optimized smart contracts devour your money,” in2017 IEEE 24th international conference on software analysis, evolution and reengineering (SANER). IEEE, 2017, pp. 442–446

2017
[18]

Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart con- tracts,

Y . Xue, M. Ma, Y . Lin, Y . Sui, J. Ye, and T. Peng, “Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart con- tracts,” in2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2020, pp. 1029–1040

2020
[19]

Static analysis of integer overflow of smart contracts in ethereum,

E. Lai and W. Luo, “Static analysis of integer overflow of smart contracts in ethereum,” inProceedings of the 2020 4th International Conference on Cryptography, Security and Privacy, ser. ICCSP 2020. New York, NY , USA: Association for Computing Machinery, 2020, pp. 110–115. [...

2020
[20]

Ra: Hunting for re- entrancy attacks in ethereum smart contracts via static analysis,

Y . Chinen, N. Yanai, J. P. Cruz, and S. Okamura, “Ra: Hunting for re- entrancy attacks in ethereum smart contracts via static analysis,” in2020 IEEE International Conference on Blockchain (Blockchain), 2020, pp. 327–336

2020
[21]

Solanalyser: A framework for analysing and testing smart contracts,

S. Akca, A. Rajan, and C. Peng, “Solanalyser: A framework for analysing and testing smart contracts,” in2019 26th Asia-Pacific Soft- ware Engineering Conference (APSEC), 2019, pp. 482–489

2019
[22]

A semantic analysis-based method for smart contract vulnerability,

X. Yan, S. Wang, and K. Gai, “A semantic analysis-based method for smart contract vulnerability,” in2022 IEEE 8th Intl Conference on Big Data Security on Cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computing, (HPSC) and IEEE Intl Conference on I...

2022
[23]

Smartbugs: A framework to analyze solidity smart contracts,

J. F. Ferreira, P. Cruz, T. Durieux, and R. Abreu, “Smartbugs: A framework to analyze solidity smart contracts,”CoRR, vol. abs/2007.04771, 2020. [Online]. Available: https://arxiv.org/abs/2007. 04771

2007 arXiv
[24]

Detection of vulnerabilities of blockchain smart contracts,

D. He, R. Wu, X. Li, S. Chan, and M. Guizani, “Detection of vulnerabilities of blockchain smart contracts,” 2023. [Online]. Available: https://ieeexplore.ieee.org/document/10034747/

2023
[25]

Security threat mitigation for smart contracts: A comprehensive survey,

N. Ivanov, C. Li, Q. Yan, Z. Sun, Z. Cao, and X. Luo, “Security threat mitigation for smart contracts: A comprehensive survey,” inACM Computing Surveys, 2023. [Online]. Available: https://dl.acm.org/doi/10.1145/3593293

2023 doi
[26]

Demystifying invariant effectiveness for securing smart contracts,

Z. Chen, Y . Liu, S. M. Beillahi, Y . Li, and F. Long, “Demystifying invariant effectiveness for securing smart contracts,” 2024, pp. 1772–

2024
[27]

When chatgpt meets smart contract vulnerability detection: How far are we?

C. Chen, J. Su, J. Chen, Y . Wang, T. Bi, J. Yu, Y . Wang, X. Lin, T. Chen, and Z. Zheng, “When chatgpt meets smart contract vulnerability detection: How far are we?” 2024. [Online]. Available: http://arxiv.org/abs/2309.05520

2024 arXiv
[28]

Z3: An efficient smt solver,

L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” inTools and Algorithms for the Construction and Analysis of Systems, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14. Springer, 2008, pp. 337–340

2008
[30]

Gptscan: Detecting logic vulnerabilities in smart contracts by combining gpt with program analysis,

Y . Sun, D. Wu, Y . Xue, H. Liu, H. Wang, Z. Xu, X. Xie, and Y . Liu, “Gptscan: Detecting logic vulnerabilities in smart contracts by combining gpt with program analysis,” pp. 1–13, 2024. [Online]. Available: https://dl.acm.org/doi/10.1145/3597503.3639117

2024
[1795]

Available: https://dl.acm.org/doi/10.1145/3660786

[Online]. Available: https://dl.acm.org/doi/10.1145/3660786

doi
[2020]

Available: https://github.com/DependableSystemsLab/ SolidiFI-benchmark

[Online]. Available: https://github.com/DependableSystemsLab/ SolidiFI-benchmark

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Mythril,

“Mythril,” 2018. [Online]. Available: https://github.com/ConsenSys/ mythril

work page 2018

[2] [2]

Gigahorse-benchmarks,

N. Grech, “Gigahorse-benchmarks,” 2019. [Online]. Available: https: //github.com/nevillegrech/gigahorse-benchmarks

work page 2019

[3] [3]

How Effective are Smart Contract Analysis Tools? Evaluating Smart Contract Static Analysis Tools Using Bug Injection

A. Ghaleb and K. Pattabiraman, “How effective are smart contract analysis tools? evaluating smart contract static analysis tools using bug injection,”CoRR, vol. abs/2005.11613, 2020. [Online]. Available: https://arxiv.org/abs/2005.11613

work page Pith review arXiv 2005

[4] [4]

Solidifi benchmark,

K. Asem Ghaleb and Pattabiraman, “Solidifi benchmark,”

work page

[5] [5]

Loi Luu, H

D.-H. Loi Luu, H. Chu, P. Olickel, A. Saxena, and Hobor, “Oyente,”

work page

[6] [6]

Securify,

P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. B ¨unzli, and M. Vechev, “Securify,” 2020. [Online]. Available: https://github.com/ eth-sri/securify

work page 2020

[7] [7]

Available: https://github.com/enzymefinance/oyente

[Online]. Available: https://github.com/enzymefinance/oyente

work page

[8] [8]

Manticore,

“Manticore,” 2017. [Online]. Available: https://github.com/trailofbits/ manticore

work page 2017